Normal view MARC view ISBD view

Provably Correct Systems.

By: Hinchey, Mike.
Contributor(s): Bowen, Jonathan P | Olderog, Ernst-Rüdiger.
Material type: TextTextSeries: eBooks on Demand.NASA Monographs in Systems and Software Engineering: Publisher: Cham : Springer International Publishing, 2017Copyright date: ©2017Description: 1 online resource (332 pages).Content type: text Media type: computer Carrier type: online resourceISBN: 9783319486284.Subject(s): Computer scienceGenre/Form: Electronic books.Additional physical formats: Print version:: Provably Correct SystemsDDC classification: 005.131 Online resources: Click here to view this ebook.
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 Theory -- 3.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 Work -- References -- 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 Abstraction -- 6 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 Architectures -- 1 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 -- 5.1 Physical Interfaces and Cyber-Physical Components -- 5.2 Model the Evolution of a Smart Meter Network -- 6 Conclusions -- References -- Part V Automatic Verification -- Computing Verified Machine Address Bounds During Symbolic Exploration of Code -- 1 Preface -- 2 Introduction -- 3 A Little Background on ACL2 -- 4 Metafunctions -- 5 Bounders -- 6 Ainni: Abstract Interpreter over Natural Number Intervals -- 7 Some Examples -- 8 Using Ainni in a Metafunction -- 9 Other Uses of Ainni -- 10 Related Work -- 11 Conclusion -- References -- Engineering a Formal, Executable x86 ISA Simulator for Software Verification -- 1 Introduction -- 2 Approach.
2.1 Formal Methodology -- 2.2 Machine-Code Analysis -- 2.3 Design Goals -- 3 Model Definition -- 3.1 Concrete State -- 3.2 Abstract State -- 3.3 Modes of Operation: Interface to the x86 State -- 3.4 Instruction Semantic Functions -- 3.5 Step and Run Functions -- 4 Model Validation -- 4.1 Machine Program Parser and Loader -- 4.2 Instrumentation -- 5 Reasoning About x86 Machine-Code Programs -- 6 Related Work -- 7 Conclusion -- References -- Advances in Connection-Based Automated Theorem Proving -- 1 Introduction -- 2 Preliminaries -- 2.1 Classical Logic -- 2.2 Non-Classical Logics -- 2.3 Matrix Characterisation -- 3 Connection Calculi for Classical Logic -- 3.1 The Basic Calculus -- 3.2 Restricted Backtracking -- 3.3 Non-clausal Calculus -- 4 Connection Calculi for Non-classical Logics -- 4.1 Intuitionistic Logic -- 4.2 Modal Logics -- 5 Implementing Connection Calculi -- 5.1 Classical Logic -- 5.2 Intuitionistic Logic -- 5.3 Modal Logics -- 6 A Brief History and Perspectives -- 7 Conclusion -- References -- Part VI Run-Time Assertion Checking -- Run-Time Deadlock Detection -- 1 Introduction -- 2 The Framework -- 3 Deadlock Detection for Concurrent Objects -- 4 Deadlock Detection for Multi-threaded Java Programs -- 4.1 Multi-threaded Events -- 4.2 Multi-threaded Perspectives -- 5 Tool Architecture -- 6 Conclusion and Future Work -- References -- In-Circuit Assertions and Exceptions for Reconfigurable Hardware Design -- 1 Introduction -- 2 Background -- 2.1 Hardware Exceptions -- 2.2 Hardware Debugging -- 2.3 Assertion-Based Verification -- 2.4 Formal Verification -- 3 High-Level Approach -- 3.1 Step-by-step Approach -- 4 Implementation: Maxeler Systems -- 4.1 Language Extensions for Runtime Assertions and Exceptions -- 4.2 Circuit Realizations of Assertions and Exceptions -- 4.3 Hardware and Software APIs for Assertions and Exceptions.
4.4 Case Study -- 5 Evaluation -- 5.1 Experimental Setup -- 5.2 Area Results -- 5.3 Imprecise Exceptions -- 6 Conclusion -- References -- Part VII Formal and Semi-formal Methods -- From ProCoS to Space and Mental Models--A Survey of Combining Formal and Semi-formal Methods -- 1 Introduction -- 2 Abstraction and Refinement--CSP and FDR2 -- 2.1 CSP -- 2.2 Refinement and FDR2 -- 2.3 Abstraction -- 2.4 Generic Theories--Pattern-Based Verification -- 2.5 Algebraic Reasoning -- 2.6 Compositional Proof Theory -- 3 Space -- 3.1 Technical Background: The Fault Tolerant Computer -- 3.2 Verification Approach -- 3.3 Lessons Learned--Part 1 -- 4 Mental Models and Refinement -- 4.1 Mode Confusion Analysis--Background -- 4.2 The Example -- 4.3 Verification Approach -- 4.4 Lessons Learned--Part 2 -- 5 Conclusion -- 5.1 Overall Evaluation -- 5.2 Other Experiments -- References -- Part VIII Web-Supported Communities in Science -- Provably Correct Systems: Community, Connections, and Citations -- 1 Background -- 2 The ProCoS Community -- 3 A Community Around a Researcher -- 4 Community of Practice -- 5 Citation Metrics -- 6 Conclusion -- References -- Erratum to: ProCoS: How It All Began - as Seen from Denmark -- Erratum to:ProCoS: How It All Began - as Seen from Denmark in: M. Hinchey et al. (eds.), Provably Correct Systems, NASA Monographs in Systems and Software Engineering, DOI 10.1007/978-3-319-48628-4_1.
Tags from this library: No tags from this library for this title. Log in to add tags.
Item type Current location Call number URL Status Date due Barcode
Electronic Book UT Tyler Online
Online
QA75.5-76.95 (Browse shelf) http://ebookcentral.proquest.com/lib/uttyler/detail.action?docID=4815414 Available EBC4815414

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 Theory -- 3.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 Work -- References -- 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 Abstraction -- 6 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 Architectures -- 1 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 -- 5.1 Physical Interfaces and Cyber-Physical Components -- 5.2 Model the Evolution of a Smart Meter Network -- 6 Conclusions -- References -- Part V Automatic Verification -- Computing Verified Machine Address Bounds During Symbolic Exploration of Code -- 1 Preface -- 2 Introduction -- 3 A Little Background on ACL2 -- 4 Metafunctions -- 5 Bounders -- 6 Ainni: Abstract Interpreter over Natural Number Intervals -- 7 Some Examples -- 8 Using Ainni in a Metafunction -- 9 Other Uses of Ainni -- 10 Related Work -- 11 Conclusion -- References -- Engineering a Formal, Executable x86 ISA Simulator for Software Verification -- 1 Introduction -- 2 Approach.

2.1 Formal Methodology -- 2.2 Machine-Code Analysis -- 2.3 Design Goals -- 3 Model Definition -- 3.1 Concrete State -- 3.2 Abstract State -- 3.3 Modes of Operation: Interface to the x86 State -- 3.4 Instruction Semantic Functions -- 3.5 Step and Run Functions -- 4 Model Validation -- 4.1 Machine Program Parser and Loader -- 4.2 Instrumentation -- 5 Reasoning About x86 Machine-Code Programs -- 6 Related Work -- 7 Conclusion -- References -- Advances in Connection-Based Automated Theorem Proving -- 1 Introduction -- 2 Preliminaries -- 2.1 Classical Logic -- 2.2 Non-Classical Logics -- 2.3 Matrix Characterisation -- 3 Connection Calculi for Classical Logic -- 3.1 The Basic Calculus -- 3.2 Restricted Backtracking -- 3.3 Non-clausal Calculus -- 4 Connection Calculi for Non-classical Logics -- 4.1 Intuitionistic Logic -- 4.2 Modal Logics -- 5 Implementing Connection Calculi -- 5.1 Classical Logic -- 5.2 Intuitionistic Logic -- 5.3 Modal Logics -- 6 A Brief History and Perspectives -- 7 Conclusion -- References -- Part VI Run-Time Assertion Checking -- Run-Time Deadlock Detection -- 1 Introduction -- 2 The Framework -- 3 Deadlock Detection for Concurrent Objects -- 4 Deadlock Detection for Multi-threaded Java Programs -- 4.1 Multi-threaded Events -- 4.2 Multi-threaded Perspectives -- 5 Tool Architecture -- 6 Conclusion and Future Work -- References -- In-Circuit Assertions and Exceptions for Reconfigurable Hardware Design -- 1 Introduction -- 2 Background -- 2.1 Hardware Exceptions -- 2.2 Hardware Debugging -- 2.3 Assertion-Based Verification -- 2.4 Formal Verification -- 3 High-Level Approach -- 3.1 Step-by-step Approach -- 4 Implementation: Maxeler Systems -- 4.1 Language Extensions for Runtime Assertions and Exceptions -- 4.2 Circuit Realizations of Assertions and Exceptions -- 4.3 Hardware and Software APIs for Assertions and Exceptions.

4.4 Case Study -- 5 Evaluation -- 5.1 Experimental Setup -- 5.2 Area Results -- 5.3 Imprecise Exceptions -- 6 Conclusion -- References -- Part VII Formal and Semi-formal Methods -- From ProCoS to Space and Mental Models--A Survey of Combining Formal and Semi-formal Methods -- 1 Introduction -- 2 Abstraction and Refinement--CSP and FDR2 -- 2.1 CSP -- 2.2 Refinement and FDR2 -- 2.3 Abstraction -- 2.4 Generic Theories--Pattern-Based Verification -- 2.5 Algebraic Reasoning -- 2.6 Compositional Proof Theory -- 3 Space -- 3.1 Technical Background: The Fault Tolerant Computer -- 3.2 Verification Approach -- 3.3 Lessons Learned--Part 1 -- 4 Mental Models and Refinement -- 4.1 Mode Confusion Analysis--Background -- 4.2 The Example -- 4.3 Verification Approach -- 4.4 Lessons Learned--Part 2 -- 5 Conclusion -- 5.1 Overall Evaluation -- 5.2 Other Experiments -- References -- Part VIII Web-Supported Communities in Science -- Provably Correct Systems: Community, Connections, and Citations -- 1 Background -- 2 The ProCoS Community -- 3 A Community Around a Researcher -- 4 Community of Practice -- 5 Citation Metrics -- 6 Conclusion -- References -- Erratum to: ProCoS: How It All Began - as Seen from Denmark -- Erratum to:ProCoS: How It All Began - as Seen from Denmark in: M. Hinchey et al. (eds.), Provably Correct Systems, NASA Monographs in Systems and Software Engineering, DOI 10.1007/978-3-319-48628-4_1.

Description based on publisher supplied metadata and other sources.

There are no comments for this item.

Log in to your account to post a comment.