Sciweavers

TASE
2008
IEEE

Bounded Model Checking of Compositional Processes

13 years 9 months ago
Bounded Model Checking of Compositional Processes
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-theart 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.
Jun Sun 0001, Yang Liu 0003, Jin Song Dong, Jing S
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TASE
Authors Jun Sun 0001, Yang Liu 0003, Jin Song Dong, Jing Sun
Comments (0)