Article: UML/event-B-based modelling and verification of the car cruise control system Journal: International Journal of Computer Aided Engineering and Technology (IJCAET) 2022 Vol.16 No.1 pp.14 - 39 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. Inderscience Publishers - linking academia, business and industry through research

Title: UML/event-B-based modelling and verification of the car cruise control system

Authors: Hemza Merouani; Fateh Boutekkouk; Imad Merouani

Addresses: Laboratory of Research on Computer Science's Complex Systems, University of Oum El Bouaghi, PoB 358, 04000, Oum El Bouaghi, Algeria ' Laboratory of Research on Computer Science's Complex Systems, University of Oum El Bouaghi, PoB 358, 04000, Oum El Bouaghi, Algeria ' Laboratory of Research on Computer Science's Complex Systems, University of Oum El Bouaghi, PoB 358, 04000, Oum El Bouaghi, Algeria

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.

Keywords: intelligent cars; cruise control system; formal verification; Event-B; Rodin.

DOI: 10.1504/IJCAET.2022.119536

International Journal of Computer Aided Engineering and Technology, 2022 Vol.16 No.1, pp.14 - 39

Received: 04 Sep 2018
Accepted: 05 Mar 2019
Published online: 09 Dec 2021 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article

Title: UML/event-B-based modelling and verification of the car cruise control system

Keep up-to-date