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

• Type: Conference
• Year: 2007
• Where: FSEN
• Authors: Domenico Bianculli, Paola Spoletini, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro
• Keywords: Descriptive Trio Specifications, FSEN 2007, Model Checking Trio, Software Engineering, TRIO Specifications