Développement formel de systèmes automatisés

Abstract : This thesis deals with the development of automated systems while following the formal methods B and TLA+. We propose a formal methodology based on the refinement paradigm to specify and verify the system that we model by two components: the controlled system representing the physical device and its environment, and the controller that controls the system. A synchronised product on the actions of these two components is applied to specify the automated system. As a first contribution, we propose an approach combining the event B method and the language TLA+ in order to verify liveness properties defined in user requirements. Inspired by the temporal logic of actions TLA, we first extend the event B notation to specify liveness properties and we give semantics of this extended syntax over traces. Second, we give transformation rules from a temporal B model into a TLA+ module. We present, in particular, our prototype system called B2TLA+, that we have developed to support this transformation. To consider infinite systems, we use predicate diagrams as abstractions of systems modelled with TLA+. To consider the real-time concept in automated systems, we propose as a second contribution a technique explicitly representing time in B event systems. This technique is based on an interleaving between any event handling time and the other system events. By considering the well known co-design technique, we propose as a third contribution a refinement-based composition technique keeping a separation between controller and controlled systems in order to build correct automated systems satisfying user requirements. We prove a compositionality theorem with respect to refinement to get an efficient approach to verify the refinement of a synchronized composition between components. We verify the refinement of a synchronized composition by verifying separately the refinement of each component. Finally, we define, prove and use in a case study as a fourth contribution the concept of a refinement pattern for continuous processes in manufacturing systems. Such proven pattern allows us to use the discrete abstraction of the effect of continuous processes operating for a while
Document type :
Theses
Complete list of metadatas

Cited literature [111 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01748685
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 11:46:14 AM
Last modification on : Tuesday, April 24, 2018 - 1:31:00 PM
Long-term archiving on : Friday, September 14, 2018 - 7:54:07 AM

File

2008_MOSBAHI_O.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01748685, version 1

Collections

Citation

Olfa Mosbahi-Khalgui. Développement formel de systèmes automatisés. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2008. Français. ⟨NNT : 2008INPL007N⟩. ⟨tel-01748685⟩

Share

Metrics

Record views

36

Files downloads

32