DocumentCode :
1643374
Title :
Efficient Model Checking of PSL Safety Properties
Author :
Launiainen, Tuomas ; Heljanko, Keijo ; Junttila, Tommi
Author_Institution :
Dept. of Inf. & Comput. Sci., Aalto Univ., Aalto, Finland
fYear :
2010
Firstpage :
95
Lastpage :
104
Abstract :
Safety properties are an important class of properties as in the industrial use of model checking a large majority of the properties to be checked are safety properties. This work presents an efficient approach to model check safety properties expressed in PSL (IEEE Std 1850 Property Specification Language), an industrial property specification language. The approach can also be used as a sound but incomplete bug hunting tool for general(non-safety) PSL properties, and it will detect exactly the finite counterexamples that are the informative bad prefixes for the PSL formulas in question. The presented technique is inspired by the temporal testers approach of Pnueli and co-authors but is aimed at finite words instead of infinite words. The new approach presented in this paper handles a larger syntactic subset of PSL safety properties than earlier translations for PSL safety subsets and has been implemented on top of the open source NuSMV 2model checker. The experimental results show the approach to be a quite competitive model checking approach when compared to a state-of-the-art implementation of PSL model checking.
Keywords :
program verification; specification languages; NuSMV 2 model checker; PSL safety properties; bug hunting tool; efficient model checking; finite counterexamples; property specification language; Data structures; Input variables; Observers; Safety; Semantics; Syntactics; Transducers; NuSMV; PSL; model checking; safety properties;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Application of Concurrency to System Design (ACSD), 2010 10th International Conference on
Conference_Location :
Braga
ISSN :
1550-4808
Print_ISBN :
978-1-4244-7266-6
Electronic_ISBN :
1550-4808
Type :
conf
DOI :
10.1109/ACSD.2010.27
Filename :
5552685
Link To Document :
بازگشت