2008 23rd IEEE/ACM International Conference on Automated Software Engineering (2008)
Sept. 15, 2008 to Sept. 19, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASE.2008.22
M. Pradella , IEIIT Consiglio Naz. delle Ric., Milan
In bounded model checking (BMC) a system is modeled with a finite automaton and various desired properties with temporal logic formulae. Property verification is achieved by translation into boolean logic and the application of SAT-solvers. bounded satisfiability checking (BSC) adopts a similar approach, but both the system and the properties are modeled with temporal logic formulae, without an underlying operational model. Hence, BSC supports a higher-level, descriptive approach to system specification and analysis. We compare the performance of BMC and BSC over a set of case studies, using the Zot tool to translate automata and temporal logic formulae into boolean logic. We also propose a method to check whether an operational model is a correct implementation (refinement) of a temporal logic model, and assess its effectiveness on the same set of case studies. Our experimental results show the feasibility of BSC and refinement checking, with modest performance loss w.r.t. BMC.
Zot tool, real-time system specifications, bounded model checking, satisfiability checking, finite automaton, temporal logic formulae, property verification
P. San Pietro, M. Pradella and A. Morzenti, "Refining Real-Time System Specifications through Bounded Model- and Satisfiability-Checking," 2008 23rd IEEE/ACM International Conference on Automated Software Engineering(ASE), L'Aquila, 2008, pp. 119-127.