Sciweavers

Share
FM
2003
Springer

Model-Checking TRIO Specifications in SPIN

10 years 3 months ago
Model-Checking TRIO Specifications in SPIN
We present a novel application on model checking through SPIN as a means for verifying purely descriptive specifications written in TRIO, a first order, linear-time temporal logic with both future and past operators and a quantitative metric on time. The approach is based on the translation of TRIO formulas into Promela programs guided by an equivalence between TRIO and 2-way alternating Büchi automata. An optimization technique based on the concept of modularized TRIO specifications is also shown. The results of our experimentation are quite encouraging, as we are able to verify properties of the Railway Crossing Problem, a well-known benchmark used in the Formal Methods community, for values of the temporal constants that make the verification totally infeasible with traditional tools and approaches.
Angelo Morzenti, Matteo Pradella, Pierluigi San Pi
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where FM
Authors Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro, Paola Spoletini
Comments (0)
books