Return to search

Formal Modelling of Cruise Control System Using Event-B and Rodin Platform

no / 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. / Romanian National Authority for Scientific Research, CNCS-UEFISCDI, project number PN-III-P4-ID-PCE-20160210.

Identiferoai:union.ndltd.org:BRADFORD/oai:bradscholars.brad.ac.uk:10454/16555
Date28 June 2018
CreatorsPredut, S., Ipate, F., Gheorghe, Marian, Campean, Felician
Source SetsBradford Scholars
LanguageEnglish
Detected LanguageEnglish
TypeConference paper, No full-text in the repository
Relationhttps://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8605812

Page generated in 0.0024 seconds