A Specification and Validation Technique Based on STATEMATE and FNLOG

Olfa Mosbahi 1 Leila Jemni Ben Ayed 1 Samir Ben Ahmed 1 Jacques Jaray 2
1 LIP2 - Laboratoire d'Informatique, de Parallélisme et de Productique
2 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The paper presents a specification technique borrowing features from an formal and a semi-formal methods each in order to cover all features needed in the development of real-time and critical systems. The work is a contribution to the integration of formal and semi-formal methodsn namely STATEMATE and the temporal logic FNLOG [7]. FNLOG deals with quantitative temporal properties and is compatible with STATEMATE. The proposed integration approach uses the notations of STATEMATE and FNLOG, defines a various transformations rules of a STATEMATE specification towards FNLOG and extends the axiomatic of the temporal logic FNLOG by new lemmas to deal with duration properties. The paper presents the various steps of our integration approach.
Keywords : Verification. Formal methods Integration Real-time Systems Semi Formal methods Specification Temporal logic Validation Verification
Type de document :
Communication dans un congrès
Chris George and Huaikou Miao. 4th International Conference on Formal Engineering Methods - ICFEM 2002, Oct 2002, Shanghai, China. Springer - Verlag GmbH, 2495, pp.216-220, 2002, Lecture Notes in Computer Science. 〈10.1007/3-540-36103-0_23〉
Liste complète des métadonnées

Littérature citée [4 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00102167
Contributeur : Jacques Jaray <>
Soumis le : vendredi 29 septembre 2006 - 11:53:04
Dernière modification le : mardi 24 avril 2018 - 13:29:21
Document(s) archivé(s) le : mardi 6 avril 2010 - 01:17:16

Fichier

Mosbahi_ICFEM02.pdf

Identifiants

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Olfa Mosbahi, Leila Jemni Ben Ayed, Samir Ben Ahmed, Jacques Jaray. A Specification and Validation Technique Based on STATEMATE and FNLOG. Chris George and Huaikou Miao. 4th International Conference on Formal Engineering Methods - ICFEM 2002, Oct 2002, Shanghai, China. Springer - Verlag GmbH, 2495, pp.216-220, 2002, Lecture Notes in Computer Science. 〈10.1007/3-540-36103-0_23〉. 〈inria-00102167〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

605

Téléchargements de fichiers

291

Contact


archive-ouverte@inria.fr