Linked e-resources
Details
Table of Contents
Preface; Acknowledgements; Contents; Contributors; 1 Virtual Prototyping of Embedded Systems: Speed and Accuracy Tradeoffs; 1.1 Introduction; 1.2 Virtual Prototyping; 1.3 Simulation Abstractions; 1.3.1 Functional Abstraction; 1.3.2 Time Abstraction; 1.4 Computation Abstraction; 1.4.1 Instruction Set Simulation; 1.4.2 Source-Level and Host-Compiled Simulation; 1.5 Communication Abstraction; 1.5.1 Transaction-Level Modeling; 1.5.2 Memory Simulation; 1.5.3 Interrupts; 1.5.4 Peripherals; 1.6 Summary and Conclusions; References
2 Model-Based Design and Automated Validation of ARINC653 Architectures Using the AADL2.1 Introduction; 2.2 Boeing 777 ADIRU Case Study; 2.3 AADL and Patterns for IMA System; 2.3.1 The AADL Core Language; 2.3.2 Modeling Integrated Modular Architectures with AADL; 2.3.3 The AADL ARINC653 Annex; 2.3.4 ADIRU Full Model; 2.4 Model-Based Assurance with AADL; 2.4.1 Validation of AADL Models; 2.4.2 Application to ARINC653 Requirements; 2.5 Safety Analysis; 2.6 From Model to Code; 2.7 Conclusion and Future Work; References
3 Formal Semantics of Behavior Specifications in the Architecture Analysis and Design Language Standard3.1 Introduction; 3.2 Example of an Adaptive Cruise Control System; 3.3 Architecture Analysis and Design Language; 3.3.1 Architecture; 3.3.2 Properties; 3.3.3 AADL Timing Execution Model; 3.4 A Formalization Using Constrained Automata; 3.4.1 Vocabulary; 3.4.2 Formulas; 3.4.3 Model; 3.4.4 Automaton; 3.4.5 Properties; 3.4.6 Product; 3.4.7 Small Step; 3.4.8 Big Step; 3.4.9 Synchronous and Asynchronous Trace; 3.4.10 Timed Step and Timed Trace; 3.5 Behavior Annex Model; 3.5.1 Formalization
3.5.2 Transition System3.5.3 Behavior Conditions; 3.5.4 Action Language; 3.5.5 Communication Actions; 3.5.6 Expression Language; 3.5.7 Synchronization Protocols; 3.6 Related Work; 3.7 Conclusion; References; 4 MARTE for CPS and CPSoS; 4.1 Introduction; 4.1.1 CPS and CPSoS; 4.1.2 Role of UML and Its Extensions; 4.1.3 Outline; 4.2 Overview of MARTE; 4.2.1 Overview; 4.2.2 Foundations; 4.2.3 Non-functional Properties; 4.2.4 Time; 4.2.5 Allocation; 4.2.6 Design and Analysis in MARTE; 4.3 MARTE for CPS; 4.3.1 Case Study: Quadcopter
4.3.2 Proposed Extensions: Mixed-Criticality, Design-Space Exploration4.4 Tooling; 4.4.1 State-of-the-Art; 4.4.2 Single-Source Design from MARTE; 4.5 Forecast About the Role MARTE May Have in Designing CPS; 4.5.1 The End of Moore's Law; 4.5.2 The Rise of Connected Ubiquitous Smart Objects; 4.6 Conclusion; References; 5 Combined Model Checking and Testing Create Confidence
A Case on Commercial Automotive Operating System; 5.1 Introduction; 5.2 OSEK/VDX Operating Systems; 5.3 Approach; 5.3.1 Design Model; 5.3.2 Design Verification and Environment Modelling; 5.3.3 Testing; 5.4 Related Works
2 Model-Based Design and Automated Validation of ARINC653 Architectures Using the AADL2.1 Introduction; 2.2 Boeing 777 ADIRU Case Study; 2.3 AADL and Patterns for IMA System; 2.3.1 The AADL Core Language; 2.3.2 Modeling Integrated Modular Architectures with AADL; 2.3.3 The AADL ARINC653 Annex; 2.3.4 ADIRU Full Model; 2.4 Model-Based Assurance with AADL; 2.4.1 Validation of AADL Models; 2.4.2 Application to ARINC653 Requirements; 2.5 Safety Analysis; 2.6 From Model to Code; 2.7 Conclusion and Future Work; References
3 Formal Semantics of Behavior Specifications in the Architecture Analysis and Design Language Standard3.1 Introduction; 3.2 Example of an Adaptive Cruise Control System; 3.3 Architecture Analysis and Design Language; 3.3.1 Architecture; 3.3.2 Properties; 3.3.3 AADL Timing Execution Model; 3.4 A Formalization Using Constrained Automata; 3.4.1 Vocabulary; 3.4.2 Formulas; 3.4.3 Model; 3.4.4 Automaton; 3.4.5 Properties; 3.4.6 Product; 3.4.7 Small Step; 3.4.8 Big Step; 3.4.9 Synchronous and Asynchronous Trace; 3.4.10 Timed Step and Timed Trace; 3.5 Behavior Annex Model; 3.5.1 Formalization
3.5.2 Transition System3.5.3 Behavior Conditions; 3.5.4 Action Language; 3.5.5 Communication Actions; 3.5.6 Expression Language; 3.5.7 Synchronization Protocols; 3.6 Related Work; 3.7 Conclusion; References; 4 MARTE for CPS and CPSoS; 4.1 Introduction; 4.1.1 CPS and CPSoS; 4.1.2 Role of UML and Its Extensions; 4.1.3 Outline; 4.2 Overview of MARTE; 4.2.1 Overview; 4.2.2 Foundations; 4.2.3 Non-functional Properties; 4.2.4 Time; 4.2.5 Allocation; 4.2.6 Design and Analysis in MARTE; 4.3 MARTE for CPS; 4.3.1 Case Study: Quadcopter
4.3.2 Proposed Extensions: Mixed-Criticality, Design-Space Exploration4.4 Tooling; 4.4.1 State-of-the-Art; 4.4.2 Single-Source Design from MARTE; 4.5 Forecast About the Role MARTE May Have in Designing CPS; 4.5.1 The End of Moore's Law; 4.5.2 The Rise of Connected Ubiquitous Smart Objects; 4.6 Conclusion; References; 5 Combined Model Checking and Testing Create Confidence
A Case on Commercial Automotive Operating System; 5.1 Introduction; 5.2 OSEK/VDX Operating Systems; 5.3 Approach; 5.3.1 Design Model; 5.3.2 Design Verification and Environment Modelling; 5.3.3 Testing; 5.4 Related Works