Sciweavers

FSEN
2007
Springer

Model Checking Temporal Metric Specifications with Trio2Promela

13 years 7 months ago
Model Checking Temporal Metric Specifications with Trio2Promela
Abstract. We present Trio2Promela, a tool for model checking TRIO specifications by means of Spin. TRIO is a linear-time temporal logic with both future and past operators and a quantitative metric on time. Our approach is based on the translation of TRIO formulae into Promela programs guided by equivalence between TRIO and alternating B
Domenico Bianculli, Paola Spoletini, Angelo Morzen
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2007
Where FSEN
Authors Domenico Bianculli, Paola Spoletini, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro
Comments (0)