Formal Techniques for Safety-Critical Systems

Name: Formal Techniques for Safety-Critical Systems | 4th International Workshop, FTSCS 2015, Paris, France, November 6-7, 2015. Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

4th International Workshop, FTSCS 2015, Paris, France, November 6-7, 2015. Revised Selected Papers

Cyrille Artho Peter Csaba Ölveczky(Herausgeber*in)

Springer (Verlag)

Erschienen am 2. Februar 2016

X, 271 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-29510-7 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Contents
Invited Paper
Variant-Based Satisfiability in Initial Algebras
1 Introduction
2 Order-Sorted Algebra, Rewriting, and Variants
3 A Satisfiability Puzzle
4 Constructor Variants and Constructor Unifiers
5 Satisfiability in Initial Algebras: Descent Results
6 OS-Compact Theories and Satisfiability in T/ACCU
6.1 Theories (,ACCU) are OS-Compact
6.2 The Descent Theorem with Free Constructors Modulo ACCU
7 Satisfiability in Parameterized FVP Data Types
8 Related Work
9 Conclusions and Future Work
References
Timed Systems
An Executable Semantics of Clock Constraint Specification Language and Its Applications
1 Introduction
2 CCSL
2.1 Syntax and Semantics of CCSL
2.2 Satisfiability Problem of CCSL
3 Maude in a Nutshell
4 Formal Semantics of CCSL in Maude
5 Applications of the Formal Semantics
5.1 Bounded Scheduling
5.2 Customized Simulation
5.3 Periodic Scheduling
5.4 Bounded Model Checking
6 Related Works and Discussion
7 Conclusion and Future Work
References
What's Decidable About Parametric Timed Automata?
1 Introduction
2 Parametric Timed Automata and Problems
2.1 Clocks, Parameters and Constraints
2.2 A Unified Syntax for Parametric Timed Automata
2.3 Decision and Computation Problems
3 Almost Everything is Undecidable for Simple PTA
3.1 Decidability of the Membership
3.2 General Undecidable Problems
3.3 Bounding Time
3.4 Bounding the Parameter Domain
4 Bounding the Numbers of Clocks and Parameters
4.1 EF-Emptiness
4.2 Language and Trace Preservation
4.3 Parametric Model Checking
5 The Disappointing Class of L/U-PTA
5.1 Decidability Results
5.2 Undecidability Results
5.3 Intractability of the Synthesis
5.4 Two Open Classes: L-PTA and U-PTA
6 Open Questions
References
Compositional Predictability Analysis of Mixed Critical Real Time Systems
1 Introduction
2 Motivating Example
3 Related Work
4 Predictable Real Time Systems
5 Compositional Framework for Predictability Analysis
5.1 Hierarchical Real-Time Systems
5.2 Compositional Analysis
5.3 Conceptual Design
6 Uppaal System Model
7 Case Study
8 Conclusion
References
Railway Systems
Towards a Body of Knowledge in Formal Methods for the Railway Domain: Identification of Settled Knowledge
1 Introduction: Motivation and Related Work
2 Method
2.1 Settled Knowledge
2.2 Formal Concept Analysis
2.3 Stability Index
3 Results
4 Discussion: Possible Threats to Validity
5 Conclusion and Outlook to Future Work
References
Towards Safety Analysis of ERTMS/ETCS Level 2 in Real-Time Maude
1 Introduction
2 ERTMS Level 2
2.1 Scheme Plans
2.2 ERTMS System Architecture
2.3 Safety Conditions
3 Maude/Real-Time Maude
4 Modelling ERTMS in Maude
4.1 Datatypes: Location Specific Data and Messages
4.2 Instantaneously Reacting Sub-Systems
4.3 Trains
4.4 Safety Condition
4.5 Completeness
5 Validation Through Simulation and Error Injection
5.1 Simulation
5.2 Error Injection
6 Model Checking Results
7 Related Work
8 Summary and Future Work
References
Modeling Railway Control Systems in Promela
1 Introduction and Related Work
2 Background and Running Example
3 Definition of the Promela Model
3.1 Generation Steps
3.2 Building the System Model
3.3 Modeling the Environment
3.4 Constraining Behaviors
4 A Case Study in the Railway Domain
4.1 The Communication Procedure of the Radio Block Centre
4.2 Results
5 Conclusions and Future Work
References
Fault Tolerance
A Formal Model and Analysis of Feature Degradation in Fault-Tolerant Systems
1 Introduction and Motivation
2 Assumed System Design
3 Deployment Calculation and Degradation Analysis
3.1 Formal System and Deployment Model
3.2 Degradation of Functional Features
3.3 Fixed Properties of the Model
3.4 Solution Properties of the Model
3.5 Reconfigurations After Isolations
4 Example
4.1 Initial Deployment Solution for the Example
4.2 Analysis of Degradations for the Example
5 Conclusion
References
Probabilistic Analysis of a Calculus for Wireless Sensor Networks
1 Introduction
2 Review of the CWQ Calculus
3 Motivating Example
4 Data-Driven Probabilistic Trust Analysis
4.1 Trust Propagation
4.2 Trust Analysis
4.3 Probabilistic Trust Analysis of the Case Study
5 Conclusion and Future Work
References
Leveraging Abstraction to Establish Out-of-Nominal Safety Properties
1 Introduction
2 Modeling Out-of-Nominal Safety Properties
3 Example Turnstile Model
4 Design and Out-of-Nominal Verification via Abstraction
4.1 Refinement (High Level)
4.2 Implementation (Low Level)
5 Conclusion
A High-Level Model for Turnstile in TLA
B Boolean Network Model for Turnstile in NuSMV
References
Automotive Systems
A Controller Safety Concept Based on Software-Implemented Fault Tolerance for Fail-Operational Automotive Applications
1 Introduction
2 From a Fail-Safe to a Fail-Operational System Architecture
3 Fail-Operational Computing Platform
4 Stochastic Model Checking of the Fail-Operational Computing Platform
4.1 Technical Background
4.2 Modeling and Implementation
4.3 Properties
4.4 Results of the Stochastic Model Checking with PRISM
4.5 Recovery from Transient Faults
4.6 Interpretation of the Results
5 Software Coded Processing
5.1 Theory About Software Coded Processing
5.2 -encoding
5.3 Evaluation of -encoding
6 Related Work
7 Conclusion
References
Modeling Safety Requirements of ISO26262 Using Goal Trees and Patterns
1 Introduction
2 Related Works
3 Safety Requirements and Goal Tree
3.1 Safety Requirements
3.2 Goal Tree
4 Safety Requirements of EPS
4.1 PAA of EPS
4.2 Analysis of Safety Requirements
5 Safety Requirements Development Based on Goal Tree and Patterns
5.1 Goal Tree for Safety Requirements
5.2 Safety Requirement Patterns
5.3 Application of Safety Requirement Pattern
6 Case Study
6.1 Development of Goal Tree
6.2 Result
6.3 Evaluation
7 Discussion
8 Conclusion
References
Software and Systems Analysis
An Approach to Static-Dynamic Software Analysis
1 Introduction
2 Overview and Related Work
3 Our Approach to Static Analysis and Symbolic Execution
3.1 Static Analysis Using Model Checking and Trace Refinement
3.2 SMT Solving Based Symbolic Execution
4 An Integrated Static-Dynamic Approach
4.1 Architecture
4.2 Implementation
5 Experiments
5.1 Examples
5.2 SV-COMP Benchmark Results
5.3 Observations and Limitations
6 Conclusions
References
Towards Verifying VDM Using SPIN
1 Introduction
2 Preliminaries
2.1 The Vienna Development Method
2.2 The SPIN Model Checker
3 Model Checking VDM Using SPIN
3.1 Hybrid Model
3.2 Hybrid Model as Extended Automata
3.3 Constructing Hybrid Model Based on EAVDM
4 Case Study
4.1 Module SIMPLE
4.2 SAFER
4.3 Discussion
5 Related Work
6 Conclusion and Future Work
References
Tools
Statistical Model Checking of Simulink Models with Plasma Lab
1 Introduction
2 Plasma Lab Architecture
3 Plasma Lab and Simulink Integration
4 Related Works
References
g-HOL: A Graphical User Interface for the HOL Proof Assistant
1 Introduction
2 g-HOL's Architecture and Features
3 Illustrative Example
4 Conclusions
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken