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

Abstract : 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.
Type de document :
Communication dans un congrès
MOSIM'06 6ième Conférence Francophone de Modélisation et Simulation des Systèmes, Apr 2006, Rabat, Morocco. 2006
Liste complète des métadonnées

https://hal.inria.fr/inria-00102229
Contributeur : Jacques Jaray <>
Soumis le : vendredi 29 septembre 2006 - 14:59:59
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : mardi 6 avril 2010 - 01:17:45

Identifiants

  • HAL Id : inria-00102229, version 1

Collections

Citation

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. 2006. 〈inria-00102229〉

Partager

Métriques

Consultations de la notice

305

Téléchargements de fichiers

108