Please use this identifier to cite or link to this item:
https://doi.org/10.1007/978-3-642-10373-5_30
Title: | Verifying stateful timed CSP using implicit clocks and zone abstraction | Authors: | Sun, J. Liu, Y. Dong, J.S. Zhang, X. |
Issue Date: | 2009 | Citation: | Sun, J.,Liu, Y.,Dong, J.S.,Zhang, X. (2009). Verifying stateful timed CSP using implicit clocks and zone abstraction. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5885 LNCS : 581-600. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-10373-5_30 | Abstract: | In this work, we study model checking of compositional real-time systems. A system is modeled using mutable data variables as well as a compositional timed process. Instead of explicitly manipulating clock variables, a number of compositional timed behavioral patterns are used to capture quantitative timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. A fully automated abstraction technique is developed to build an abstract finite state machine from the model. The idea is to dynamically create/delete clocks, and maintain/ solve a constraint on the clocks. The abstract machine weakly bi-simulates the model and, therefore, LTL model checking or trace-refinement checking are sound and complete. We enhance our home-grown PAT model checker with the technique and show its usability via the verification of benchmark systems. © Springer-Verlag Berlin Heidelberg 2009. | Source Title: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | URI: | http://scholarbank.nus.edu.sg/handle/10635/40018 | ISBN: | 3642103723 | ISSN: | 03029743 | DOI: | 10.1007/978-3-642-10373-5_30 |
Appears in Collections: | Staff Publications |
Show full item record
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.