Symbolic model checking for event-driven real-time systems

In this article, we consider symbolic model checking for event-driven real-time systems. We first propose a Synchronous Real-Time Event Logic (SREL) for capturing the formal semantics of synchronous, event-driven real-time systems. The concrete syntax of these systems is given in terms of a graphical programming language called Modechart hy Jahanian and Mok, which can be translated into SREL structures. We then present a symbolic model-checking algorithm for SREL. In particular, we give an efficient algorithm for constructing OBDDs (ordered Binary Decision Diagrams) for linear constraints among integer variables. This is very important in a BDD-based symbolic model checker for real-time systems, since timing and event occurrence constraints are used very often in the specification of these systems. We have incorporated our construction algorithm into the SMV v2.3 from Carnegie-Mellon University and have been able to achieve one to two orders of magnitude in speedup and space saving when compared to the implementation of timing and event-counting functions by integer arithmetics provided by SMV.