Browsing Engineering and Informatics by Subject "iUML-B"
Now showing items 1-1 of 1
Formal Modelling of Cruise Control System Using Event-B and Rodin PlatformFormal modelling is essential for precisely deﬁning, understanding and reasoning when designing complex systems, such as cyberphysical systems. In this paper we present a formal speciﬁcation 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 speciﬁcation and veriﬁcation, being supported by the Rodin platform, based on theorem proving, allowing a stepwise speciﬁcation process based on reﬁnement. We also use, from the same platform, the ProB model checker for the veriﬁcation of the B-Machine and iUML plug-in to visualize our model. This approach shows the beneﬁts of using a formal modelling platform, in the context of cyberphysical systems, which provides multiple ways of analysing a system.