Title: Translating STATEMATE models into FNLOG for the verification of safety requirements in reactive systems

Authors: Leila Jemni Ben Ayed, Yousra Hlaoui Ben Daly

Addresses: Research Unit of Technologies of Information and Communication (UTIC), Higher School of Sciences and Technologies of Tunis (ESSTT) 5, Avenue Taha Hussein, B.P.: 56, Bab Menara, 1008 Tunis, Tunisia. ' Research Unit of Technologies of Information and Communication (UTIC), Higher School of Sciences and Technologies of Tunis (ESSTT) 5, Avenue Taha Hussein, B.P.: 56, Bab Menara, 1008 Tunis, Tunisia

Abstract: In this paper, the authors explore the usefulness of a combination of semi-formal and formal methods in specifying reactive systems and verifying their properties. The authors propose an approach combining STATEMATE and the temporal logic FNLOG. STATEMATE is a semi-formal method, which has been used for the development of large industrial applications. It pertains to the specification and design of complex reactive systems and builds simulations and prototypes rapidly. Though STATEMATE provides rigorous specifications, these are not verifiable to ensure and guarantee the reliability of the system being developed. To fulfil the verification objective, a STATEMATE specification is translated into a logic based specification language FNLOG, which allows its verification. This paper describes the cross reference between STATEMATE and FNLOG features. Systematic derivation schemes from STATEMATE models to FNLOG specifications and different steps of the proposed translation procedure.

Keywords: STATEMATE; FNLOG; safety requirements; specifications; translation; verification; reactive systems; temporal logic; simulation.

DOI: 10.1504/IJITST.2009.023907

International Journal of Internet Technology and Secured Transactions, 2009 Vol.1 No.3/4, pp.236 - 271

Published online: 18 Mar 2009 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article