|
| This Article | ||
| | ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
29th International Conference on Software Engineering (ICSE'07 Companion)
Minneapolis, Minnesota
May 20-May 26
ISBN: 0-7695-2892-9
| 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 - | |||
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.