OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Stepwise Formal Modelling and Reasoning of Insulin Infusion Pump Requirements

Singh, Neeraj Kumar and Wang, Hao and Lawford, Mark and Maibaum, Thomas S. E. and Wassyng, Alan Stepwise Formal Modelling and Reasoning of Insulin Infusion Pump Requirements. (2015) In: Digital Human Modeling - Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health - 6th International Conference (DHM 2015), 2 August 2015 - 7 August 2015 (Los Angeles, United States).

(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-21070-4_39


An insulin infusion pump (IIP) is a critical software-intensive medical device that infuses insulin satisfying patient needs under safety and timing constraints that are appropriate for the treatment of diabetes. This device is used by millions of people around the world. The USA Food and Drug Administration (FDA) has reported several recalls in which IIP failures were responsible for a large number of serious illnesses and deaths. The failures responsible for this harm to people who are dependent on external insulin were caused by the introduction of hardware or software design errors during the system development process. This paper presents an incremental proof-based development of an IIP. We use the Event-B modelling language to formalize the given system requirements. Further, the Rodin proof tools are used to verify the correctness of functional behaviour, internal consistency checking with respect to safety properties, invariants and events.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-02354182
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Other partners > Aalesund University College (NORWAY)
Other partners > McMaster University (CANADA)
Laboratory name:
Deposited On:07 Nov 2019 14:59

Repository Staff Only: item control page