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

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00102229
Contributor : Jacques Jaray Connect in order to contact the contributor
Submitted on : Friday, September 29, 2006 - 2:59:59 PM
Last modification on : Friday, February 4, 2022 - 3:30:21 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 1:17:45 AM

Identifiers

  • 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. ⟨inria-00102229⟩

Share

Metrics

Record views

126

Files downloads

82