Title :
Trio2Promela: A Model Checker for Temporal Metric Specifications
Author :
Bianculli, Domenico ; Morzenti, Angelo ; Pradella, Matteo ; Pietro, Pierluigi San ; Spoletini, Paola
Author_Institution :
Fac. of Inf., Lugano Univ., Lugano
Abstract :
We present Trio2Promela, a tool for model checking metric temporal logic specifications written in the TRIO language. Our approach is based on the translation of formulae into Promela programs for the model checker Spin, guided by equivalence between temporal logic and alternating Bilchi automata. Trio2Promela may be used also to check satisfiability of temporal logic specifications (a distinguishing difference with other model checking tools).
Keywords :
automata theory; computability; formal specification; program verification; temporal logic; Bilchi automata; Promela program; Spin model checker; TRIO language; Trio2Promela model checker; formal verification; formulae translation; metric temporal logic specification; satisfiability checking; Automata; Automatic logic units; Computer networks; Counting circuits; Informatics; Performance analysis; Plastics; Real time systems; Software engineering;
Conference_Titel :
Software Engineering - Companion, 2007. ICSE 2007 Companion. 29th International Conference on
Conference_Location :
Minneapolis, MN
Print_ISBN :
0-7695-2892-9
DOI :
10.1109/ICSECOMPANION.2007.79
