FM 2011: Formal Methods
17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011, Proceedings
Published on 21. June 2011
XIV, 450 pages
978-3-642-21437-0 (ISBN)
Description
This book constitutes the refereed proceedings of the 17th International Symposium on Formal Methods, FM 2011, held in Limerick, Ireland, in June 2011.
The 29 revised full papers presented together with 3 invited talks were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on cyber-physical systems, runtime analysis, case studies/tools, experience, program compilation and transformation, security, progress algebra, education, concurrency, dynamic structures, and model checking.
The 29 revised full papers presented together with 3 invited talks were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on cyber-physical systems, runtime analysis, case studies/tools, experience, program compilation and transformation, security, progress algebra, education, concurrency, dynamic structures, and model checking.
More details
Other editions
Additional editions
Michael Butler | Wolfram Schulte
FM 2011: Formal Methods
17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011, Proceedings
Book
06/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- 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
