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 <>
Submitted on : Friday, September 29, 2006 - 2:59:59 PM
Last modification on : Friday, February 26, 2021 - 3:28:04 PM
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

432

Files downloads

243