Cyber-Physical System Design from an Architecture Analysis Viewpoint (eBook)

Editors: Shin Nakajima is a professor at the National Institute of Informatics (NII) and also a professor at the Graduate University for Advanced Studies (SOKENDAI). His research interests include formal methods, automated verification, and software testing. Jean-Pierre Talpin is a senior research associate (directeur de recherche) with Inria and leads Inria project-team TEA (time, events and architectures).  His research background ranges from type theory, programming languages, concurrency theory, code generation, scheduling, and verification to proof.  His current research interests include the component-based design, analysis, verification, and integration of cyber-physical systems. Masumi Toyoshima is a research project manager at DENSO Corporation. His research background includes design of distributed computing systems and recent interest is Systems Engineering. Huafeng Yu is a senior researcher with Boeing Research & Technology. He serves on IEEE Technical Committee on for Cyber-Physical Systems. His research interests include mobile autonomous systems, software architecture and safety, model-based engineering, and software certification.

Preface 5
Acknowledgements 8
Contents 9
Contributors 10
1 Virtual Prototyping of Embedded Systems: Speed and Accuracy Tradeoffs 12
1.1 Introduction 12
1.2 Virtual Prototyping 13
1.3 Simulation Abstractions 17
1.3.1 Functional Abstraction 20
1.3.2 Time Abstraction 21
1.4 Computation Abstraction 23
1.4.1 Instruction Set Simulation 24
1.4.2 Source-Level and Host-Compiled Simulation 29
1.5 Communication Abstraction 32
1.5.1 Transaction-Level Modeling 33
1.5.2 Memory Simulation 34
1.5.3 Interrupts 36
1.5.4 Peripherals 36
1.6 Summary and Conclusions 37
References 38
2 Model-Based Design and Automated Validation of ARINC653 Architectures Using the AADL 43
2.1 Introduction 44
2.2 Boeing 777 ADIRU Case Study 45
2.3 AADL and Patterns for IMA System 46
2.3.1 The AADL Core Language 46
2.3.2 Modeling Integrated Modular Architectures with AADL 49
2.3.3 The AADL ARINC653 Annex 50
2.3.4 ADIRU Full Model 54
2.4 Model-Based Assurance with AADL 54
2.4.1 Validation of AADL Models 55
2.4.2 Application to ARINC653 Requirements 56
2.5 Safety Analysis 57
2.6 From Model to Code 58
2.7 Conclusion and Future Work 60
References 61
3 Formal Semantics of Behavior Specifications in the Architecture Analysis and Design Language Standard 63
3.1 Introduction 63
3.2 Example of an Adaptive Cruise Control System 64
3.3 Architecture Analysis and Design Language 66
3.3.1 Architecture 66
3.3.2 Properties 68
3.3.3 AADL Timing Execution Model 68
3.4 A Formalization Using Constrained Automata 69
3.4.1 Vocabulary 69
3.4.2 Formulas 70
3.4.3 Model 70
3.4.4 Automaton 71
3.4.5 Properties 72
3.4.6 Product 72
3.4.7 Small Step 73
3.4.8 Big Step 73
3.4.9 Synchronous and Asynchronous Trace 74
3.4.10 Timed Step and Timed Trace 74
3.5 Behavior Annex Model 74
3.5.1 Formalization 75
3.5.2 Transition System 75
3.5.3 Behavior Conditions 80
3.5.4 Action Language 82
3.5.5 Communication Actions 84
3.5.6 Expression Language 85
3.5.7 Synchronization Protocols 85
3.6 Related Work 86
3.7 Conclusion 88
References 88
4 MARTE for CPS and CPSoS 90
4.1 Introduction 90
4.1.1 CPS and CPSoS 90
4.1.2 Role of UML and Its Extensions 93
4.1.3 Outline 94
4.2 Overview of MARTE 94
4.2.1 Overview 94
4.2.2 Foundations 94
4.2.3 Non-functional Properties 95
4.2.4 Time 97
4.2.5 Allocation 98
4.2.6 Design and Analysis in MARTE 99
4.3 MARTE for CPS 100
4.3.1 Case Study: Quadcopter 100
4.3.2 Proposed Extensions: Mixed-Criticality, Design-Space Exploration 103
4.4 Tooling 107
4.4.1 State-of-the-Art 107
4.4.2 Single-Source Design from MARTE 108
4.5 Forecast About the Role MARTE May Have in Designing CPS 111
4.5.1 The End of Moore's Law 111
4.5.2 The Rise of Connected Ubiquitous Smart Objects 112
4.6 Conclusion 114
References 115
5 Combined Model Checking and Testing Create Confidence---A Case on Commercial Automotive Operating System 118
5.1 Introduction 119
5.2 OSEK/VDX Operating Systems 120
5.3 Approach 122
5.3.1 Design Model 122
5.3.2 Design Verification and Environment Modelling 123
5.3.3 Testing 124
5.4 Related Works 126
5.5 Design Model and Verification 127
5.5.1 Construction of Design Model 127
5.5.2 Environment Modelling 129
5.5.3 Approximation of Environments 129
5.5.4 Verification Result 131
5.6 Testing Based on Design Model 132
5.6.1 Generation of Test Cases and Programs 132
5.6.2 Test Models 133
5.6.3 Test Cases and Test Programs 134
5.6.4 Test Results 136
5.7 Discussion 137
5.7.1 Practical Applications of Model Checking 137
5.7.2 Verification Results 138
5.7.3 Meaning of Testing 139
5.7.4 Creating the Confidence in Correctness 139
5.8 Conclusion 140
References 140
6 Formal Methods for Aerospace Systems 142
6.1 Introduction 143
6.2 Space Systems Engineering 144
6.3 Achievements 145
6.3.1 The COMPASS Approach 145
6.3.2 System Modelling 147
6.3.3 Requirements Specification 148
6.3.4 COMPASS Toolset 149
6.3.5 Case Studies 158
6.4 Challenges 159
6.4.1 Formal Validation of Probabilistic Properties 159
6.4.2 Contract-Based Fault Injection 160
6.4.3 FDIR Design and Diagnosability 160
6.4.4 Timed Failure Propagation Graphs 161
6.4.5 Parametric Error Models 161
6.4.6 Dynamic Fault Trees 162
6.4.7 Multi-objective Verification 163
6.5 Conclusion 164
References 165