Modeling of a speed control system using Event-B
| Autor: | Mammar, Amel, Frappier, Marc |
|---|---|
| Přispěvatelé: | Département Informatique (INF), Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP), Institut Polytechnique de Paris (IP Paris), Méthodes et modèles pour les réseaux (METHODES-SAMOVAR), Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux (SAMOVAR), Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP)-Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP), Groupe de recherche en informatique fondamentale de l'Université de Sherbrooke (GRIF), Université de Sherbrooke (UdeS) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Computer science
Speed limit Verification 020207 software engineering Control engineering 02 engineering and technology [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Refinement Article Set (abstract data type) Control theory Position (vector) 020204 information systems 0202 electrical engineering electronic engineering information engineering Key (cryptography) Event-B method Point (geometry) State (computer science) Actuator Speed control system |
| Zdroj: | Rigorous State-Based Methods: 7th International Conference, ABZ 2020, Ulm, Germany, May 27–29, 2020, Proceedings ABZ 2020: 7th international conference on Rigorous State-Based Methods ABZ 2020: 7th international conference on Rigorous State-Based Methods, May 2020, Ulm, Germany. pp.367-381, ⟨10.1007/978-3-030-48077-6_29⟩ Rigorous State-Based Methods ISBN: 9783030480769 ABZ Rigorous State-Based Methods |
| DOI: | 10.1007/978-3-030-48077-6_29⟩ |
| Popis: | International audience; The present paper presents our proposal of an Event-B model of a speed control system, a part of the case study provided in the ABZ2020 conference. The case study describes how the system regulates the current speed of a car according to a set criteria like the speed desired by the driver, the position of a possible preceding vehicle but also a given speed limit that the driver must not exceed. For that purpose, this controller reads different information form the available sensors (key state, desired speed, etc.) and takes the adequate actions by acting on the actuators of the car’s speed according to the read information. To formally model this system, we adopt a stepwise refinement approach with the Event-B method. We consider most features of the case study, all proof obligations have been discharged using the Rodin provers. Our model has been validated using ProB by applying the different provided scenarios. This validation has permitted us to point out and correct some mistakes, ambiguities and oversights contained in the first versions of the case study. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|