Please use this identifier to cite or link to this item:
https://doi.org/10.1007/978-3-642-10373-5_30
DC Field | Value | |
---|---|---|
dc.title | Verifying stateful timed CSP using implicit clocks and zone abstraction | |
dc.contributor.author | Sun, J. | |
dc.contributor.author | Liu, Y. | |
dc.contributor.author | Dong, J.S. | |
dc.contributor.author | Zhang, X. | |
dc.date.accessioned | 2013-07-04T07:54:49Z | |
dc.date.available | 2013-07-04T07:54:49Z | |
dc.date.issued | 2009 | |
dc.identifier.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. <a href="https://doi.org/10.1007/978-3-642-10373-5_30" target="_blank">https://doi.org/10.1007/978-3-642-10373-5_30</a> | |
dc.identifier.isbn | 3642103723 | |
dc.identifier.issn | 03029743 | |
dc.identifier.uri | http://scholarbank.nus.edu.sg/handle/10635/40018 | |
dc.description.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. | |
dc.description.uri | http://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1007/978-3-642-10373-5_30 | |
dc.source | Scopus | |
dc.type | Conference Paper | |
dc.contributor.department | COMPUTER SCIENCE | |
dc.description.doi | 10.1007/978-3-642-10373-5_30 | |
dc.description.sourcetitle | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | |
dc.description.volume | 5885 LNCS | |
dc.description.page | 581-600 | |
dc.identifier.isiut | NOT_IN_WOS | |
Appears in Collections: | Staff Publications |
Show simple 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.