NDLI: Poster abstract: Formal analysis of fresenius infusion pump (FIP)

Content Provider	IEEE Xplore Digital Library
Author	Sfyrla, V. Marcoux, S. Vittoria, C.
Copyright Year	2013
Description	Author affiliation: Le Grand Chemin, Fresenius Vial, Brezins, France (Marcoux, S.; Vittoria, C.) \|\| Objet Direct, Grenoble, France (Sfyrla, V.)
Abstract	Summary form only given. Today's medical devices are based on embedded architecture, with software used to control the underlying hardware. They are highly critical since errors in the software can endanger end users such as patients and medics. Medical devices should be designed and manufactured in such a way that when used, they perform as intended and they ensure a high level of safety. Current industrial practices are based on testing processes to check if the software meets the specifications and if it fulfills its purpose. However, testing does have several disadvantages that limit the reliability of this verification and validation process. Testing cannot guarantee that a device will function properly under all conditions and bugs can never be completely identified withing a program. Several attempts have already been made to provide standards for the formal verification of safety properties of medical devices, initiated by the Generic Infusion Pump project [2]. Our work is a collaboration between Objet Direct R&D and Fresenius [1]. Fresenius is a leading international health care group which produces and markets pharmaceuticals and medical devices. We aim to investigate innovative methods for software development, validation and verification. We study existing results provided amongst others by [3, 4] which we intend to extend by analyzing the Fresenius Infusion Pump (FIP) software. FIP automatizes the delivery process of fluid medical solution into patient's body. Its design is based on three layers. The highest level is the user interface and consists of three components, the administration protocol, the application system and the power management. The middle level consists of the pumping control components and the lowest level contains driver components such as Door, Watchdog, Optical Disk, Motor. FIP is modeled in UML (a total of 100 state machines) and the requirements are written in natural language. The implementation of the model is done in C++ with automatic code generation. For the V&V process, software testing checks if the implementation meets the requirements using fault scenarios written in UML. The main objective of this project is to use model-based design for migrating from software testing to formal based solution for verifying the Fresenius Infusion Pump. The goal is to use model checking technologies in order to verify requirements and eliminate bugs during the design process. Several faulty design patterns have already been identified to be caused by deadlocks, lost signal events, stack overflow, violation of real-time properties, incoherent behavior of UML state machines. We present and analyze the case study of the FIP's Motor component, a driver component of the lowest level. Its interest lies on the fact that while the Motor Control is stopped, the Motor Driver is still running. This faulty behavior was detected during the test checks and bug was partially corrected in code review.
Starting Page	253
Ending Page	253
File Size	52507
Page Count	1
File Format	PDF
ISBN	9781450319966
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2013-04-08
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Association for Computing Machinery, Inc. (ACM)
Subject Keyword	Unified modeling language Computer bugs Pumps Medical services Software Safety Testing
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Formal analysis of Fresenius infusion pump (FIP)

Architectural specification for infusion pumps and realization towards safety technological trends

A panacea or academic poppycock: formal methods revisited

Specifying and Checking Refinement Relationships in VDM++

Formal Methods Based Development of a PCA Infusion Pump Reference Model: Generic Infusion Pump (GIP) Project

Automating Software FMEA via Formal Analysis of Dependence Relations

Generation of Conformance Test Suites for Compositions of Web Services Using Model Checking

Specifying constraints with message sequence specifications

Efficient Modelling of Embedded Software Systems and their Formal Verification

Poster abstract: Formal analysis of fresenius infusion pump (FIP)

Similar Documents

Formal analysis of Fresenius infusion pump (FIP)

Architectural specification for infusion pumps and realization towards safety technological trends

A panacea or academic poppycock: formal methods revisited

Specifying and Checking Refinement Relationships in VDM++

Formal Methods Based Development of a PCA Infusion Pump Reference Model: Generic Infusion Pump (GIP) Project

Automating Software FMEA via Formal Analysis of Dependence Relations

Generation of Conformance Test Suites for Compositions of Web Services Using Model Checking

Specifying constraints with message sequence specifications

Efficient Modelling of Embedded Software Systems and their Formal Verification

Poster abstract: Formal analysis of fresenius infusion pump (FIP)