Symboloc Model Checking for Event-Driven Real-Time Systems

Abstract

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, by 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.