Critical Systems: Formal Methods and Automated Verification

Name: Critical Systems: Formal Methods and Automated Verification | Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, Pisa, Italy, September 26-28, 2016, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, Pisa, Italy, September 26-28, 2016, Proceedings

Maurice H. ter Beek Stefania Gnesi Alexander Knapp(Herausgeber*in)

Springer (Verlag)

Erschienen am 12. September 2016

XVI, 247 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-45943-1 (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
Abstracts of the Invited Talks
Lessons Learned in a Journey Toward Correct-by-Construction Model-Based Development
Model-based Testing Strategies and Their (In)dependence on Syntactic Model Representations
Random Testing of Formal Properties for Industrial Critical Systems
Contents
Invited Talk
Model-Based Testing Strategies and Their (In)dependence on Syntactic Model Representations
1 Introduction
2 Problem Description
3 A Model-Independent Method for Input Equivalence Class Partition Testing
4 Model-Based Transformation-Invariant Calculation of Input Equivalence Classes
5 Conclusion
References
Automated Verification Techniques
Abstract Interpretation of MATLAB Code with Interval Sets
1 Introduction
1.1 Contribution
2 Related Work
3 Abstract Interpretation of MATLAB
3.1 Syntax and Concrete Semantics
3.2 Abstract Semantics
3.3 Abstract Interpretation
4 Evaluation
5 Conclusion
References
Workflow Nets Verification: SMT or CLP?
1 Introduction
2 Preliminaries
2.1 Workflow Nets
2.2 Modal Specifications
2.3 Modal Specifications Verification Method
3 Experimental Protocol
4 Results and Feedback from Experiments
4.1 Observation from State-Machine Workflow Nets Verification
4.2 Observation from Marked-Graph Workflow Nets Verification
4.3 Observation from Free-Choice Workflow Nets Verification
4.4 Observation from Ordinary Workflow Nets Verification
4.5 Lessons Learned from Experience
5 Related Work and Conclusion
References
One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast
1 Introduction
2 Architecture
3 An Inner Look at Automated VeriFast
3.1 Auto-generating Predicates
3.2 Auto-fixing
4 Automated VeriFast by Examples
4.1 Stack Example
4.2 Bank Example
5 Related Work
6 Conclusions and Future Work
References
Analyzing Unsatisfiability in Bounded Model Checking Using Max-SMT and Dual Slicing
1 Introduction
2 Background and Motivating Example
2.1 Bounded Model Checking for Embedded Control Software
2.2 Example Model with a Counter
2.3 Motivation
3 Initial Condition Analysis Using Maximum Satisfiability
3.1 Max-SMT
3.2 Analyzing Initial Conditions with a Partial Max-SMT Solver
3.3 Example of Analyzing Initial Conditions
3.4 Limitations
4 Causal Path Analysis Using Dual Slicing
4.1 Dual Slicing
4.2 Causal Path Analysis
4.3 How to Compare Execution Logs
4.4 Example of Analyzing the Causal Path
5 Case Study
5.1 Outline of the Model and Problem Setting
5.2 Results
6 Related Work
7 Conclusion and Future Work
References
Towards the Automated Verification of Weibull Distributions for System Failure Rates
1 Introduction
2 Multi-state Failure Mode in Satellite Subsystems
3 Preliminaries
3.1 Continuous-Time Markov Chains
3.2 The PRISM Model Checker
3.3 Continuous Stochastic Logic
4 Approximation of Weibull Failure Models
4.1 Weibull Distributions
4.2 Increasing Failure Rates (IFR)
4.3 Decreasing Failure Rates (DFR)
5 Encoding the Weibull Models with CTMCs in PRISM
5.1 Encoding the Weibull Distribution with IFR
5.2 Encoding the Weibull Distribution with DFR
6 Conclusion and Future Work
References
Fault-Aware Modeling and Specification for Efficient Formal Safety Analysis
1 Introduction
2 Model-Based Safety Analysis
2.1 Fault Terminology
2.2 State-Based Fault Modeling
3 Fault-Aware Modeling and Specification
3.1 Fault-Aware Kripke Structures
3.2 Fault-Aware Linear Temporal Logic
3.3 Fault Injection
4 Deductive Cause Consequence Analysis
4.1 Conceptual Improvement: Safe Fault Sets
4.2 Efficiency Improvement: Fault Removal
5 Tool Support and Evaluation
5.1 The S# Modeling and Analysis Framework for Safety-Critical Systems
5.2 Evaluated Case Studies
5.3 Evaluation Results
6 Conclusion and Future Work
References
Model-Based System Analysis
Block Library Driven Translation Validation for Dataflow Models in Safety Critical Systems
1 Introduction
2 Formal Specification of Blocks in Dataflow Languages
2.1 Example of Block Specification: IntegerDelay
2.2 Specifying a Block Family
2.3 Verification and Validation of Block Specifications
2.4 Handling Loop Constructs
3 Verification of the Correctness of Generated Code
3.1 Semantic Annotation of the Generated Code
3.2 Verification Using the Frama-C Toolset
4 Translation Validation of IntegerDelay
5 Related Work
6 Conclusion and Future Work
References
A Model-Based Framework for the Specification and Analysis of Hierarchical Scheduling Systems
1 Introduction
2 Background
3 Formal Model-Based Compositional Framework for Hierarchical Scheduling Systems
3.1 Automata-Based Models for a Scheduling Unit
3.2 Formal Analysis of Hierarchical Scheduling Systems
References
Utilising K Semantics for Collusion Detection in Android Applications
1 Introduction
1.1 Related Work
2 A Collusion Definition on the Android Level
3 The K Framework
4 Concrete Android Semantics
5 Abstract Android Semantics
6 Model Checking for Collusion
7 Concluding Remarks and Future Work
References
Unified Simulation, Visualization, and Formal Analysis of Safety-Critical Systems with
1 Introduction
2 Case Study: Height Control System
3 Modeling Safety-Critical Systems with
3.1 Model of Computation
3.2 The Modeling Language
3.3 Fault Modeling
4 Analyzing Safety-Critical Systems with
4.1 Execution Semantics of Models
4.2 Model Checking Models
4.3 Simulating Models
4.4 Evaluation of Model Checking Efficiency
4.5 Safety Analysis of the Height Control Case Study
5 Conclusion and Future Work
References
Applications and Case Studies
Formal Verification of a Rover Anti-collision System
1 Introduction
2 The S3 Toolset
3 Specification and Design of the ARP Use Case
3.1 The Context of Use Case
3.2 System-Level Safety and Functional Requirements
3.3 System Design Choice
3.4 High-Level Software Requirements and Software Design
4 Property Verification
4.1 The Workflow of Property Verification
4.2 K-Inductive Proof of Safety Property
4.3 BMC and Test Case Generation
4.4 Safety Property and Map Data Validation
4.5 Property Verification Results
5 Equivalence Proof Between Design and Generated Code
6 Lessons Learned
6.1 Proof of Generated Code
6.2 Proof-Driven Design Guidance
7 Conclusion and Perspective
References
Verification of AUTOSAR Software Architectures with Timed Automata
1 Introduction
2 Background
2.1 Introduction to AUTOSAR
2.2 Timed Automata
3 Transformation of AUTOSAR Models
3.1 Transformation
4 AUTOSAR Timing Extensions
4.1 Timing Events
5 Implementation and Evaluation
6 Conclusion
References
Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System
1 Introduction
2 Application: Arbitrary Waveform Generator (AWG)
3 Expressing the AWG in TLA+
3.1 Limitations of the TLA+ Framework
4 Expressing the AWG in TLACoq
5 Implementing TLACoq
6 Conclusions
References
Application of Coloured Petri Nets in Modelling and Simulating a Railway Signalling System
1 Introduction
2 Introduction to the Railway Signalling Principle and Desired Properties
2.1 Railway Signalling Principle
2.2 Desired Properties
3 The Coloured Petri Net Model
3.1 Global Declarations and Route's State
3.2 Setting Routes
3.3 Clearing Signals
3.4 Approach Locked and Back Locked
3.5 Releasing Route
4 Lessons Learnt and Perspective
5 Conclusion and Suggested Work
References
Formal Techniques for a Data-Driven Certification of Advanced Railway Signalling Systems
1 Introduction
2 Innovation in Signalling Systems
2.1 ``Communication Based'' Distancing Systems
2.2 Highly Innovative Distancing Concepts
2.3 Distributed Interlocking Systems
2.4 Safety Paradigm Shift
3 Integrity and Consistency of Vital Information
4 Demonstrating Safety
4.1 Data-Driven Safety Design Techniques
4.2 Software Faults
5 Quantitative Dependability Assessment
6 Conclusions
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken