ABSTRACT
CONTENTS 9.1 Introduction 200 9.2 Preliminaries 202
9.2.1 Requirements Engineering 202 9.2.2 CRT Pacemaker 202 9.2.3 Denition of the NBG Code 203 9.2.4 Event-B 203
9.3 Environment Modeling (The Heart) 204 9.3.1 Heart Block 208
9.3.1.1 SA Block 208 9.3.1.2 AV Block 208 9.3.1.3 Infra-Hisian Block 208 9.3.1.4 Left Bundle Branch Block 208 9.3.1.5 Right Bundle Branch Block 208
9.3.2 Cellular Automata Model 209 9.4 CRT Pacemaker Control Requirements 211 9.5 Closed-Loop Model of the CRT Pacemaker and Heart 214
9.5.1 Abstract Model 214 9.5.2 First Renement: Impulse Propagation and Timing
Requirements 217 9.5.3 Second Renement: Threshold and Heart Blocks 221 9.5.4 Third Renement: Refractory and Blanking Periods and a Cellular
Model 224 9.5.5 Model Validation and Analysis 229
9.6 Discussion 230
9.7 Related Work 231 9.8 Conclusion 232 References 233
Trustworthy-cyber physical systems (TCPS) are safety-critical systems, in whichfailures can lead to injuries and loss of life. These systems demand strong integration and coordination among the computing sciences, network communication, and physical modeling. Analyzing systems requirements is a major challenge in the area of safety-critical software, where requirements quality is also an important issue in building a dependable cyber-physical system. Most projects fail due to a lack of understanding of user needs, inadequate knowledge of the system’s environment, and inconsistent system specications. This combination typically results in poor systems requirements. Since software plays such an important role in critical systems embedded in a physical environment, it is essential that we trace unidentied and hidden requirements by validating and checking the consistency of the systems requirements. To this end, formal methods that model the closed-loop system are invaluable. In this chapter, we present an incremental proof-based development of a closed-loop model of the Cardiac Resynchronization Therapy (CRT) and heart. We analyze the prime benets of a closed-loop modeling approach in requirements engineering to validate the appropriateness and correctness of system behaviors in the early stage of systems development, including new research directions.
