Linked e-resources
Details
Table of Contents
Preface; Organization; Table of Contents; Verification of Embedded Real-time Systems; 1 Introduction; 2 Related Work; 2.1 Formal Verification of SystemC Designs; 2.2 Conformance Testing for Real-time Systems; 2.3 Automatic Test Generation for SystemC; 3 Preliminaries; 3.1 SystemC; 3.2 Uppaal Timed Automata; 4 VeriSTA; 5 Formal Semantics for SystemC; 6 Model Checking and Conformance Testing; 7 Evolutionary Generation of Timed Test Traces; 8 Experimental Results; 8.1 Results from the AMBA advanced high-performance bus; 8.2 Results from the ASR/ABS system; 9 Conclusion; Acknowledgements
2.2 Definition and Semantics3 Numerical Simulation; 3.1 Solving ODEs; 3.2 Computing Trajectories and Jumps; 3.3 Accounting for Nondeterminism; 3.4 Verification by simulation; 4 Reachability Analysis; 4.1 Reachability Algorithm; 4.2 Piecewise Constant Dynamics; 4.3 Piecewise Affine Dynamics; 4.4 Nonlinear Dynamics; 5 Conclusions; References; Model Checking and Model-based Testing in the Railway Domain; 1 Introduction; 2 Formal Verification; 2.1 Verification by Bounded Model Checking and k-Induction; 2.2 Formal Modelling; 2.3 Method Summary; 3 Interlocking System Verification
a Case Study
3.1 The Novel Danish Interlocking Systems3.2 The Domain-specific Language for Interlocking Systems; 3.3 Framework Implementation; 3.4 Generated Models; 3.5 Generated Safety Conditions; 3.6 Invariant Strengthening; 3.7 Verification Experiments; 4 Model-based Testing; 4.1 Model-based Testing Terminology; 4.2 Overall Test Objectives for the Railway Application; 4.3 Semantic Domain: I/O State Transition Systems; 4.4 Complete Testing Strategies; 4.5 Test Requirements Enforced by Standards; 4.6 Generic Domain-specific Test Strategy; 4.7 Functional Decomposition and Equivalence Classes
4.8 Further Test Reduction Heuristics5 Conclusion; Acknowledgments; References; Modeling Unknown Values in Test and Verification; 1 Introduction; 1.1 Unknown Values in Circuit Test; 1.2 Unknown Values in Verification; 1.3 Minimization/Maximization in Test and Verification; 2 Basics; 2.1 Boolean Satisfiability and Extensions; 2.2 Quantified Boolean Formulas; 2.3 Dependency Quantified Boolean Formulas; 2.4 From Circuits to Formulas; 3 Unknown Values in Circuit Test; 3.1 Standard X-Logic Simulation; 3.2 Accurate Logic Simulation; 3.3 Accurate Fault Simulation
2.2 Definition and Semantics3 Numerical Simulation; 3.1 Solving ODEs; 3.2 Computing Trajectories and Jumps; 3.3 Accounting for Nondeterminism; 3.4 Verification by simulation; 4 Reachability Analysis; 4.1 Reachability Algorithm; 4.2 Piecewise Constant Dynamics; 4.3 Piecewise Affine Dynamics; 4.4 Nonlinear Dynamics; 5 Conclusions; References; Model Checking and Model-based Testing in the Railway Domain; 1 Introduction; 2 Formal Verification; 2.1 Verification by Bounded Model Checking and k-Induction; 2.2 Formal Modelling; 2.3 Method Summary; 3 Interlocking System Verification
a Case Study
3.1 The Novel Danish Interlocking Systems3.2 The Domain-specific Language for Interlocking Systems; 3.3 Framework Implementation; 3.4 Generated Models; 3.5 Generated Safety Conditions; 3.6 Invariant Strengthening; 3.7 Verification Experiments; 4 Model-based Testing; 4.1 Model-based Testing Terminology; 4.2 Overall Test Objectives for the Railway Application; 4.3 Semantic Domain: I/O State Transition Systems; 4.4 Complete Testing Strategies; 4.5 Test Requirements Enforced by Standards; 4.6 Generic Domain-specific Test Strategy; 4.7 Functional Decomposition and Equivalence Classes
4.8 Further Test Reduction Heuristics5 Conclusion; Acknowledgments; References; Modeling Unknown Values in Test and Verification; 1 Introduction; 1.1 Unknown Values in Circuit Test; 1.2 Unknown Values in Verification; 1.3 Minimization/Maximization in Test and Verification; 2 Basics; 2.1 Boolean Satisfiability and Extensions; 2.2 Quantified Boolean Formulas; 2.3 Dependency Quantified Boolean Formulas; 2.4 From Circuits to Formulas; 3 Unknown Values in Circuit Test; 3.1 Standard X-Logic Simulation; 3.2 Accurate Logic Simulation; 3.3 Accurate Fault Simulation