Event-B Based Formal Modeling of a Controller: a Case Study

EasyChair Preprint 2599

Abstract

Event-B is an event-driven approach for system development. It has the flexibility to develop different discrete control systems. It is a modeling language over a wide range of application domain. It is a refinement based step by step modeling methodology, used to develop the model of the system incrementally. There is a well-tested open-source tool available for model B checking, formalization of mathematical proofs and system validation is RODIN. In this paper, we present a short survey on usage of Event-B based model to locate the research gaps followed by a case study to build a model using 2 stage refinement strategy of event B to stop the precious groundwater wastage and conserve it. We try to model the behavior required for the environment of the system. Our proposed controller then controls the environment. The controller acts accordingly and we achieve the goal of groundwater conservation.

Keyphrases: Eclipse IDE, Event-B, Event-B Modeling, Formal Modeling, Industry Automation, Proof obligation, RODIN tool, Water pump controller, control system

@booklet{EasyChair:2599,
  author    = {Rahul Karmakar and Bidyut Biman Sarkar and Nabendu Chaki},
  title     = {Event-B Based Formal Modeling of a Controller: a Case Study},
  howpublished = {EasyChair Preprint 2599},
  year      = {EasyChair, 2020}}