Download PDFOpen PDF in browser

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

EasyChair Preprint no. 2599

10 pagesDate: February 7, 2020


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: control system, Eclipse IDE, Event-B, Event-B Modeling, Formal Modeling, Industry Automation, Proof obligation, RODIN tool, Water pump controller

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  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 no. 2599},

  year = {EasyChair, 2020}}
Download PDFOpen PDF in browser