Symbolic model checking for event-driven real-time systems

Author

Yang, Jin ; Mok, Aloysius K. ; Wang, Farn

Author_Institution

Dept. of Comput. Sci., Texas Univ., Austin, TX, USA

fYear

1993

fDate

1-3 Dec 1993

Firstpage

23

Lastpage

32

Abstract

We consider symbolic model-checking for event-driven real-time systems. The concrete syntax of these systems is given in terms of a graphical programming language called Modechart. We propose a logic, Synchronous Real-Time Event logic (SREL) for specifying the timing properties of these systems. We then present a symbolic model-checking algorithm which checks a modechart against an SREL formula, and discuss several implementation issues. In particular, we give an efficient solution to the problem of encoding timing and event counting functions based on Binary Decision Diagram (BDD). This solution has been incorported into the SMV system v2.3 and has been able to achieve one to two orders of magnitude in speedup and space saving when compared to the solution based on the integer operations provided by the SMV system

Keywords

algebraic specification; diagrams; formal logic; formal specification; formal verification; real-time systems; visual languages; visual programming; Binary Decision Diagram; Modechart; SMV system; SREL; Synchronous Real-Time Event logic; concrete syntax; encoding; event counting functions; event-driven real-time systems; graphical programming language; integer operations; space saving; specification; speedup; symbolic model-checking; timing properties; Binary decision diagrams; Boolean functions; Computer languages; Concrete; Contracts; Data structures; Encoding; Logic programming; Real time systems; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Real-Time Systems Symposium, 1993., Proceedings.

Conference_Location

Raleigh Durham, NC

Print_ISBN

0-8186-4480-X

Type

conf

DOI

10.1109/REAL.1993.393518

Filename

393518