@article{singh_use_2017,
	title = {Use of {Tabular} {Expressions} for {Refinement} {Automation}},
	url = {https://core.ac.uk/display/265386784?recSetID=},
	doi = {10/ghwgbz},
	abstract = {International audienceOur 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)},
	language = {en-gb},
	urldate = {2021-01-28},
	author = {Singh, Neeraj Kumar and Lawford, Mark and Maibaum, Thomas S. E. and Wassyng, Alan},
	year = {2017},
}

{"_id":"ex2idBKvvNrttq7Tz","bibbaseid":"singh-lawford-maibaum-wassyng-useoftabularexpressionsforrefinementautomation-2017","author_short":["Singh, N. K.","Lawford, M.","Maibaum, T. S. E.","Wassyng, A."],"bibdata":{"bibtype":"article","type":"article","title":"Use of Tabular Expressions for Refinement Automation","url":"https://core.ac.uk/display/265386784?recSetID=","doi":"10/ghwgbz","abstract":"International audienceOur 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)","language":"en-gb","urldate":"2021-01-28","author":[{"propositions":[],"lastnames":["Singh"],"firstnames":["Neeraj","Kumar"],"suffixes":[]},{"propositions":[],"lastnames":["Lawford"],"firstnames":["Mark"],"suffixes":[]},{"propositions":[],"lastnames":["Maibaum"],"firstnames":["Thomas","S.","E."],"suffixes":[]},{"propositions":[],"lastnames":["Wassyng"],"firstnames":["Alan"],"suffixes":[]}],"year":"2017","bibtex":"@article{singh_use_2017,\n\ttitle = {Use of {Tabular} {Expressions} for {Refinement} {Automation}},\n\turl = {https://core.ac.uk/display/265386784?recSetID=},\n\tdoi = {10/ghwgbz},\n\tabstract = {International audienceOur 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)},\n\tlanguage = {en-gb},\n\turldate = {2021-01-28},\n\tauthor = {Singh, Neeraj Kumar and Lawford, Mark and Maibaum, Thomas S. E. and Wassyng, Alan},\n\tyear = {2017},\n}\n\n","author_short":["Singh, N. K.","Lawford, M.","Maibaum, T. S. E.","Wassyng, A."],"key":"singh_use_2017","id":"singh_use_2017","bibbaseid":"singh-lawford-maibaum-wassyng-useoftabularexpressionsforrefinementautomation-2017","role":"author","urls":{"Paper":"https://core.ac.uk/display/265386784?recSetID="},"metadata":{"authorlinks":{}},"html":""},"bibtype":"article","biburl":"https://bibbase.org/zotero/SilverSylvester","dataSources":["YCBcQPneB9oxahSnp"],"keywords":[],"search_terms":["use","tabular","expressions","refinement","automation","singh","lawford","maibaum","wassyng"],"title":"Use of Tabular Expressions for Refinement Automation","year":2017}