Use of Tabular Expressions for Refinement Automation

Neeraj Kumar Singh (1, 2) , Mark Lawford (3) , Thomas S. E. Maibaum (3) , Alan Wassyng (3)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 Toulouse INP - Institut National Polytechnique (Toulouse)
3 McMaster University [Hamilton, Ontario]

Our interest is in the development of comprehensive and sound techniques to automate the task of 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 are 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 is 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).

Mots clés: Tabular expression; Event-B; Refinement; Formal methods; Verification; Validation; Insulin Infusion Pump

Domaines: Informatique et langage [cs.CL]

Neeraj Kumar Singh, Mark Lawford, Thomas S. E. Maibaum, Alan Wassyng. Use of Tabular Expressions for Refinement Automation. MEDI 2017 - Model and Data Engineering - 7th International Conference, Oct 2017, Barcelona, Spain. pp.167-182. ⟨hal-02353273⟩