Integrated Formal Methods
9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings
Published on 26. June 2012
XII, 360 pages
978-3-642-30729-4 (ISBN)
Description
This book constitutes the refereed proceedings of the 9th International Conference on Integrated Formal Methods, IFM 2012, held Pisa, Italy, in June 2012. The 20 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 59 submissions. The papers cover the spectrum of integrated formal methods, ranging from formal and semiformal notations, semantics, proof frameworks, refinement, verification, timed systems, as well as tools and case studies.
More details
Other editions
Additional editions
John Derrick | Stefania Gnesi | Diego Latella
Integrated Formal Methods
9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings
Book
06/2012
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Foreword
- Preface
- Organization
- Contents
- Contribution to a Rigorous Analysis of Web Application Frameworks
- Introduction
- Concrete Goals and Results So Far
- Modeling Browser Components
- Browsing Context
- Renderer
- Event Loop
- A High-Level WebServer Model
- Functional Request-Reply Web Server View
- Refinement for File Transfer Execution
- Refinement for Common Gateway Module Execution
- Refinement for Scripting Module Execution
- The Challenge of Accurate Analysis
- References
- Process Algebra for Event-Driven Runtime Verification: A Case Study of Wireless Network Management
- References
- Translating TLA+ to B for Validation with ProB
- Introduction and Motivation
- An Example Translation from TLA+ to B
- The Translation from TLA+ to B
- Type System
- Translation Rules
- Implementation and Experiments
- More Related Work, Discussion and Conclusion
- References
- Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands
- Introduction
- A Real-Time Framework
- Intervals, Streams and Interval Stream Predicates
- Evaluating State Predicates over an Interval
- Chop, Iterated Chop and Alternation
- Multi-time-Band Systems
- Sampling and Time Bands
- Teleo-reactive Programs
- Rely/Guarantee Reasoning
- Rely/Guarantee Rules
- Proof of Safety for mp
- Conclusions
- References
- Safety and Line Capacity in Railways - An Approach in Timed CSP
- Introduction
- Railway Terminology and the Double Junction Example
- Modelling Railways for Safety in CSP
- Timed CSP and Timed Traces
- Modelling Timed Behaviours of Railway System
- Modelling Railway Capacity
- Capacity Semantically
- Capturing Storage and Increase in Timed Csp
- Capacity via Refinement
- Studying Safety and Capacity in the Context of the Double Junction
- Summary and Future Work
- References
- Refinement-Based Development of Timed Systems
- Introduction
- Related Work
- Case-Study: Safety Related Controller Design
- Preliminaries
- Preliminaries of Event-B
- Preliminaries of UPTA
- Mapping from Event-B Models to UPTA
- Abstract Event-B and UPTA Specifications of Safety Controller
- Proving Refinement of Timed Systems
- Superposition Refinement of UPTA
- Event-B and UPTA Refinement of Safety Controller
- Conclusion and Future Work
- References
- Analysing and Closing Simulation Coverage by Automatic Generation and Verification of Formal Properties from Coverage Reports
- Introduction
- Background
- Coverage
- Model Checking
- Related Work
- Methodology
- The Principle of Temporal Induction
- Application of the Methodology
- Further Considerations
- Implementation
- Experiments and Results
- Discussion
- Conclusion
- References
- Model Checking as Static Analysis: Revisited
- Introduction
- Modal -Calculus
- Kripke Structures
- Syntax and Semantics of the Modal -Calculus
- Logical Approach to Static Analysis
- Alternation-Free Least Fixed Point Logic
- Succinct Fixed Point Logic
- Model Checking as Static Analysis
- Conclusion
- References
- Formal Verification of Compiler Transformations on Polychronous Equations
- Introduction
- An Equational Model of Synchronous Programs
- An Equational Model of the Synchronous Program Behavior
- Overview of the SIGNAL Language Features
- PDS Model of SIGNAL Programs
- Formally Verified Compilation Approaches
- Definition of Correct Translation: Refinement
- Proving Refinement by Simulation
- Composition of Compilation Phases
- Proving the SIGNAL Compiler
- Implementation of Symbolic Simulation with SIGALI
- Proving the Compiler Transformations
- Related Work and Conclusions
- References
- Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples
- Introduction
- Context-Bounded Model Checking with ESBMC
- EZProofCMethod
- First Step: Code Preprocessing
- Second Step: Model Checking with ESBMC
- Third Step: Code Instantiation
- Fourth Step: Code Execution and Confirmation of Errors
- Experimental Results
- Planning and Design the Experiments
- Experiment's Execution and Results Analysis
- Related Work
- Conclusions and Future Work
- References
- MULE-Based Wireless Sensor Networks: Probabilistic Modeling and Quantitative Analysis
- Introduction
- Probabilistic Rewrite Theories and PMaude
- Grouping Nodes in MULE-Based Sensor Networks
- A Declarative Model of MULE-Based Communication
- Combining Declarative and Operational Models
- Quantitative Analysis of the Combined Model
- Conclusion
- References
- Mechanized Extraction of Topology Anti-patterns in Wireless Networks
- Introduction
- Related Work
- Identifying Topology Anti-patterns
- Minimization
- Isolation
- Discussion
- Case Studies
- Experimental Setup
- PRISM
- Verifying Trickle
- Verifying LMAC
- Handling Multiple Faults
- Comparison to Diagnosis
- Conclusions
- References
- A Proof Framework for Concurrent Programs
- Introduction
- Framework Basics
- An Example: Bakery Algorithm
- Framework with Thread Synchronisation
- Related Work
- Conclusions and Future Work
- References
- A UTP Semantics of pGCL as a Homogeneous Relation
- Introduction
- Background
- UTP
- pGCL
- Probabilistic UTP
- Observing Distributions
- Assignment
- UTP Semantics of pGCL
- Deterministic Constructs
- Non-deterministic Choice
- Generic Choice
- The Linkage between Other Semantic Models and Ours
- Conclusion and Future Work
- References
- Behaviour-Based Cheat Detection in Multiplayer Games with Event-B
- Introduction
- Behaviour-Based Cheat Detection with Formal Methods
- Cheating Behaviour Modelling
- Cheating Behaviour in Event-B
- Production of Cheat Detector
- Merits of Implementation
- Validation of the Framework
- Related Work
- Conclusions
- References
- Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems
- Introduction
- Preliminaries
- Event-B
- Register-Voice Interactive Systems
- From Event-B to Structured rv-IS
- An Example - A Simple File Transfer Protocol
- Conclusions
- References
- Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B
- Introduction
- Modelling in Event-B
- Service-Oriented Systems
- Service Orchestration
- Towards Formalisation of Service Orchestration
- Modelling the Dynamic Service Architecture
- Case Study
- Probabilistic Verification in Event-B
- Probabilistic Event-B
- Case Study: Quantitative Modelling and Verification
- Related Work and Conclusions
- References
- Partially-Supervised Plants: Embedding Control Requirements in Plant Components
- Introduction
- Supervisory Control Theory
- Supervisor Synthesis for a Patient Support System
- Process-Theoretic Approach to Controllability
- Partially-Supervised Plants
- Concluding Remarks
- References
- Early Fault Detection in Industry Using Models at Various Abstraction Levels
- Introduction
- Control Components for an Interventional X-Ray System
- Modelling and Analysing Requirements
- Modelling and Analysing Designs
- Comparing Requirements and Designs
- Detailed Design with ASD
- Conclusions and Further Work
- References
- PE-KeY: A Partial Evaluator for Java Programs
- Introduction
- Calculus
- Dynamic Logic
- Sequent Calculus
- Compilation Rules
- Implementation and Experiments
- Related Work
- Conclusions and Future Work
- References
- Specification-Driven Unit Test Generation for Java Generic Classes
- Introduction
- Specifications of Generic Data Types
- Semantics
- Generation of Abstract Tests
- Tests for Parameterized Specifications
- Generation Technique
- From Algebraic Specifications to Alloy and Back
- From Abstract Tests to JUnit Tests
- Refinement Mappings
- Mock Classes and JUnit Tests
- Evaluation
- Conclusions and Future Work
- References
- Specifying UML Protocol State Machines in Alloy
- Introduction
- Case Study
- Preliminary Concepts
- UML Protocol State Machines
- Alloy
- Specifying Protocol State Machines in Alloy
- Importing UML Class Diagram into Alloy
- PSM's States and Transitions
- Finite Execution Traces
- Verification and Validation of UML Diagrams
- Implementation
- Related Work
- Conclusions and Future Work
- References
- Patterns for a Log-Based Strengthening of Declarative Compliance Models
- Introduction
- Basic Concepts and Related Work
- Declare
- Approach
- Existence Constraints
- Relation Constraints
- Methodology
- Case Study
- Conclusion
- References
- A Formal Interactive Verification Environment for the Plan Execution Interchange Language
- Introduction
- PLEXILOverview
- PLEXIL5
- Architecture and Design
- User Interaction
- Formal Analysis in PLEXIL5
- Simulation and Debugging
- Model Checking
- Semantic Validation
- A Case Study
- Model Description
- Verification
- Related Work and Conclusion
- References
- Author Index
