Formal Modelling of Cruise Control System Using Event-B and Rodin Platform
| Autor: | Felician Campean, Florentin Ipate, Sorina-Nicoleta Predut, Marian Gheorghe |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Model checking
0209 industrial biotechnology Computer science Process (engineering) Event (computing) business.industry B-Method 0211 other engineering and technologies Context (language use) 02 engineering and technology Automated theorem proving 020901 industrial engineering & automation Formal specification Software engineering business Cruise control 021106 design practice & management |
| Zdroj: | HPCC/SmartCity/DSS |
| DOI: | 10.1109/hpcc/smartcity/dss.2018.00253 |
| Popis: | Formal modelling is essential for precisely defining, understanding and reasoning when designing complex systems, such as cyberphysical systems. In this paper we present a formal specification using Event-B and Rodin platform for a case study of a cruise control system for a hybrid propulsion vehicle and electric bicycle (e-Bike). Our work uses the Event- B method, a formal approach for reliable systems specification and verification, being supported by the Rodin platform, based on theorem proving, allowing a stepwise specification process based on refinement. We also use, from the same platform, the ProB model checker for the verification of the B-Machine and iUML plug-in to visualize our model. This approach shows the benefits of using a formal modelling platform, in the context of cyberphysical systems, which provides multiple ways of analysing a system. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|