Author :
Power, Christopher ; Miller, Alice
Author_Institution :
Dept. of Comput. Sci., Univ. of Glasgow, Glasgow
Abstract :
The Prism model checker facilitates the formal modelling and analysis of systems that exhibit random or probabilistic behaviour. Prism lacks the provision of methods for specification debugging. To help alleviate this problem, we present a tool Prism2Promela for translating Prism into Promela. Once in this form, the SPIN model checker can be used to identify errors in the Promela specification, which can be traced back to corresponding errors in the original Prism specification.
Keywords :
probability; program debugging; program verification; Prism model checker; Prism2Promela; Promela specification; Spin model checker; formal modelling; probabilistic behaviour; specification debugging; Context modeling; Debugging; Error correction; Formal verification; Mirrors; Power system modeling; Stochastic systems; System recovery; Prism; Spin; Verification; model checking;
Conference_Titel :
Quantitative Evaluation of Systems, 2008. QEST '08. Fifth International Conference on
Conference_Location :
St. Malo
Print_ISBN :
978-0-7695-3360-5
DOI :
10.1109/QEST.2008.20
