Download PDFOpen PDF in browser

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

EasyChair Preprint 2599

10 pagesDate: February 7, 2020

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@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}}
Download PDFOpen PDF in browser