Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
7-2008
Abstract
Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, not a trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit on-the-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, Nanjing, China, June 17-19
First Page
1
Last Page
8
ISBN
978-0-7695-3249-3
Identifier
10.1109/TASE.2008.12
Publisher
IEEE
City or Country
Nanjing, China
Citation
SUN, Jun; LIU, Yang; DONG, Jin Song; and SUN, Jing.
Bounded model checking of compositional processes. (2008). Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, Nanjing, China, June 17-19. 1-8.
Available at: https://ink.library.smu.edu.sg/sis_research/5051
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1109/TASE.2008.12