First lessons on the specification of a landing-system in Event-B

Autor: Jacquot, Jean-Pierre
Přispěvatelé: Development of specifications (DEDALE), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Jazyk: francouzština
Rok vydání: 2016
Předmět:
Zdroj: Revue des Sciences et Technologies de l'Information-Série TSI : Technique et Science Informatiques
Revue des Sciences et Technologies de l'Information-Série TSI : Technique et Science Informatiques, Lavoisier, 2016, 34 (5), pp.549-573. ⟨10.3166/TSI.34.547-571⟩
Revue des Sciences et Technologies de l'Information-Série TSI : Technique et Science Informatiques, 2016, 34 (5), pp.549-573. ⟨10.3166/TSI.34.547-571⟩
ISSN: 0752-4072
2116-5920
DOI: 10.3166/TSI.34.547-571⟩
Popis: International audience; This article presents the preliminary lessons gained from developing in Event-B the case-study proposed for the ABZ2014 conference. The case is the modeling of the software control for the landing-gears system of a plane. The use of Event-B for this case-study raises interesting questions such as the nature of the invariants, the moment when they are introduced, as well as the expression and verification of the functional properties. The refinement chain is organized in observation levels structured following the hardware description. The system is seen as an automaton controled by external sensors. Describing such a system in Event-B is simple but validating it is much more difficult. This activity relies on JeB, a simulator for EventB in JavaScript. Emulating the sensors is a crucial issue.; Cet article présente les leçons préliminaires obtenues en traitant en B Événementiel l’étude de cas proposée par la conférence ABZ 2014. Le problème consiste à modéliser le logi- ciel de contrôle du train d’atterrissage d’un avion. L’utilisation de B Évémentiel sur cette étude pose des questions intéressantes quant à la nature des invariants, au moment de leur introduc- tion, ainsi qu’à l’expression et la vérification des propriétés fonctionnelles. Le raffinement est organisé en niveaux d’observation structurés par la description du matériel. Le système est vu comme un automate piloté par des capteurs externes. La description d’un tel système en B Évé- nementiel est simple mais sa validation est beaucoup plus difficile. Cette étape utilise JeB, un simulateur de B Événementiel en JavaScript. L’émulation des capteurs est un point crucial.
Databáze: OpenAIRE
Externí odkaz: