Modeling and Verification of TTCAN Startup Protocol Using Synchronous Calendar

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 fault-tolerant 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.