Use of Tabular Expressions for Refinement Automation

We aim to develop sound and effective techniques to automate formal modelling and refinement from tabular expressions using a correct-by-construction approach. In this work, we present a refinement strategy to generate formal models from tabular expressions, as they can be used in the Event-B modelling paradigm. The proposed refinement strategy permits us to develop an abstract model using tabular expressions and a series of Event-B models using refinement from the set of tabular expressions. Further the proofs associated with the refinement strategy used to generate the model are examined through the Rodin tools. Our work is an important step towards eliciting patterns of automatic refinement for Event-B models from tabular expressions and to meet the properties of completeness and disjointness in a rigorous manner. To assess the effectiveness of our proposed approach, we use a medical device case study: the Insulin Infusion Pump (IIP).