Formal Development Method of Automated Systems using the Temporal Logic of Actions TLA - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2006

Formal Development Method of Automated Systems using the Temporal Logic of Actions TLA

Résumé

The paper presents a method for control systems formal development. We focus on the refinement process used for the development of a control part controlling an operative part of an automated (controlled) system satisfying requirements. We first build an abstract model of both operative and control parts and complete this model to get a model of the automated system. The next steps consists in refining the control part and the operative one to get a model of the automated system capturing every important feature. The method is developed through a case study : a parcel sorting system. We use the temporal logic of actions TLA+ which deals with refiement and proved usufull for the specification and the verifiation of safety and liveness properties.
Fichier principal
Vignette du fichier
Mosbahi_MOSIM06.pdf (368.93 Ko) Télécharger le fichier

Dates et versions

inria-00102229 , version 1 (29-09-2006)

Identifiants

  • HAL Id : inria-00102229 , version 1

Citer

Olfa Mosbahi, Leila Jemni Ben Ayed, Jacques Jaray. Formal Development Method of Automated Systems using the Temporal Logic of Actions TLA. MOSIM'06 6ième Conférence Francophone de Modélisation et Simulation des Systèmes, Apr 2006, Rabat, Morocco. ⟨inria-00102229⟩
126 Consultations
92 Téléchargements

Partager

Gmail Facebook X LinkedIn More