Name
Abstract | ||
|---|---|---|
We describe the modeling and verification of TTCAN startup protocol using SAL model checker. For the modeling purposes we propose a new modeling framework called Synchronous Calendar which can be seen as an adaptation of Calendar based models introduced by Duterte and Sorea. A Synchronous Calendar can express dense time systems without relying on continuously varying clocks and supports synchronous message transmission. We capture both fault-free and faulttolerant aspects of startup algorithm of TTCAN in two different models and verify the safety and liveness properties for them. Our verification technique relies on induction and abstraction methods which are supported by SAL model checker. To our knowledge this is the first work towards a formal analysis of TTCAN startup protocol. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1109/SEFM.2007.27 | SEFM |
Keywords | Field | DocType |
different model,synchronous calendar,dense time system,startup algorithm,abstraction method,new modeling framework,ttcan startup protocol,modeling purpose,verification technique,sal model checker,data structures,synchronisation,fault tolerant,formal verification | Data structure,Synchronization,Model checking,Computer science,Electronic messaging,Embedded system,Distributed computing,Liveness,Formal verification | Conference |
ISSN | ISBN | Citations |
1551-0255 | 0-7695-2884-8 | 1 |
PageRank | References | Authors |
0.39 | 7 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Indranil Saha | 1 | 296 | 18.27 |
| Suman Roy | 2 | 21 | 7.25 |
| Kuntal Chakraborty | 3 | 3 | 0.84 |