Linked e-resources
Details
Table of Contents
Foreword; Preface; Impact; Structure of this Book; Historic Account; Hybrid Systems; Correctness of Concurrent Algorithms; Interfaces and Linking; Automatic Verification; Run-Time Assertion Checking; Formal and Semi-formal Methods; Web-Supported Communities in Science; Acknowledgements; Contents; Part I Historic Account; ProCoS: How It All Began
as Seen from Denmark; Part II Hybrid Systems; Constraint-Solving Techniques for the Analysis of Stochastic Hybrid Systems; 1 Introduction; 2 Stochastic Hybrid Transition Systems; 3 Bounded Reachability Checking for Stochastic Hybrid Automata
3.1 Stochastic Satisfiability Modulo Theory3.2 CSSMT Solving; 4 Parameter Synthesis for Parametric Stochastic Hybrid Automata; 4.1 Parameter Synthesis Using Symbolic Importance Sampling; 5 Conclusion; References; MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems; 1 Introduction; 1.1 Related Work; 2 Sim2HCSP Translator; 3 HHL Prover; 4 Invariant Generator; 4.1 Isabelle Oracle; 4.2 Differential Invariant Generation; 4.3 Abstraction of Elementary Hybrid Systems by Variable Transformation; 4.4 QE-Based Invariant Generator; 4.5 SOS-Based Invariant Generator
5 Conclusion and Future WorkReferences; Part III Correctness of Concurrent Algorithms; A Proof Method for Linearizability on TSO Architectures; 1 Introduction; 2 Linearizability; 2.1 A Formal Definition of Linearizability; 2.2 A Proof Method for Linearizability; 3 The TSO Memory Model; 3.1 TSO-Linearizability; 4 Using a Coarse-Grained Abstraction; 4.1 Defining the Coarse-Grained Abstraction; 4.2 From Coarse-Grained to Abstract Specification; 5 Case Study: Work-Stealing Deque; 5.1 Abstract Specification; 5.2 Concrete Specification; 5.3 Refined Abstract Specification
5.4 Coarse-Grained Abstraction6 Conclusion; References; Part IV Interfaces and Linking; Linking Discrete and Continuous Models, Applied to Traffic Manoeuvrers; 1 Introduction; 2 Symbolic Model; 2.1 View; 2.2 Spatial Logic; 2.3 Transition System; 3 Abstract Controllers; 3.1 Keeping Distance; 3.2 Changing Lanes; 3.3 Safety; 4 Concrete Model; 4.1 Longitudinal Motion; 4.2 Lateral Motion; 5 Linking; 5.1 Distance Controller; 5.2 Lane-Change Controller; 6 Concrete Controllers; 6.1 Longitudinal Control; 6.2 Lane Change; 7 Related Work; 8 Conclusion; References
Towards Interface-Driven Design of Evolving Component-Based Architectures1 Introduction; 2 Complex Evolving Systems; 2.1 Chronic Complexity of Digital Ecosystems; 2.2 An Application Examples; 3 Interfaces and Component-Based Architectures; 3.1 Key Features of rCOS; 3.2 Components and Their Interfaces; 3.3 Composition and Orchestration; 3.4 Separation of Concerns; 4 Incremental Design of an Enterprise Application; 4.1 Requirements Modelling; 4.2 OO Design of Components; 4.3 Incremental Development and System Evolution; 5 Towards Modelling Cyber-Physical Component Systems
as Seen from Denmark; Part II Hybrid Systems; Constraint-Solving Techniques for the Analysis of Stochastic Hybrid Systems; 1 Introduction; 2 Stochastic Hybrid Transition Systems; 3 Bounded Reachability Checking for Stochastic Hybrid Automata
3.1 Stochastic Satisfiability Modulo Theory3.2 CSSMT Solving; 4 Parameter Synthesis for Parametric Stochastic Hybrid Automata; 4.1 Parameter Synthesis Using Symbolic Importance Sampling; 5 Conclusion; References; MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems; 1 Introduction; 1.1 Related Work; 2 Sim2HCSP Translator; 3 HHL Prover; 4 Invariant Generator; 4.1 Isabelle Oracle; 4.2 Differential Invariant Generation; 4.3 Abstraction of Elementary Hybrid Systems by Variable Transformation; 4.4 QE-Based Invariant Generator; 4.5 SOS-Based Invariant Generator
5 Conclusion and Future WorkReferences; Part III Correctness of Concurrent Algorithms; A Proof Method for Linearizability on TSO Architectures; 1 Introduction; 2 Linearizability; 2.1 A Formal Definition of Linearizability; 2.2 A Proof Method for Linearizability; 3 The TSO Memory Model; 3.1 TSO-Linearizability; 4 Using a Coarse-Grained Abstraction; 4.1 Defining the Coarse-Grained Abstraction; 4.2 From Coarse-Grained to Abstract Specification; 5 Case Study: Work-Stealing Deque; 5.1 Abstract Specification; 5.2 Concrete Specification; 5.3 Refined Abstract Specification
5.4 Coarse-Grained Abstraction6 Conclusion; References; Part IV Interfaces and Linking; Linking Discrete and Continuous Models, Applied to Traffic Manoeuvrers; 1 Introduction; 2 Symbolic Model; 2.1 View; 2.2 Spatial Logic; 2.3 Transition System; 3 Abstract Controllers; 3.1 Keeping Distance; 3.2 Changing Lanes; 3.3 Safety; 4 Concrete Model; 4.1 Longitudinal Motion; 4.2 Lateral Motion; 5 Linking; 5.1 Distance Controller; 5.2 Lane-Change Controller; 6 Concrete Controllers; 6.1 Longitudinal Control; 6.2 Lane Change; 7 Related Work; 8 Conclusion; References
Towards Interface-Driven Design of Evolving Component-Based Architectures1 Introduction; 2 Complex Evolving Systems; 2.1 Chronic Complexity of Digital Ecosystems; 2.2 An Application Examples; 3 Interfaces and Component-Based Architectures; 3.1 Key Features of rCOS; 3.2 Components and Their Interfaces; 3.3 Composition and Orchestration; 3.4 Separation of Concerns; 4 Incremental Design of an Enterprise Application; 4.1 Requirements Modelling; 4.2 OO Design of Components; 4.3 Incremental Development and System Evolution; 5 Towards Modelling Cyber-Physical Component Systems