Loading...
Formal Modelling of Cruise Control System Using Event-B and Rodin Platform
Predut, S. Ipate, F. Gheorghe, Marian
Predut, S.
Ipate, F.
Gheorghe, Marian
Publication Date
2018-06-28
End of Embargo
Supervisor
Rights
Peer-Reviewed
Yes
Open Access status
Accepted for publication
Institution
Department
Awarded
Embargo end date
Additional title
Abstract
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 EventB 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.
Version
No full-text in the repository
Citation
Predut S, Ipate F, Gheorghe M and Campean IF (2018) Formal Modelling of Cruise Control System Using Event-B and Rodin Platform. [Proceedings of the] 2018 IEEE 20th International Conference on High Performance Computing and Communications; IEEE 16th International Conference on Smart City; IEEE 4th International Conference on Data Science and Systems. IEEE. ISBN: 978-1-5386-6614-2.
Link to publisher’s version
Link to published version
Link to Version of Record
Type
Conference paper