FM 2011: Formal Methods

Name: FM 2011: Formal Methods | 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011, Proceedings

Michael Butler Wolfram Schulte(Herausgeber*in)

Springer (Verlag)

Erschienen am 21. Juni 2011

XIV, 450 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-21437-0 (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
Invited Talks
Model Integration and Cyber Physical Systems: A Semantics Perspective
Some Thoughts on Behavioral Programming
The Only Way Is Up
Introduction
The Process of Hardware Design
Hardware and Wetware
The Software of Life
References
Cyber-Physical Systems
Does It Pay to Extend the Perimeter of a World Model?
Introduction
A Motivating Example
From Correctness to Dominance
Verification and Synthesis
Foundations
World Models
Strategic Objectives
Strategy Classes
Winning Strategies
Remorsefree Dominance
An Automata-Theoretic Characterization of Remorsefree Dominance
Preliminaries: Automata over Infinite Words and Trees
Dominant Computations
Dominant Strategies
Verifying and Synthesizing Dominant Strategies
Towards Optimal World Models
Conclusions
References
System Verification through Program Verification
Introduction
Preliminaries
Kripke Structure
LTL Syntax
LTL Semantics
The Interface between Requirements and Software
The Class of Memory-Mapped Systems
Case Study
Related Work
Conclusion
References
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified
Introduction
Related Work
Preliminaries: Quantified Differential Dynamic Logic
The Distributed Car Control Problem
Local Lane Control
Global Lane Control
Local Highway Control
Global Highway Control
Conclusion and Future Work
References
Runtime Analysis
TRACECONTRACT: A Scala DSL for Trace Analysis
Introduction
The TraceContract DSL
The DSL and a First Example
State Machines
Future Time Temporal Logic
Past Time Temporal Logic
Using Monitors
Implementation
Formulas and Linear Temporal Logic
State-Oriented Constructs
Properties, Formulas, and Error Traces
Conclusion
References
Using Debuggers to Understand Failed Verification Attempts
Introduction
Approach
State Construction
Type Mocking
Program Stubs
Driver
Verification Semantics
Method Calls
Loops
Extended Runtime Checking
Error Validation
Spurious Errors
Invalid Counterexamples
Experience
Related Work
Conclusions
References
Sampling-Based Runtime Verification
Introduction
Preliminaries
Formal Semantics of Sampling-Based Monitoring
Calculating the Sampling Period
Constructing and Composing Sampling-Based Monitor
Optimizing Sampling Period and Its Complexity
Mapping to Integer Linear Programming
Experimental Results
Related Work
Conclusion
References
Case Studies / Tools
Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP
Introduction
Component Assembly
The Reconfiguration Protocol
Specification in LOTOS NT
Verification Using CADP
Related Work
Concluding Remarks
References
Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems
Introduction
The Railway Application Domain
Track-Side Equipment
Route Based Interlocking
Relay Circuits
Relay Circuit Diagrams
Dynamic Behaviour of Relay Circuits
Required System Properties
Informal Description of the Model Generator Tool
Development Overview
Abstract Specification
Circuit Diagrams
Paths in a Diagram
Models
Generator Function
Refinement into a Concrete Specification
Refinement of Sorts
Refinement of Functions
Experiments
Conclusions
References
Relational Reasoning via SMT Solving
Introduction
Background
The Alloy Language
The SMT2 Language
Approach
Type and Relation Declarations
Formulas
Transitive Closure
Integer Expressions
Simplifications
Correctness
Experiments
Related Work
Conclusions
References
Building VCL Models and Automatically Generating Z Specifications from Them
Introduction
VCL Tool
Illustration
Discussion
Related Work
Conclusions and Future Work
References
Experience
The 1st Verified Software Competition: Experience Report
Introduction
The Challenge Problems
The Team Reports
Team anonymousHolHacker (Tom Ridge)
Team Holfoot (Thomas Tuerk)
Team KeY (Vladimir Klebanov, Mattias Ulbrich, Benjamin Weiß)
Team Leino (Rustan Leino)
Team SPARKuLike (Rod Chapman)
Team MonaPoli (Rosemary Monahan, Nadia Polikarpova)
Team Resolve (Derek Bronish)
Team RobArthan (Rob Arthan)
Team VC Crushers (Eyad Alkassar, Ernie Cohen, Mark Hillebrand, Stephan Tobies)
Team VeriFast (Bart Jacobs, Frank Piessens, Jan Smans)
Conclusions
References
Program Compilation and Transformation
Validated Compilation through Logic
Introduction
Extended Front-End
De-compiling Assembly Code
Example Program Transformations
Results
Related Work and Conclusions
References
Certification of Safe Polynomial Memory Bounds
Introduction
The Language
Function Signatures
Proof-Rules
Soundness Theorems
Certification
Case Study
Related Work and Conclusion
References
Relational Verification Using Product Programs
Introduction
Motivating Examples
Program Products
Programming Model
Product Construction
Case Studies
Related Work
Further Work and Conclusions
References
Security
Specifying Confidentiality in Circus
Introduction
Circus
Specifying Confidentiality Properties
The Semantics of -Annotations
Propagation: Divide and Conquer!
Block-Level Verification
Forwards Propagation
Backwards Propagation
Verifying Confidentiality
Confidentiality-Preserving Refinement
Related Work
Conclusions
References
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization
Introduction
A Primer on Virtualization
The Model
Informal Overview of the Memory Model
Formalizing States
Actions
Traces
Isolation Properties
Availability
Related Work
Conclusion and Future Work
References
The Safety-Critical Java Memory Model: A Formal Account
Introduction
Safety-Critical Java Memory Model
Unifying Theories of Programming
Invariants in the UTP
Operation Invariants
State Invariants
A Theory for the Safety-Critical Java Memory Model
Conclusions
References
Process Algebra
Failure-Divergence Refinement of Compensating Communicating Processes
Introduction
Syntax of the Extended cCSP
Failure-Divergence Semantics of Standard Processes
Basic Notations
Semantics of Standard Processes
Failure-Divergence Semantics of Compensable Processes
Refinement Theory and Recursion Semantics
Refinement of Standard Processes
Refinement Order of Compensable Processes
Laws of Long Running Transactions
Case study
Conclusion
References
Termination without $\surd$ in CSP
Introduction
A Selective Overview of CSP
Deadlock, Divergence and Termination
The Standard CSP Semantic Models T, F and N
Infinite Traces
Process Refinement
Denoting Termination
Recasting the Denotational Models of CSP
The Model Tm
The Isomorphism between Tm and T
Persistent Failures versus Stable Failures
The Model Fm
The Isomorphism between Fm and F
Calculating the Fm Semantics of Processes
The Model Nm
The Isomorphism between Nm and N
Calculating the Nm Semantics of Processes
Termination and External Choice
CSP in the Unifying Theories of Programming
Correctness Perspectives
Conclusion
References
Timed Migration and Interaction with Access Permissions
Introduction
Syntax and Semantics of PerTiMo
Safe Access Permissions
Conclusions and Related Work
References
Education
From a Community of Practice to a Body of Knowledge: A Case Study of the Formal Methods Community
Introduction
Community of Practice
Fundamental Elements of a CoP
Cultivating a CoP
Stages of Community Development
Body of Knowledge
Characterising Formal Methods
Organizational Matters
FMBOK Initiative
Formal Model in Z
Conclusions and Future Work
References
Concurrency
Verifying Linearisability with Potential Linearisation Points
Introduction
The Lazy Concurrent Set
Linearisability and Refinement
Local Proof Obligations
Verification of the Case Study
Conclusion
References
Refinement-Based Verification of Local Synchronization Algorithms
Introduction
Synchronization Algorithms for Local Computation Models
The 3-Coloring Problem of a Ring
Synchronization Algorithms
Event-B Overview
The Modelling Process
Implementing the Local Computations Model
The Handshake Algorithm Development
Conclusion and Future Works
References
Simulating Concurrent Behaviors with Worst-Case Cost Bounds
Introduction
A Language for Distributed Concurrent Objects
Operational Semantics
Worst-Case Cost Bounds
Deployment Components
Simulation and Experimental Results
Related Work
Discussion
References
Dynamic Structures
Automatically Refining Partial Specifications for Program Verification
Introduction
Illustrative Example
Language and Abstract Domain
The Analysis
Refining Specifications for Primary Methods
Inferring Specifications for Auxiliary Methods and Loops
Experiments and Evaluation
Related Work and Conclusion
References
Structured Specifications for Better Verification of Heap-Manipulating Programs
Introduction
Motivating Examples
Example 1
Example 2
Structured Specifications
Semantic Model for Structured Formulae
Modular Verification
Building Verification Rules
Entailment for Structured Formula
Experiments
Related Work and Conclusion
References
Verification of Unloadable Modules
Introduction
Problem Statement
Formal Programming Language
Example Program
Specification and Verification Approach
Specification Language
Proof System
Verification Tool
Conclusion and Related Work
References
Model Checking
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking
Introduction
Preliminaries
A Symbolic Transition-Based Generalized Büchi Automata (TGBA) Encoding
A Set of 30 Symbolic Automata Encodings
Experimental Methodology
Experimental Results
Discussion
References
On Combining State Space Reductions with Global Fairness Assumptions
Introduction
Preliminaries
Model Checking with Fairness
Fairness
Model Checking with Fairness
Algorithm for Model Checking with Global Fairness
Model Checking with Symmetry Reduction
Symmetry Reduction with Global Fairness
Partial Order Reduction with Global Fairness
Implementation and Evaluation
Related Work
Conclusion and Future Work
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken