Formal Methods for Industrial Critical Systems

Name: Formal Methods for Industrial Critical Systems | 16th International Workshop, FMICS 2011, Trento, Italy, August 29-30, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

16th International Workshop, FMICS 2011, Trento, Italy, August 29-30, 2011, Proceedings

Gwen Salaün Bernhard Schätz(Herausgeber*in)

Springer (Verlag)

Erschienen am 19. September 2011

X, 261 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-24431-5 (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

Title
Preface
Organization
Table of Contents
Towards Trustworthy Aerospace Systems: An Experience Report
Introduction
Modeling Using an AADL Dialect
Formal Verification
Requirements
Safety
Toolset
Industrial Evaluation
References
Satisfiability at Microsoft
Lightweight Verification of a Multi-Task Threaded Server: A Case Study With The Plural Tool
Introduction
Preliminaries
Plural Specification Language
Checking Programs with Plural
General Outline of the MTTS Application
Specification and Verification of MTTS
The General Specification Approach
Miscellaneous Aspects of the Specification of the MTTS
Discussion on the Limitations of Plural
Conclusion and Future Work
References
Runtime Verification of Typical Requirements for a Space Critical SoC Platform
Introduction
ABV for SoC Platforms
Expression of Requirements for TLM Designs
Platform Instrumentation
Related Works
The Case Study
Platform Description
Some Typical Requirements
Application of ABV to the Case Study
Convolution Processings in Sequence
Convolution Processing and Transfer of Addresses
Successive Splits Forbidden
Performances
Conclusion
References
Past Time LTL Runtime Verification for Microcontroller Binary Code
Introduction
Runtime Verification by Code Instrumentation
Pitfalls of Code Instrumentation
Requirements to Runtime Verification of Microcontroller Code
Contributions to Runtime Verification
Structure of the Paper
Preliminaries
Formal Microcontroller Model
Past Time LTL
System Overview
ptLTL Observer Synthesis
Hardware Monitor Unit
Host Application
Worked Example
ptLTL Specification
Online Runtime Verification
Offline Runtime Verification
Related Work
Conclusion and Future Challenges
References
A SAT-Based Approach for the Construction of Reusable Control System Components
Introduction
Illustration of Basic Concepts with an Example
Overview of the Main Concepts of HCA
Overview of Alloy and Its Use in the Design of Components
Construction of Elementary Components with Alloy
Checking the Condition for Tc
Checking the Consistency of Marking
Checking the Observer Property
Construction of Composite Components with Alloy
Conclusion
References
Formal Safety Analysis in Industrial Practice
Introduction
Safety Analysis and DCCA
Safety Analysis
Safety-Oriented Software Design
Formal Verification Using Scade DV
Deductive Cause Consequence Analysis
Liveness and Abstraction Techniques
Liveness Analysis
Dealing with Complexity within Scade DV
Model Transformation to UPPAAL
Correctness of the Model Transformation
Comparative Safety Analysis of Level Crossing Control
Application of FMEA
Application of DCCA
Liveness Analysis
Lessons Learned and Conclusions
Lessons Learned
Open Issues and Future Work
References
Structural Test Coverage Criteria for Integration Testing of LUSTRE/SCADE Programs
Introduction
Background
Overview of Lustre
Lustre Coverage Criteria
Integration Testing Approach
Motivation
Path Activation Conditions
Extended Criteria Definition
Empirical Evaluation
Testing Effort
Fault Finding Effectiveness
Threats to Validity
Conclusion
References
Formal Analysis of a Triplex Sensor Voter in an Industrial Context
Introduction
The Triplex Voter
Analysis of the Simulink Model
Properties of Interest
Analysis Results
Analysis of a Floating Point Implementation
Analysis Using an SMT Solver
Analysis by Abstract Interpretation
Automated Generation of Invariants
Lessons Learned
Ongoing and Future Work
References
Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost.
Introduction
Background
The XBus and Its Context
Model-Based Testing
The Specification Language mCRL2
Development of the XBus
XBus Requirements
XBus Design
Implementation
Unit Testing
Model-Based Integration Testing
Acceptance Testing
Findings and Lessons Learned
Conclusions and Future Research
References
Symbolic Power Analysis of Cell Libraries
Introduction
Preliminaries
Reducing Input Vector Orders for Power Analysis
Order-Independence of Power-Extended Transition Systems
Equivalence Relation on Orders
Selecting Orders to Minimize Power Consumption
Implementation
Experimental Results
Reducing Input Vector Orders
Selecting Input Vector Orders
Conclusions
References
An Automated Semantic-Based Approach for Creating Tasks from Matlab Simulink Models
Introduction
Function Networks
From Specification Models to Function Networks
Translating Simulink
Preserving Semantics
Task Creation - Semantics and Application
Cohesion and Weights
Syntax and Semantics of Task Creation
Task Creation Algorithm
Case Study and Experimental Results
Conclusions
References
Performability Measure Specification: Combining CSRL and MSL
Introduction
Reference Model
Core Logic of UMSL
Extending MSL Parameterization
Extending CSRL with Actions
Intertwining aCSRL and dnfMSL
Measure Definition Mechanism of UMSL
Conclusion
References
Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit Using CADP
Introduction
Dynamic Task Dispatcher
Formal Model of the DTD
Design Choices
Modeling the Dynamic Task Dispatcher Hardware
Modeling Applications and Processors
Formal Analysis of the DTD
Co-simulation of the C++ and LOTOS NT Models
Principles of the EXEC/CÆSAR Framework
Approach
Results
Conclusion
References
Transforming SOS Specifications to Linear Processes
Introduction
Preliminaries
Structural Operational Semantics
(Simplified) Linear Process Specifications
Method
Signature Transformation
Transitions
Linear Process Transition Generator
Application
Implementation
Extension of the Framework
Related Work
Assessment and Future Work
References
Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study
Introduction
BLMS Overview
Successive Running Sums (SRS)
Verification of the SRS Implementation Using HOL4
Introduction
Formal Model of SRS
Theorems about the Model
Conclusions and Lessons Learned
References
Hierarchical Modeling and Formal Verification. An Industrial Case Study Using Reo and Vereofy
Introduction
The ASK System
Top-Down Modeling and Specification of ASK
Basic Principles of Reo and Constraint Automata
Hierarchical Modeling
Verification of the ASK Model
Verification of the ASK Model Using Vereofy
Conclusion
References
Modeling and Verifying Timed Compensable Workflows and an Application to Health Care
Introduction
Preliminaries
Workflow and Time Constraints
Compensable Transaction
Modeling Timed Compensable Workflow with CWFT-Nets
Timed Compensable Workflow Nets (CWFT-Nets)
Graphical Representation of CWFT-Net
Verification of CWFT-Nets
Case Study and Property Verification
Related and Future Work
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken