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.
| Identifer | oai:union.ndltd.org:BRADFORD/oai:bradscholars.brad.ac.uk:10454/16555 |
| Date | 28 June 2018 |
| Creators | Predut, S., Ipate, F., Gheorghe, Marian, Campean, Felician |
| Source Sets | Bradford Scholars |
| Language | English |
| Detected Language | English |
| Type | Conference paper, No full-text in the repository |
| Relation | https://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8605812 |
Page generated in 0.0028 seconds