Preface xxiii
Contributors xxxv
Acknowledgments xxxix
Part I Models and Paradigms 1
1. Formal Verification Techniques for Digital Systems 3
Masahiro Fujita, Satoshi Komatsu, and Hiroshi Saito
1.1 Introduction 3
1.2 Basic Techniques for Formal Verification 4
1.3 Verification Techniques for Combinational Circuit Equivalence 7
1.4 Verification Techniques for Sequential Circuits 14
1.5 Summary 24
References 24
2. Tolerating Arbitrary Failures With State Machine Replication 27
Assia Doudou, Beno®t Garbinato, and Rachid Guerraoui
2.1 Introduction 27
2.2 System Model 31
2.3 Total Order Broadcast 32
2.4 Weak Interactive Consistency 36
2.5 Muteness Failure Detector 44
2.6 Concluding Remarks 52
References 55
3. Model-Based Evaluation as a Support to the Design of Dependable Systems 57
Andrea Bondavalli, Silvano Chiaradonna, and Felicita di Giandomenico
3.1 Introduction 57
3.2 The Role of Model-Based Evaluation in the Development of Dependable Systems 58
3.3 Dependability Modeling Methodologies and Tools 61
3.4 Analytical Modeling to Support Design Decisions 68
3.5 Analytical Modeling to Support Fault Removal During Operational Life 76
3.6 Summary 82
References 82
4. Voting: A Paradigm for Adjudication and Data Fusion in Dependable Systems 87
Behrooz Parhami
4.1 Introduction 87
4.2 Voting in Dependable Systems 88
4.3 Voting Schemes and Problems 94
4.4 Voting for Data Fusion 98
4.5 Implementation Issues 102
4.6 Unifying Concepts 107
4.7 Conclusion 110
References 111
5. Robust Communication Primitives for Wireless Sensor Networks 115
Amol Bakshi and Viktor K. Prasanna
5.1 Introduction 115
5.2 Defining Realistic Models 117
5.3 Our System Model 119
5.4 Permutation Routing in a Single-hop Topology: State-of-the-Art 121
5.5 An Energy-Efficient Protocol Using a Low-Power Control Channel 125
5.6 Our Routing Protocol for a Faulty Network 132
5.7 Our Generalized Protocol for a Multichannel Network 135
5.8 Concluding Remarks 140
References 140
6. System-Level Diagnosis and Implications in Current Context 143
Arun K. Somani
6.1 Issues in Large and Complex Computing Systems 143
6.2 System-Level Diagnosis 145
6.3 Classification of Diagnosable Systems 148
6.4 Diagnosability Algorithms 157
6.5 Diagnosis Algorithms 160
6.6 Application of System-Level Diagnosis Algorithm 165
6.7 Summary and Conclusions 166
References 167
7. Predicate Detection in Asynchronous Systems With Crash Failures 171
Felix C. G¤rtner and Stefan Pleisch
7.1 Introduction 171
7.2 Predicate Detection in Fault-Free Environments 173
7.3 Failures and Failure Detection 177
7.4 Predicate Detection in Faulty Environments 183
7.5 Solving Predicate Detection in Faulty Environments 194
7.6 Conclusion 209
References 211
8. Fault Tolerance Against Design Faults 213
Lorenzo Strigini
8.1 Introduction 213
8.2 Examples and Principles 215
8.3 Potential and Actual Benefits 225
8.4 Design Solutions 230
8.5 Summary 236
References 238
9. Formal Methods for Safety Critical Systems 243
Ali E. Abdallah, Jonathan P. Bowen, and Nimal Nissanke
9.1 Introduction 243
9.2 Specification of Safety 245
9.3 Historical Background 247
9.4 Safety 248
9.5 Application Areas 253
9.6 Specification Framework 256
9.7 System State and Behavior 262
9.8 Discussion 265
9.9 Conclusion 268
References 269
Part II Enabling Technologies and Applications 273
10. Dependability Support in Wireless Sensor Networks 275
Denis Gracanin, Mohamed Eltoweissy, Stephan Olariu, and Ashraf Wadaa
10.1 Motivation and Background 276
10.2 Service Centric Model 279
10.3 Conclusion 283
References 283
11. Availability Modeling in Practice 285
Kishor S. Trivedi, Archana Sathaye, and Srinivasan Ramani
11.1 Introduction 285
11.2 Modeling Approaches 286
11.3 Composite Availability and Performance Model 292
11.4 Digital Equipment Corporation Case Study 297
11.5 Conclusion 315
References 315
12. Experimental Dependability Evaluation 319
Jo£o Gabriel Silva and Henrique Madeira
12.1 Field Measurement 321
12.2 Fault Injection 323
12.3 Robustness Testing 337
12.4 Recent Developments: Dependability Benchmarking 340
12.5 Conclusion 342
References 343
13. A Dependable Architecture for Telemedicine in Support of Disaster Relief 349
Stephan Olariu, Kurt Maly, Edwin C. Foudriat, Sameh M. Yamany, and Thomas Luckenbach
13.1 Introduction 349
13.2 Telemedicineâ"State of the Art 350
13.3 The WIRM System Architecture 352
13.4 A Novel 3D Data Compression Technique 356
13.5 Interactive Remote Visualization 358
13.6 An Overview of H3Mâ"Our Wireless Architecture 359
13.7 Concluding Remarks 366
References 366
14. An Overview of IBM Mainframe Dependable Computing: From System/360 to Series 369
Lisa Spainhower
14.1 Introduction 369
14.2 Error Detection and Fault Isolation 375
14.3 Instruction Level Retry 380
14.4 Online Repair 386
14.5 Summary 391
References 392
15. Tracking the Propagation of Data Errors in Software 395
Martin Hiller, Arshad Jhumka, and Neeraj Suri
15.1 Introduction 395
15.2 Target System Model 396
15.3 Overview of the Tool Suite 397
15.4 Setup: Experiment Design and Target Instrumentation 401
15.5 Injection: Running Experiments 407
15.6 Analysis: Obtaining Error Propagation Characteristics 408
15.7 Example Results Generated by Propane 409
15.8 Propaneâs Attributes and Main Characteristics 414
15.9 Summary 415
References 416
16. Integrated Reliable Real-Time Systems 419
Mohamed Younis
16.1 Background 421
16.2 Integration Issues 425
16.3 Few Forward Steps 429
16.4 An Example Aerospace Application 432
16.5 Conclusion 442
References 443
17. Network Resilience by Emergent Behavior from Simple Autonomous Agents 449
Bjarne E. Helvik and Otto Wittner
17.1 Introduction 449
17.2 Network Resilience 450
17.3 Handling Routing and Resources in Networks by Emergence 457
17.4 Cross-Entropy Based Path Finding 460
17.5 Finding âBest-Effortâ Primary/Backup Paths 468
17.6 Discussion 473
17.7 Concluding Remarks 475
References 475
18. Safeguarding Critical Infrastructures 479
David Gamez, Simin Nadjm-Tehrani, John Bigham, Claudio Balducelli, Kalle Burbeck, and Tobias Chyssler
18.1 Introduction 479
18.2 Attacks, Failures, and Accidents 480
18.3 Solutions 483
18.4 The Safeguard Architecture 486
18.5 Future Work 497
18.6 Conclusion 497
References 498
19. Impact of Traffic Self-Similarity on the Performance of Routing Algorithms in Multicomputer Systems 501
Geyong Min, Mohamed Ould-Khaoua, Demetres D. Kouvatsos, and Irfan U. Awan
19.1 Introduction 502
19.2 The k-ary n-Cube and Dimension-Ordered Routing 504
19.3 Modeling of Traffic Self-Similarity 506
19.4 The Analytical Model 507
19.5 Impact of Self-Similar Traffic on Routing Performance 518
19.6 Conclusions 519
References 520
Appendix 19.1: Notation 523
20. Some Observations on Adaptive Meta-Heuristics for Routing in Datagram Networks 525
Albert Y. Zomaya, Tysun Chan, and Miro Kraetzl
20.1 Introduction 525
20.2 The Routing Problem 526
20.3 Genetic Algorithms and Routing 532
20.4 Genetic Routing Protocol Design 536
20.5 Genetic Routing Protocol Implementation 547
20.6 Results and Analysis 552
20.7 Conclusions 560
References 561
21. Reconfigurable Computing for Cryptography 563
Hassan B. Diab
21.1 Introduction 564
21.2 Reconfigurable Computing 565
21.3 AES Cryptography 576
21.4 Case Study: The Twofish Cipher on a Dynamic RC System 579
21.5 Future of RC 589
21.6 Conclusion 590
References 591
22. Dependability of Reconfigurable Computing 597
Mohamed Younis, I-Hong Yeh, Nicholas Kyriakopoulos, Nikitas Alexandridis, and Tarek El-Ghazawi
22.1 FPGA Preliminaries 598
22.2 FPGA Fault Taxonomy 603
22.3 Handling FPGA Failures 608
22.4 Conclusion and Open Issues 621
References 622
Index 627
