Provably correct systems. (2017)

• Record Type: Book
• Further Information: Note: Mike Hinchey, Jonathan P. Bowen, Ernst-Rüdiger Olderog, editors.
• Editors: Hinchey, Michael G (Michael Gerard), 1969-; Bowen, J. P (Jonathan Peter), 1956-; Olderog, E.-R
• 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.
• Publisher Details: Cham, Switzerland : Springer
• Publication Date: 2017
• Extent: 1 online resource (xviii, 328 pages), illustrations (some color)
• Subjects: 005.1/4; Computer science; Computer software -- Verification; Embedded computer systems; COMPUTERS -- Software Development & Engineering -- General; Computer software -- Verification; Embedded computer systems; Computers -- Programming -- General; Computers -- Online Services -- General; Computer programming / software development; Computer science; Logic design; Mathematics -- Logic; Mathematical theory of computation; Electronic books
• Languages: English
• ISBNs: 9783319486284; 3319486284
• Related ISBNs: 9783319486277; 3319486276
• Notes: Note: Includes bibliographical references.; Note: Online resource; title from PDF title page (SpringerLink, viewed March 9, 2017).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.