Name
Title | ||
|---|---|---|
Modeling and verification of master/slave clock synchronization using hybrid automata and model-checking |
Abstract | ||
|---|---|---|
An accurate and reliable clock synchronization mechanism is a basic requirement for the correctness of many safety-critical systems. Establishing the correctness of such mechanisms is thus imperative. This paper addresses the modeling and formal verification of a specific fault-tolerant master/slave clock synchronization system for the Controller Area Network. It is shown that this system may be modeled with hybrid automata in a very natural way. However, the verification of the resulting hybrid automata is intractable, since the modeling requires variables that are dependent. This particularity forced us to develop some modeling techniques by which we translate the hybrid automata into singlerate timed automata verifiable with the model-checker UPPAAL. These techniques are described and illustrated by means of a simple example. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-76650-6_18 | ICFEM |
Keywords | Field | DocType |
controller area network,reliable clock synchronization mechanism,safety-critical system,basic requirement,model-checker uppaal,slave clock synchronization system,simple example,modeling technique,hybrid automaton,formal verification,fault tolerant,clock synchronization,model checking | Synchronization,Slave clock,Computer science,Correctness,Real-time computing,Theoretical computer science,Timed automaton,Clock synchronization,Master/slave,Hybrid automaton,Distributed computing,Formal verification | Conference |
Volume | ISSN | ISBN |
4789 | 0302-9743 | 3-540-76648-0 |
Citations | PageRank | References |
0 | 0.34 | 9 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Guillermo Rodriguez-Navas | 1 | 23 | 3.47 |
| Julián Proenza | 2 | 18 | 3.27 |
| H. Hansson | 3 | 399 | 40.19 |