DocumentCode
3175621
Title
Yet Another Model Checker for PROMELA - The Transformation Approach
Author
Zhao, WenDi
Author_Institution
Sch. of Comput., Nat. Univ. of Singapore, Singapore, Singapore
fYear
2010
fDate
9-11 June 2010
Firstpage
137
Lastpage
142
Abstract
Automated verification plays vital roles on concurrent system design. PROMELA, as a popular system description language, has been widely used for this purpose. PROMELA models can be analyzed with the SPIN model checker, which is, however, deficient with respect to perform verification under strong fairness. In this work, we represent a translator that can translate PROMELA models into CSP# models automatically, which can be analyzed and be verified under strong fairness using PAT.
Keywords
program verification; simulation languages; PAT; Promela; SPIN model checker; automated verification; concurrent system design; description language; Algebra; Automata; Computer bugs; Computer languages; Concurrent computing; Performance analysis; Protocols; Real time systems; Software systems; System testing; PAT; PROMELA; model checking;
fLanguage
English
Publisher
ieee
Conference_Titel
Secure Software Integration and Reliability Improvement Companion (SSIRI-C), 2010 Fourth International Conference on
Conference_Location
Singapore
Print_ISBN
978-1-4244-7644-2
Type
conf
DOI
10.1109/SSIRI-C.2010.38
Filename
5521572
Link To Document