HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Integrating FNLLOG and STATEMATE for the Specification and Validation of Real Time Systems

Abstract : Summary form only given, as follows. We present a specification technique borrowing features from two classes of specification methods, formal and semiformal ones. Each of the above methods have been proved to be useful in the development of real-time and critical systems and widely reported in different papers. Formal methods are based on mathematical notations and axiomatic which induce verification and validation. Semiformal methods are, in the other hand, graphic, structural and user-friendly. Each method is applied on a suitable case study, that we regret some missing features we could find in the other class. This remark has motivated our work. We are interested in the integration of formal and semiformal methods in order to lay out a specification approach which combines the advantages of these two classes of methods. The proposed technique is based on the integration of the semiformal method STATEMATE and the temporal logic FNLOG. This choice is justified by the fact that FNLOG is formal, deals with quantitative temporal properties and that these two approaches have a compatibility which simplifies their integration. The proposed integration approach uses the notations of STATEMATE and FNLOG, defines various transformation rules of a STATEMATE specification towards FNLOG and extends the axiomatics of the temporal logic FNLOG by new lemmas to deal with duration properties. We present the various steps of our integration approach, the proposed extentions and illustrates it over a case of critical real-time systems: the gas burner system.
Document type :
Conference papers
Complete list of metadata

Contributor : Mohamed Khalgui Connect in order to contact the contributor
Submitted on : Monday, November 21, 2005 - 11:40:43 AM
Last modification on : Wednesday, October 28, 2020 - 2:20:03 PM



Olfa Mosbahi, Leila Jemni Ben Ayed, Samir Ben Ahmed. Integrating FNLLOG and STATEMATE for the Specification and Validation of Real Time Systems. ACS/IEEE International Conference on Computer Systems and Applications - AICCSA'03, Jul 2003, Tunis, Tunisia. ⟨10.1109/AICCSA.2003.1227447⟩. ⟨inria-00000810⟩



Record views