UML/event-B-based modelling and verification of the car cruise control system
by Hemza Merouani; Fateh Boutekkouk; Imad Merouani
International Journal of Computer Aided Engineering and Technology (IJCAET), Vol. 16, No. 1, 2022

Abstract: Method B, as well as its Event-B extension is a formal method used for the development of computer systems whose accuracy must be formally established. Event B development is an incremental specification of multiple machines/contexts. It starts with an abstract mathematical specification of the system and ends with the corresponding computer code. A great asset of Event-B is the Rodin platform, which is based on Eclipse and can be extended with plug-ins. The iUML-B plug-in is the combination of the UML notation and the Event-B method. It allows generating an Event-B code automatically from two views: static (class diagrams) and dynamic (state/transition diagram). The functional view is not taken into account by Rodin. To remedy this problem, we propose a flow of specification and formal verification based on the UML notation and the Event B. This flow is carried out by successive refinement starting from a very abstract specification and purely functional based on the UML case diagram. To validate our approach, we applied our flow to the car cruise controller system.

Online publication date: Thu, 09-Dec-2021

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Computer Aided Engineering and Technology (IJCAET):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com