DocumentCode
2894301
Title
Symbolic model checking for real-time systems
Author
Henzinger, Thomas A. ; Nicollin, X. ; Sifakis, Joseph ; Yovine, S.
Author_Institution
Dept. of Comput. Sci., Cornell Univ., Ithaca, NY, USA
fYear
1992
fDate
22-25 Jun 1992
Firstpage
394
Lastpage
406
Abstract
Finite-state programs over real-numbered time in a guarded-command language with real-valued clocks are described. Model checking answers the question of which states of a real-time program satisfy a branching-time specification. An algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space, is given
Keywords
formal specification; program verification; programming theory; real-time systems; CTL; automatic verification; branching-time specification; finite state programs; guarded-command language; real-numbered time; real-time program; real-time systems; real-valued clocks; state predicates; state space; symbolic model checking; Algorithm design and analysis; Boolean functions; Clocks; Computer science; Data structures; Power system modeling; Real time systems; Safety; State-space methods; Upper bound;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on
Conference_Location
Santa Cruz, CA
Print_ISBN
0-8186-2735-2
Type
conf
DOI
10.1109/LICS.1992.185551
Filename
185551
Link To Document