Event-B Based Formal Modeling of a Controller: A Case Study
Event-B is an event-driven approach for system development. It has the flexibility to develop different discrete control systems. Event-B is a refinement-based step-by-step modeling methodology. There is a well-tested open-source tool available for Event-
- PDF / 338,032 Bytes
- 10 Pages / 439.37 x 666.142 pts Page_size
- 28 Downloads / 193 Views
Abstract Event-B is an event-driven approach for system development. It has the flexibility to develop different discrete control systems. Event-B is a refinementbased step-by-step modeling methodology. There is a well-tested open-source tool available for Event-B model checking, formalization of mathematical proofs and system validation is done in RODIN. This paper presents a short survey on the usage of an Event-B-based model to locate the research gaps followed by a case study to build a model using the 2-stage refinement strategy to stop the precious groundwater wastage and conserve it. We try to model the behavior required for the environment of the system. The proposed controller then controls the environment. The controller acts accordingly and achieves the goal of groundwater conservation. Keywords Formal modeling · Event-B · RODIN tool · Industry automation · Eclipse IDE · Water pump controller · Groundwater conservation
1 Introduction Event-B [1] is a modeling language and its application range is versatile. Not only a sequential program to distributed systems but it also has the privilege to model different control systems. Event-B models the environment which is the necessity to assure the correctness of the proposed systems [2]. The Event-B-based formal modeling proposed by Abrial [1] is a top-down engineering approach consisting of the step-by-step refinement strategy. The designers, therefore, design the refinement R. Karmakar (B) The University of Burdwan, Burdwan, India e-mail: [email protected]; [email protected] B. B. Sarkar Techno International, Rajarhat, Kolkata, India e-mail: [email protected] N. Chaki University of Calcutta, Kolkata, India e-mail: [email protected] © Springer Nature Singapore Pte Ltd. 2021 D. Bhattacharjee et al. (eds.), Proceedings of International Conference on Frontiers in Computing and Systems, Advances in Intelligent Systems and Computing 1255, https://doi.org/10.1007/978-981-15-7834-2_60
649
650
R. Karmakar et al.
strategies to meet the system requirements and specifications. A model in EventB consists of two components—context and machine. Context is the static part of a model. It contains all the constants, axioms, sets, and theorems that remain unaffected at any state of a machine. The machine describes a whole model. It sees the context and also contains the dynamic part consisting of variables, invariants, theorems, and events. The dynamic part is affected when an event has occurred (i.e. when the state of a machine is changed). An event consists of a set of actions, guards, and parameters. The axioms are the predicates made-of constants, and the invariants are the predicates made-of variables (and constants). The refinement can be done by imposing features one-by-one to an abstract model. Thus, we can find a set of refined models. At the final refinement, the model has all the desired features. The context of one model can be extended to the context of another model. When a machine (concrete machine) refines another machine (abstract machi
Data Loading...
