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 Logi c (SREL) for capturing the formal semantics of synchronous, event-driv en real-time systems. The concrete syntax of these systems is given in terms of a graphical programming language called Modechart hy Jahania n and Mok, which can be translated into SREL structures. We then prese nt a symbolic model-checking algorithm for SREL. In particular, we giv e an efficient algorithm for constructing OBDDs (ordered Binary Decisi on Diagrams) for linear constraints among integer variables. This is v ery important in a BDD-based symbolic model checker for real-time syst ems, since timing and event occurrence constraints are used very often in the specification of these systems. We have incorporated our const ruction algorithm into the SMV v2.3 from Carnegie-Mellon University an d have been able to achieve one to two orders of magnitude in speedup and space saving when compared to the implementation of timing and eve nt-counting functions by integer arithmetics provided by SMV.