 |
|
|||
| Authors: | Karsten Strehl |
| Group: | Computer Engineering |
| Type: | Inproceedings |
| Title: | Interval Diagrams: Increasing Efficiency of Symbolic Real-Time Verification |
| Year: | 1999 |
| Month: | December |
| Pub-Key: | Str99 |
| Book Titel: | Proceedings of the 6th International Conference on Real-Time Computing Systems and Applications (RTCSA `99) |
| Pages: | 488-491 |
| Keywords: | SMC IDD |
| Abstract: | 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. |
| Remarks: | Proceedings of the 6th International Conference on Real-Time Computing Systems and Applications (RTCSA `99), Hong Kong, pages 488-491, December 13-15, 1999 |
| Location: | Hong Kong |
| Resources: | [BibTeX] [Paper as PDF] |
