Skip to Main content Skip to Navigation
Conference papers

Une technique de spécification et de validation basée sur STATEMATE et FNLOG.

Résumé : Le papier présente une technique de spécification et de validation empruntant les avantages de deux classes de méthodes de spécification, formelles et semi-formelles. Il s'inscrit dans le cadre d'intégration de méthodes pour la spécification des systèmes critiques Temps réels sûrs de fonctionnement. La technique que nous présentons utilise STATEMATE comme méthode semi -formelle et la logique temporelle FNLOG comme méthode formelle. La technique proposée présente une démarche d'intégration employant les notations de STATEMATE et de FNLOG. Elle définit des règles de transformation d'une spécification STATEMATE en des formules FNLOG et étend l'axiomatique de la logique temporelle FNLOG par de nouveaux lemmes pour prendre en compte les propriétés temporelles de durée. Le papier présente les différentes étapes de la démarche proposée, les règles de transformation ainsi que l'extension axiomatique.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00000809
Contributor : Mohamed Khalgui <>
Submitted on : Monday, November 21, 2005 - 11:37:39 AM
Last modification on : Wednesday, October 28, 2020 - 2:20:03 PM

Identifiers

  • HAL Id : inria-00000809, version 1

Citation

Leila Jemni Ben Ayed, Olfa Mosbahi, Samir Ben Ahmed. Une technique de spécification et de validation basée sur STATEMATE et FNLOG.. Quatrième conférence francophone de Modélisation et Simulation - MOSIM'03, Apr 2003, Toulouse, France. ⟨inria-00000809⟩

Share

Metrics

Record views

77