J. Yang et al., SYMBOLIC MODEL CHECKING FOR EVENT-DRIVEN REAL-TIME SYSTEMS, ACM transactions on programming languages and systems, 19(2), 1997, pp. 386-412
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.