Timeout and calendar based finite state Modeling and verification of real-time systems

To overcome the complexity of verification of real-time systems with dense time dynamics, Dutertre and Sorea proposed timeout and calender based transition systems to model real-time systems and verify safety properties using k-induction. In this work, we propose a canonical finitary reduction technique, which reduces the infinite state space of timeout and calender based transition systems to a finite state space. The technique is formalized in terms of clockless finite state timeout and calendar based models represented as predicate transition diagrams. Using the proposed reduction, we can verify these systems using finite state model checkers and thus can avoid the complexity of induction based proof methodology. We present examples of Train-Gate Controller and the TTA startup algorithm to demonstrate how such an approach can be efficiently used for verifying safety, liveness, and timeliness properties using the finite state model checker Spin.