loading...
Trio2Promela: A Model Checker for Temporal Metric Specifications
Minneapolis, Minnesota May 20-May 26
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICSECOMPANION.2007.7929th International Conference on Soft ...
 This Article 
 
PURCHASE ARTICLE: $0
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Domenico Bianculli, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro, Paola Spoletini, "Trio2Promela: A Model Checker for Temporal Metric Specifications," International Conference on Software Engineering Companion, pp. 61-62, 29th International Conference on Software Engineering (ICSE'07 Companion), 2007.
 
 
BibTex
x
 
@article{ 10.1109/ICSECOMPANION.2007.79,
author = {Domenico Bianculli and Angelo Morzenti and Matteo Pradella and Pierluigi San Pietro and Paola Spoletini},
title = {Trio2Promela: A Model Checker for Temporal Metric Specifications},
journal ={International Conference on Software Engineering Companion},
volume = {0},
year = {2007},
isbn = {0-7695-2892-9},
pages = {61-62},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICSECOMPANION.2007.79},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - International Conference on Software Engineering Companion
TI - Trio2Promela: A Model Checker for Temporal Metric Specifications
SN - 0-7695-2892-9
SP61
EP62
A1 - Domenico Bianculli,
A1 - Angelo Morzenti,
A1 - Matteo Pradella,
A1 - Pierluigi San Pietro,
A1 - Paola Spoletini,
PY - 2007
KW - null
VL - 0
JA - International Conference on Software Engineering Companion
ER -
 
Domenico Bianculli, University of Lugano, Switzerland
Angelo Morzenti, Politecnico di Milano, Italy
Matteo Pradella, CNR IEIIT-MI, Italy
Pierluigi San Pietro, Politecnico di Milano, Italy
Paola Spoletini, Politecnico di Milano, Italy
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 B?uchi automata. Trio2Promela may be used also to check satisfiability of temporal logic specifications (a distinguishing difference with other model checking tools).
Citation:
Domenico Bianculli, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro, Paola Spoletini, "Trio2Promela: A Model Checker for Temporal Metric Specifications," icsecompanion, pp.61-62, 29th International Conference on Software Engineering (ICSE'07 Companion), 2007
Usage of this product signifies your acceptance of the Terms of Use.


Suggestions