Symbolic Model Checking for Event-Driven Real-Time Systems

23Citations
Citations of this article
10Readers
Mendeley users who have this article in their library.

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.

Cite

CITATION STYLE

APA

Yang, J., Mok, A. K., & Wang, F. (1997). Symbolic Model Checking for Event-Driven Real-Time Systems. ACM Transactions on Programming Languages and Systems, 19(2), 386–412. https://doi.org/10.1145/244795.244803

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free