(Downloads - 0)
For more info about our services contact : help@bestpfe.com
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
