|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99)
Interval Diagrams: Increasing Efficiency of Symbolic Real-Time Verification
Hong Kong, China
December 13-December 15
ISBN: 0-7695-0306-3
| ASCII Text | x | ||
| Karsten Strehl, "Interval Diagrams: Increasing Efficiency of Symbolic Real-Time Verification," 2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, pp. 488, Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), 1999. | |||
| BibTex | x | ||
| @article{ 10.1109/RTCSA.1999.811303, author = {Karsten Strehl}, title = {Interval Diagrams: Increasing Efficiency of Symbolic Real-Time Verification}, journal ={2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications}, volume = {0}, year = {1999}, issn = {1530-1427}, pages = {488}, doi = {http://doi.ieeecomputersociety.org/10.1109/RTCSA.1999.811303}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - 2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications TI - Interval Diagrams: Increasing Efficiency of Symbolic Real-Time Verification SN - 1530-1427 SP EP A1 - Karsten Strehl, PY - 1999 KW - Formal verification KW - timed reachability analysis KW - real-time symbolic model checking KW - timed automata KW - binary decision diagrams VL - 0 JA - 2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications ER - | |||
In this paper, we suggest interval diagram techniques for formal verification of real-time systems modeled by means of timed automata. Interval diagram techniques are based on interval decision diagrams (IDDs) -- representing sets of system configurations of, e.g., timed automata -- and interval mapping diagrams (IMDs) -- modeling their transition behavior. IDDs are canonical representations of Boolean functions and allow for their efficient manipulation. Our approach is used for performing both timed reachability analysis and real-time symbolic model checking. We present the methods necessary for our approach and compare its results to another, similar verification technique -- achieving a speedup of 7 and more.
Index Terms:
Formal verification, timed reachability analysis, real-time symbolic model checking, timed automata, binary decision diagrams
Citation:
Karsten Strehl, "Interval Diagrams: Increasing Efficiency of Symbolic Real-Time Verification," rtcsa, pp.488, Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), 1999
Usage of this product signifies your acceptance of the Terms of Use.