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

fYear

2007

fDate

20-26 May 2007

Firstpage

61

Lastpage

62

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering - Companion, 2007. ICSE 2007 Companion. 29th International Conference on

Conference_Location

Minneapolis, MN

Print_ISBN

0-7695-2892-9

Type

conf

DOI

10.1109/ICSECOMPANION.2007.79

Filename

4222681