OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Use of Tabular Expressions for Refinement Automation

Singh, Neeraj Kumar and Lawford, Mark and Maibaum, Thomas S. E. and Wassyng, Alan Use of Tabular Expressions for Refinement Automation. (2017) In: MEDI 2017 - Model and Data Engineering - 7th International Conference, 4 October 2017 - 6 October 2017 (Barcelona, Spain).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/978-3-319-66854-3\_13


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).

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-02353273
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > McMaster University (CANADA)
Laboratory name:
Deposited On:07 Nov 2019 10:34

Repository Staff Only: item control page