Formal Modelling of Cruise Control System Using Event-B and Rodin Platform
dc.contributor.author | Predut, S. | * |
dc.contributor.author | Ipate, F. | * |
dc.contributor.author | Gheorghe, Marian | * |
dc.contributor.author | Campean, Felician | * |
dc.date.accessioned | 2018-08-28T15:24:45Z | |
dc.date.available | 2018-08-28T15:24:45Z | |
dc.date.issued | 2018-06-28 | |
dc.identifier.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. | en_US |
dc.identifier.uri | http://hdl.handle.net/10454/16555 | |
dc.description | no | en_US |
dc.description.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. | en_US |
dc.description.sponsorship | Romanian National Authority for Scientific Research, CNCS-UEFISCDI, project number PN-III-P4-ID-PCE-20160210. | en_US |
dc.language.iso | en | en_US |
dc.relation.isreferencedby | https://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8605812 | |
dc.subject | Event-B | en_US |
dc.subject | Formal verification | en_US |
dc.subject | Formal validation | en_US |
dc.subject | ProB | en_US |
dc.subject | Visualization | en_US |
dc.subject | iUML-B | en_US |
dc.subject | Cruise control system | en_US |
dc.subject | Hybrid propulsion vehicle | en_US |
dc.subject | Electric bicycle (e-Bike) | en_US |
dc.subject | Formal modelling | en_US |
dc.title | Formal Modelling of Cruise Control System Using Event-B and Rodin Platform | en_US |
dc.status.refereed | Yes | en_US |
dc.type | Conference paper | en_US |
dc.type.version | No full-text in the repository | en_US |
refterms.dateFOA | 2018-08-28T15:24:58Z |