Electrocardiogram (ECG) Interpretation Protocol using Formal Methods 

Get Complete Project Material File(s) Now! »

Software in Safety-critical Systems

Software is a vital part of any system, especially in embedded systems, where it is used to control the whole functionality of the systems. The embedded systems have major role to control the behavior of the safety critical systems. When we use these systems, we con-sider that their risk has been minimized and uses of the systems are effectively safe. The system is not only safe, but we also expect other attributes like reliable and cost effective. Main safety-critical systems are commercial aircraft, medical care, train signaling systems, air traffic control, nuclear power, and weapons, where any kind of failure can quickly lead to human life in danger, loss of equipment, and so on. The industries are responsible for designing and delivering the safety-critical systems according to the standards authori-ties [ISO ; IEEE-SA ; CC ; FDA ], which satisfy the requirements.
To address the problem of system’s failure related to the software errors for exam-ple, overdoses from Therac-25 for treating cancer through radiation [Leveson 1993], the overshooting of the runway at Warsaw airport by an Airbus A320 [Commission 1994], Intel Pentium floating point divide [Price 1995], 5000 adverse events for Insulin Infusion Pump(IIP) reported by FDA [Zhang 2010; Xu 2011] and Ariane 5 flight 501 going off [72]. All these problems and many more are considered as a part of the “software crisis”. The term “software crisis” has been introduced in late 1960s to describe the failures of the sys-tem in which software-development problems cause the entire system [Gibbs 1994]. In 1968, a meeting is organized by NATO related to the software crisis. This crisis had as its root cause the problem of complexity brought about in many cases by sheer length of pro-grams combined with a poor control over how each line of code affects the overall system. Almost three decades later, this problem still remains as indicated in [Gibbs 1994].
Software crisis is a well-known problem for other engineering disciplines, and over the years of experience has been accumulated to provide effective solutions: the technology has been available, and it has been shown to work with a very high degree of confidence. Software is using frequently in the system development, which is also classified as an en-gineering discipline, so it would seem natural that one can apply the insights and quickly surmount any hurdles. However, it is true that the engineering insights are applicable to modern the critical-system development to come over the traditional approach of the sys-tem development.

Safety Standards

It is perhaps best to start by considering the various standards that exist for industries, which develop the safety critical systems. Standards are documented agreements containing tech-nical specifications, which produce precise criteria, consistent rules, procedures to ensure reliability, software processes, methods, products, services and use of products, are fit for their purpose in this world. Standards include a set of issues corresponding to the product functionality and compatibility, facilitate interoperability including designing, developing, enhancing, and maintaining. A set of protocols and guidelines, which are produced by the standards, are consistent and universally acceptable for the product development. The standards allow to understand the quality of different products for competing with them and provide a way to verify the credibility of a new product [ISO ; IEEE-SA ].
Verification and validation (V & V) are part of the certification process for any critical system. There are several reasons, why certification is required for any critical system. For example, medical device like a cardiac pacemaker must obtain a certificate before im-plantation. Certification of the product not only assures about the safety, but also helps to a customer to gain confidence to buy and to use the product, which is also important for com-mercial reasons like having a sales advantage to industry. Certifications are usually carried out by some national and international authorities. Certification can be applicable to an organization, tools or methods, or systems or products. Main objectives of the certification bodies for providing assurance that the organization achieves a certain level of proficiency, and that they agree to the certain standards or criteria. In the case of product certification, there are always issues for the certification, whether a methodology or development process is certified or not.
There is a wide variety of standards bodies. More than 300 software standards and 50 organizations are developing software standards [Fries C. 2011]. Standards come in many different flavours, for example, de-facto standards, local, national and international stan-dards. Some of the standards are more specific related to the defense, financial, medical, nuclear, and transportation etcetera (See in Appendix-A).
There are number of standards addressing safety and security of a system related to the software development. For example, avionics RTCA-Do-178B [RTCA 1992] or the IEC 61508 [IEC61508 2008; Gall 2008] as the fundamental standard for the functional safety of E/E/EP systems [IEC61508 2008; Gall 2008]. The IEC 62304 [IEC62304 2006] standard is for the software life-cycles of medical device development, which addresses to achieve more specific goals through standard process activity, and helps to design the safe systems. All necessary requirements for each life cycle process are provided by the IEC 62304. The process standard IEC 62304 [IEC62304 2006] is a collection of two other standards ISO 14791 and ISO 13485, where the ISO 14791 standard is for quality, and the ISO 13485 is for risk management.
The Institute of Electrical and Electronics Engineers (IEEE) standards [IEEE-SA ] pro-vides a safety assurance level for industries, including: power and energy, biomedical and health care, information technology, transportation, nanotechnology, telecommunication, information assurance, and many more. The IEEE standard is approved by authority and considers the users recommendations before apply into the development process. All these standards are reviewed at least every five years to qualify the new amendments in the sys-tems.
The Food and Drug Administration (FDA) [Keatley 1999] is established by US De-partment of Health and Human Services (HHS) in 1930 for regulating the various kinds of product like food, cosmetics, medical devices, etcetera. The FDA is now using stan-dards in the regulatory review process to provide a safety to the public before using any product. The FDA provides some guidelines on the recognition to use of and consensus standards. The FDA is interested in standards because they can help to serve as a com-mon yardstick to assist with mutual recognition, based on the signed Mutual Recognition Agreement between the European Union and United States. The FDA standard classifies the medical devices based on risk and the use of medical devices. The FDA provides some standard guidelines for the medical devices, and the medical devices have required to meet these standards. Time to time lots of amendments have been done in the FDA stan-dards [FDA ; Keatley 1999] according to the use of medical devices to provide a safety.
Common Criteria (CC) [CC ] is an international standard that allows an evaluation of security for the IT products and technology. The CC is an international standard (ISO/IEC 15408) [ISO ] for computer security certification. CC is a collection of existing criteria: Eu-ropean (Information Technology Security Evaluation Criteria)(ITSEC)), US (Trusted Com-puter Security Evaluation Criteria (TCSEC)) and Canadian (Canadian Trusted Computer Product Evaluation Criteria (CTCPEC)) [CC 2009a; CC 2009b; CC 2009c]. The Common Criteria enable an objective evaluation to validate that a particular product or system satis-fies a defined set of security requirements. The CC provides a framework for the computer users, vendors and testing organizations for fulfill their requirements and assures that the process of specification, implementation and testing of the product has been conducted in a rigorous and standard manner.
There are several ways to tackle the complexity issues of software, which major the software at industrial scales and usability of the softwares. The Software Engineering Insti-tute, funded by the military, has produced a Capability Maturity Model (CMM) [Paulk 1995] by which may be assessed the quality of management in a software engineering team. The CMM broadly refers to a process improvement approach that is based on a process model. A process model is a structured collection of practices that describe the characteristics of effective processes; the practices included are those proven by experience to be effective. The CMM can be used to assess an organization against a scale of five process maturity levels. Each level ranks the organization according to its standardization of processes in the subject area being assessed.

Traditional System Engineering Approach

A critical system uses a standard life-cycle to achieve a certificate from the standard au-thorities [IEEE-SA ; ISO ; FDA ; CC ]. A system can be considered safe if all hazards have been eliminated, or the risk associated hazards have been reduced to an acceptable level. Software is a part of the system, which is used within the system to operate the system safely. The integrated software within the system does not show any kind of misbehav-ior. However, if the same software is used by multiple systems then the software must have similar behavior in each system. However, sometimes it is not true. It is believed that each system is different, with different requirements, different risk level with different hazard’s characteristics, it is impossible to know if software is safe without considering the behaviour of the software as a part of the system which it is controlling. Therefore, when considering the process for developing a safe software, it is crucial that the whole system of which the software is a part is considered, as well as the software itself [Blanchard 2006]. In the following section, we review a typical safety-critical development process.

The Software Safety Life-cycle

In recognition of the distinctive nature of safety-related systems, there is a standard de-velopment process known as V-model, which is widely accepted by large companies and defense. It is an extension of the standard Waterfall model in engineers [Wichmann 1992; Bell 1993; Acuña 2005; Schumann 2001]. The V-model represents a software-development process, where the process steps are bent upwards after the coding phase to form the typical V shape. The V-model presents the relationships between each phase of the development life cycle and its associated phase of testing. V-model is also called verification and vali-dation model (V & V). This process uses a very intensive testing for removing the bug or error, which may appear during any stage of the system development.

Table of contents :

0 Présentation de la thèse en français 
0.1 Motivation
0.2 Approche
0.3 Contribution et vue générale de la thèse
0.3.1 Contribution
0.3.2 Vue générale de la thèse
0.4 Publications
0.5 Aperçu des chapitres
0.5.1 Etat de l’art
0.5.2 Modélisation avec Event-B
0.5.3 Méthodologie formellement fondée pour le développement de de systèmes critiques
0.5.4 Animateur Temps Réel et Traçabilité des Exigences
0.5.5 Chartes de raffinement
0.5.6 L’atelier EB2ALL: génération automatique des codes
0.5.7 Modélisation du fonctionnement du coeur
0.5.8 Etudes de cas
0.6 Conclusion et Perspectives
0.6.1 Contributions
0.6.2 Perspectives
1 Introduction 
1.1 Motivation
1.2 Approach
1.3 Contribution and Outline
1.3.1 Contribution
1.3.2 Thesis outline
1.4 Publications
2 State of the Art 
2.1 Introduction
2.2 Software in Safety-critical Systems
2.2.1 Safety Standards
2.3 Traditional System Engineering Approach
2.3.1 The Software Safety Life-cycle
2.3.2 Hazards Analysis
2.3.3 Risk Assessment and Safety Integrity
2.3.4 Safety Integrity and Assurance
2.4 Standard Design Methodologies in Development
2.5 Industrial Application of Formal Methods
2.5.1 IBM’s Customer Information Control System
2.5.2 The Central Control Function Display Information System (CDIS)
2.5.3 The Paris Métro Signaling System (SACEM)
2.5.4 The Traffic Collision Avoidance System (TCAS)
2.5.5 The Rockwell AAMP5 Microprocessor
2.5.6 The VIPER Microprocessor
2.5.7 The Mondex Electronic Purse
2.5.8 The BOS Control System
2.5.9 The Intelr CoreTM i7 Processor Execution Cluster
2.6 Formal Methods for Safety-critical systems
2.6.1 Why Formal Methods?
2.6.2 Motivation for their use
3 The Modeling Framework : Event-B 
3.1 Introduction
3.1.1 Overview of B
3.1.2 Proof-based Development
3.1.3 Scope of the B Modelling
3.1.4 Related Techniques
3.2 The Event-B Modelling Notation
3.2.1 Contexts
3.2.2 Machines
3.2.3 Modeling actions over states
3.2.4 Proof Obligations
3.2.5 Model refinement
3.2.6 Tools Environments for Event-B
I Techniques and Tools 
4 Critical System Development Methodology 
4.1 Introduction
4.2 Related Work
4.3 Overview of the Methodology
4.3.1 Informal Requirements
4.3.2 Formal Specification
4.3.3 Formal Verification
4.3.4 Formal Validation
4.3.5 Real-time Animation Phase
4.3.6 Code Generation
4.3.7 Acceptance Testing
4.4 Benefits of Using our Proposed Approach
4.4.1 Improving Requirements
4.4.2 Reducing Error Introduction
4.4.3 Improving Error Detection
4.4.4 Reducing Development Cost
4.5 Conclusion
5 Real-Time Animator and Requirements Traceability 
5.1 Introduction
5.2 Motivation
5.2.1 Traceability
5.3 Related Work
5.4 Animation
5.4.1 Benefits of Animation
5.4.2 Limitations of Animation
5.5 Proposed Architecture
5.5.1 Data acquisition & Preprocessing
5.5.2 Feature extraction
5.5.3 Database
5.5.4 Graphical animations tool: Macromedia Flash
5.5.5 Animator: Brama plug-in
5.5.6 Formal modeling Language: Event-B
5.6 Applications and Case Studies
5.7 Limitations
5.8 Conclusion
6 Refinement Chart 
6.1 Introduction
6.2 Related Work
6.3 Refinement Chart
6.4 Applications and Case Studies
6.5 Conclusion
7 EB2ALL : An Automatic Code Generator Tool 
7.1 Introduction
7.2 Related Work
7.3 A Basic Framework of Translator
7.3.1 Selection of a Rodin Project
7.3.2 Introduction of a Context File
7.3.2.1 Motivation
7.3.2.2 Selection of a Context File
7.3.2.3 Refinement using a new Context File
7.3.3 Generated Proof Obligations
7.3.4 Filter Context and Concrete machine Modules
7.3.5 Basic Principles of Code Generation
7.3.5.1 Process Context and Machine Files using Lexical and Syntax Analysis
7.3.5.2 Process Context Files
7.3.5.3 Mapping Event-B Constant Types to Programming Language
7.3.5.4 Process Machine Files
7.3.5.5 Mapping Event-B Variable Types to Programming Language
7.3.5.6 Mapping Event-B Events to Programming Language
7.3.6 Events Scheduling
7.3.7 External Code Injection and Code Verification
7.3.8 Compiling and Running the Code
7.4 How to use Code Generator plugins
7.4.1 Assessment of the Translation tool
7.5 Limitations
7.6 Conclusions
8 Formal Logic Based Heart-Model 
8.1 Introduction
8.1.1 Motivation
8.2 Related Work
8.3 Background
8.3.1 The Heart System
8.3.2 Basic overview of Electrocardiogram (ECG)
8.3.3 ECG Morphology
8.4 Proposed Idea
8.4.1 Heart Block
8.4.1.1 SA block:
8.4.1.2 AV block:
8.4.1.3 Infra-Hisian block:
8.4.1.4 Left bundle branch block:
8.4.1.5 Right bundle branch block:
8.4.2 Cellular Automata Model
8.5 Functional Formal Modeling of the Heart
8.5.1 The Context and Initial Model
8.5.2 Abstract Model
8.5.3 Refinement 1: Introducing Steps in the Propagation
8.5.4 Refinement 2: Impulse Propagation
8.5.5 Refinement 3: Perturbation the Conduction
8.5.6 Refinement 4: Getting a Cellular Model
8.5.7 Model Validation and Analysis
8.6 Discussion
8.7 Conclusion
II Case Studies 
9 The Cardiac Pacemaker 
9.1 Introduction
9.1.1 Why Model-Checker?
9.1.2 Related Work for the Cardiac Pacemaker
9.2 Basic Overview of Pacemaker system
9.2.1 The Heart System
9.2.2 The Pacemaker System
9.2.3 Bradycardia Operating Modes
9.3 Event-B Patterns for Modeling Cardiac Pacemaker
9.3.1 Action-Reaction Pattern
9.3.2 Time-based Pattern
9.4 Refinement Structure of a Cardiac Pacemaker
9.5 Development of the Cardiac Pacemaker using Refinement Chart
9.6 Formal development of the one-electrode cardiac pacemaker
9.6.1 Context and Initial Model
9.6.1.1 Abstraction of AOO and VOO modes:
9.6.1.2 Abstraction of AAI and VVI modes:
9.6.1.3 Abstraction of AAT and VVT modes:
9.6.2 First refinement: Threshold
9.6.3 Second refinement: Hysteresis
9.6.4 Third refinement: Rate Modulation
9.7 Formal Development of the Two-Electrode Cardiac Pacemaker
9.7.1 Context and Initial Model
9.7.1.1 Abstraction of DDD mode:
9.7.1.2 Abstraction of DVI mode:
9.7.1.3 Abstraction of DDI mode:
9.7.1.4 Abstraction of VDD mode:
9.7.1.5 Abstraction of DOO mode:
9.7.2 First refinement:Threshold
9.7.2.1 First refinement of DDD mode:
9.7.2.2 First refinement of DVI mode:
9.7.2.3 First refinement of DDI mode:
9.7.2.4 First refinement of VDD mode:
9.7.3 Second refinement of DDD mode: Hysteresis
9.7.4 Third refinement: Rate Modulation
9.8 Model Validation and Analysis
9.9 Closed-Loop Model (Heart & Cardiac Pacemaker)
9.9.1 Formal Development of The Cardiac Pacemaker
9.9.1.1 Abstract Model: Introducing, Pacing and Sensing Activities with Normal and Abnormal Heart Behavior
9.9.1.2 Refinement 1: Introducing threshold in Cardiac Pacemaker and Impulse Propagation in the Heart System
9.9.1.3 Refinement 2: Introduction of Hysteresis for cardiac pacemaker model and Perturbation the Conduction for the heart model
9.9.1.4 Refinement 3: Introduction of Rate Modulation for the Cardiac Pacemaker Model and a Cellular Model for the Heart system
9.10 Real-Time Animation Using Pacemaker Case Study
9.11 Code Generation for A Cardiac Pacemaker using EB2ALL Tool
9.12 Discussion and Conclusion
9.12.1 Discussion
9.12.2 Conclusion
10 Adaptive Cruise Control (ACC) 
10.1 Introduction
10.2 PID Controller
10.3 Overview of Methodology
10.4 Informal Description of ACC
10.4.1 Basic Components of ACC
10.4.2 Basic I/Os of ACC
10.5 Development of the ACC System using Refinement Chart
10.6 Formal development of the ACC
10.6.1 Abstraction of ACC system
10.6.2 First Refinement: State-flow Model
10.6.3 Second Refinement: Detailed modeling of State-flow
10.6.4 Third Refinement: Controller Definition
10.7 Model Validation and Analysis
10.8 Formal Specification into Simulink
10.9 Code Generation for ACC System using EB2ALL
10.10Discussion and Conclusion
10.10.1 Discussion
10.10.2 Conclusion
11 Electrocardiogram (ECG) Interpretation Protocol using Formal Methods 
11.1 Introduction
11.2 Related Work
11.3 Selection of Medical Protocol
11.4 Basic overview of Electrocardiogram (ECG)
11.4.1 Differentiating the P-, QRS- and T-waves
11.5 Formal Development of the ECG Interpretation
11.5.1 Abstract Model : Assessing Rhythm and Rate
11.5.2 Overview of the Full Refinement Chain
11.5.2.1 First Refinement : Assess Intervals and Blocks
11.5.2.2 Second Refinement : Assess for Nonspecific Intraventricular Conduction Delay andWolff-parkinson-white Syndrome
11.5.2.3 Third Refinement : Assess for ST-segment Elevation or Depression
11.5.2.4 Fourth Refinement : Assess for Pathologic Q-wave
11.5.2.5 Fifth Refinement : P-wave
11.5.2.6 Sixth Refinement : Assess for left and right ventricular hypertrophy
11.5.2.7 Seventh Refinement : Assess T-wave
11.5.2.8 Eighth Refinement : Assess Electrical Axis
11.5.2.9 Ninth Refinement: Assess for Miscellaneous Conditions
11.5.2.10 Tenth Refinement: Assess Arrhythmias
11.6 Statistical Analysis and Lesson Learned
11.6.1 Statistical Analysis
11.6.2 Lesson learned
11.6.2.1 Ambiguous
11.6.2.2 Inconsistencies
11.6.2.3 Incompleteness
11.7 Conclusion
12 Conclusion and Outlook
12.1 Contributions
12.2 Consequences and Future Challenges .

GET THE COMPLETE PROJECT