|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
18th IEEE Real-Time Systems Symposium (RTSS '97)
On-the-fly symbolic model checking for real-time systems
San Francisco, CA
December 03-December 05
ISBN: 0-8186-8268-X
| ASCII Text | x | ||
| A. Bouajjani, S. Tripakis, S. Yovine, "On-the-fly symbolic model checking for real-time systems," 2011 IEEE 32nd Real-Time Systems Symposium, pp. 25, 18th IEEE Real-Time Systems Symposium (RTSS '97), 1997. | |||
| BibTex | x | ||
| @article{ 10.1109/REAL.1997.641266, author = {A. Bouajjani and S. Tripakis and S. Yovine}, title = {On-the-fly symbolic model checking for real-time systems}, journal ={2011 IEEE 32nd Real-Time Systems Symposium}, volume = {0}, year = {1997}, issn = {1052-8725}, pages = {25}, doi = {http://doi.ieeecomputersociety.org/10.1109/REAL.1997.641266}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - 2011 IEEE 32nd Real-Time Systems Symposium TI - On-the-fly symbolic model checking for real-time systems SN - 1052-8725 SP EP A1 - A. Bouajjani, A1 - S. Tripakis, A1 - S. Yovine, PY - 1997 KW - temporal logic; on-the-fly symbolic model checking; real-time systems; timed automaton; timed temporal logic; boolean combinations; linear inequalities; FDDI protocol verification VL - 0 JA - 2011 IEEE 32nd Real-Time Systems Symposium ER - | |||
This paper presents an on-the-fly and symbolic algorithm for checking whether a timed automaton satisfies a formula of a timed temporal logic which is more expressive than TCTL. The algorithm is on-the-fly in the sense that the state-space is generated dynamically and only the minimal amount of information required by the verification procedure is stored in memory. The algorithm is symbolic in the sense that it manipulates sets of states, instead of states, which are represented as boolean combinations of linear inequalities of clocks. We show how a prototype implementation of our algorithm has improved the performances of the tool KRONOS for the verification of the FDDI protocol.
Index Terms:
temporal logic; on-the-fly symbolic model checking; real-time systems; timed automaton; timed temporal logic; boolean combinations; linear inequalities; FDDI protocol verification
Citation:
A. Bouajjani, S. Tripakis, S. Yovine, "On-the-fly symbolic model checking for real-time systems," rtss, pp.25, 18th IEEE Real-Time Systems Symposium (RTSS '97), 1997
Usage of this product signifies your acceptance of the Terms of Use.