Formal Methods and Software Engineering
13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings
Published on 23. October 2011
XIV, 670 pages
978-3-642-24559-6 (ISBN)
Description
This book constitutes the refereed proceedings of the 13th International Conference on Formal Engineering Methods, ICFEM 2011, held in Durham, UK, October 2011. The 40 revised full papers together with 3 invited talks presented were carefully reviewed and selected from 103 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on formal models; model checking and probability; specification and development; security; formal verification; cyber physical systems; event-B; verification, analysis and testing; refinement; as well as theorem proving and rewriting.
More details
Other editions
Additional editions
Shengchao Qin | Zongyan Qiu
Formal Methods and Software Engineering
13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings
Book
10/2011
Springer
€53.49
Shipment within 7-9 days
Content
- Title Page
- Preface
- Organization
- Table of Contents
- Invited Talks
- Towards a Signal Calculus for Event-Based Synchronous Languages
- Introduction
- Pure Signals and Event Guards
- Instantaneous Reactions: I-Calculus
- Algebraic Semantics
- Parallel
- Guard
- Concealment
- Primitives
- Dependence
- Additional Laws
- Normal Form for I-Calculus
- Discussion
- References
- Reasoning about Programs Using a Scientific Method
- Poirot-A Concurrency Sleuth
- Formal Models
- Context-Based Behavioral Equivalence of Components in Self-Adaptive Systems
- Introduction
- Illustrating Example
- PobSAM
- Formal Modeling of Collaborating UAVs
- Statebased Bisimulation
- Context-Specific Behavioral Equivalence
- Context-Specific Behavioral Equivalence of Actions
- Context-Specific Behavioral Equivalence of Governing Policies
- Context-Specific Behavioral Equivalence of Adaptation Policies
- Context-Specific Behavioral Equivalence of Configurations and Managers
- Related Work
- Conclusions
- References
- Towards a Practical Approach to Check UML/fUML Models Consistency Using CSP
- Introduction
- Background
- fUML
- CSP
- Approach Overview
- The Model Formalizer
- Behavioural Consistency Checking
- Formalization and Model Checking Feedback
- Formalization Report
- Model Debugger
- Approach Implementation
- Related Work
- Conclusion and Future Work
- References
- The Safety-Critical Java Mission Model: A Formal Account
- Introduction
- Preliminaries
- Safety-Critical Java
- Circus and OhCircus
- Framework and Application Models
- Safelet Model
- Mission Sequencer Model
- Mission Model
- Handler Models
- Conclusions
- References
- Is There Evolution Before Birth? Deterioration Effects of Formal Z Specifications
- Introduction
- Perfection or Decay
- Back to the Roots
- The Role of Formal Design
- On the Search for Measures
- Specification Measures
- Slice-Based Coupling and Cohesion Measures
- Specification Slicing
- Evaluation
- Experimental Subject
- The Study
- Results
- An Extended Model of Evolution
- Conclusion
- References
- Asynchronous Communication in MSVL
- Introduction
- Projection Temporal Logic
- Syntax
- Semantics
- Modeling, Simulation and Verification Language
- Asynchronous Communication
- Process
- Channel
- Communication Commands
- An Application
- An Example of Electronic Contract Signing Protocol
- Modeling, Simulation and Verification with MSVL
- Conclusion
- References
- Model Checking and Probability
- Verification of Orchestration Systems Using Compositional Partial Order Reduction
- Introduction
- Orchestration Language Orc
- Syntax
- Semantics
- Hierarchical Concurrent Processes (HCP)
- Compositional Partial Order Reduction (CPOR)
- Classic POR and CPOR
- CPOR Algorithm
- Soundness
- Evaluation
- Related Work
- Conclusion
- References
- Domain-Driven Probabilistic Analysis of Programmable Logic Controllers
- Introduction
- Preliminaries
- Symbolic Framework
- Modeling Uncertainty of PLC Systems
- Construction of Hidden Markov Model
- Solving the Hidden Markov Model
- Construction of Combined Regular Markov Model
- Property Analysis with PRISM
- Case Studies
- Conclusion
- References
- Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications
- Introduction
- Preliminaries
- Distributed Probabilistic Control Hybrid Automata
- Quantified Bounded Linear Temporal Logic
- Bayesian Statistical Model Checking
- Case Study: Smart Grid
- Conclusions
- References
- PRTS: An Approach for Model Checking Probabilistic Real-Time Hierarchical Systems
- Introduction
- Basic Concepts
- Syntax of PRTS
- Operational Semantics
- Abstraction
- Verification
- Implementation and Evaluation
- Related Work
- Conclusion
- References
- Specification and Development
- Integrating Prototyping into the SOFL Three-Step Modeling Approach
- Introduction
- Related Work
- SOFL Three-Step Approach and Its Problems
- SOFL Three-Step Approach
- Problem Descriptions
- Prototyping
- Proposed Framework for Integration
- Phase I
- Phase II
- Phase III
- Case Study
- Phase I
- Phase II
- Phase III
- Discussion
- Conclusion
- References
- A Deterministic Interpreter Simulating a Distributed Real Time System Using VDM
- Introduction
- The VDM Technology
- Interpreting Sequential VDM Models
- Interpreting Concurrent Real-Time Models
- Creating a Deterministic Debugger
- Deterministic Debugging
- Debugging User Interface
- Debugging Multi-threaded Applications
- Related Work
- Concluding Remarks
- References
- On Fitting a Formal Method into Practice
- Introduction
- Event-B in an Industrial Development Process
- Event-B
- Fitting Event-B into Development Practice
- Problem Frames
- The Cruise Control System
- Relating Problem Frames to Event-B Models
- Problem Frames Description of the Cruise Control
- Relating Problem Frames Concepts to Event-B Concepts
- A Matching Event-B Model of the Cruise Control
- Elaboration in Event-B
- Verifying Deadlock Freedom
- Conclusion
- References
- A Formal Engineering Approach to High-Level Design of Situation Analysis Decision Support Systems
- Introduction
- Problem Description
- Design and Validation of SADS Systems
- Related Work
- Abstract State Machines
- ASM Systems Engineering Method
- Distributed ASMs
- The CoreASM Extensible Architecture
- Extensible Language
- Extensible Engine
- Application Scenario
- Vessels
- Observers
- Rendezvous Awareness
- The SA Plugin
- Extending the CoreASM Engine
- Visualization
- Situation Analysis
- Conclusions and Future Work
- References
- Security
- Conformance Checking of Dynamic Access Control Policies
- Introduction
- Context
- sif
- Evolving Access Control
- RBAC Policy Editing Tool
- Constraints and Requirements
- RBAC
- An Alloy Representation of RBAC
- Adding Sessions
- Gauge
- Overview
- Instances
- Evaluation
- Types
- Scalability
- Optimisation
- Conclusions and Further Work
- References
- A Knowledge-Based Verification Method for Dynamic Access Control Policies
- Introduction
- Related Work
- Definitions
- Access Control Policy
- Access Control System
- Query Language
- Model-Checking and Strategy Synthesis
- Finding Effective Propositions
- Pseudocode for Finding Strategy
- Knowledge vs. Guessing in Strategy
- Experimental Results
- Conclusion and Future Work
- References
- Validation of Security-Design Models Using Z
- Introduction
- Illustrative Example: Medical Information System
- Translating the Functional Model into Z
- The Security Kernel
- Permissions
- Role Hierarchy
- Action Hierarchy
- Roles, Users and Sessions
- Putting It All Together
- Linking Functional and Security Models
- Validating and Animating Secure Operations
- Normal Behaviour
- Analysing a Malicious Behaviour
- Related Work
- Conclusion and Future Work
- References
- Formal Verification
- Mutation in Linked Data Structures
- Introduction
- Separation Logic
- Mutation: Reasoning about Shape and Data
- Heaplet Analysis and Heap Decomposition
- Heaplet Attraction, Cancellation and Fertilisation
- An Example General Decomposition
- Towards a Generalisation of Mutation
- Implementations and Results
- Related and Future Work
- Conclusion
- References
- Contract-Based Verification of Simulink Models
- Introduction
- Simulink
- Contracts in Simulink
- Synchronous Data Flow Graphs
- The Sequential Language
- Translation of SDF Graphs
- Correctness of the Translation
- SDF Graph Representation of Simulink Models
- Mapping Simulink Blocks to Nodes
- Mapping a Subsystem Contract Description to an SDF Graph
- Verification with Respect to Contracts
- Tool Support
- Example of Subsystem Refinement
- Conclusions
- References
- Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units
- Introduction
- Background
- Using Positive Equality to Formally Verify Pipelined Processors
- Abstracting a Single Reconfigurable Functional Unit
- The ADRES Reconfigurable Architecture
- Techniques for Abstracting Arrays of Reconfigurable Functional Units
- Detailed Abstract Modeling of the Array of Reconfigurable Functional Units
- Abstracting the Entire Array of Reconfigurable Functional Units with One FSM
- Results
- Conclusion
- References
- Architectural Verification of Control Systems Using CSP
- Introduction
- Simulink and the Verification of Control Systems
- Verification of Control Systems
- A Strategy to Verify [acas]Control System Designs
- Mapping Control Law Diagrams to CSP
- Mapping Architectural Requirements to CSP
- Defining Properties
- Abstraction and Validation
- Tool Support and Completeness
- [jbjj]VerifyingValidating a Fly-by-Wire Elevator Control System
- Validation and Results
- Related Work
- Conclusion
- References
- Symbolic Execution of Alloy Models
- Introduction
- Background and Illustrative Example
- Symbolic Execution Basics
- Alloy Basics
- Illustrative Example: Symbolic Execution for Alloy
- Symbolic Execution of Alloy Formulas
- Symbolic Alloy Module
- User Modifications to Alloy Model
- Mechanically Generated Facts
- Alloy Analyzer Usage
- Case Studies
- Red-Black Trees
- Colored List
- Fibonacci Series
- Traditional Symbolic Execution of Imperative Code
- Related Work
- Conclusion
- References
- Cyber Physical Systems
- Distributed Theorem Proving for Distributed Hybrid Systems
- Introduction
- Related Work
- Preliminaries: Quantified Differential Dynamic Logic
- RevisedQdL Proof Calculus
- Working Outside-In
- A Note about Capture
- Assignment
- Equality Substitution
- Differential Equations
- Eliminating Index Variables
- Real Arithmetic
- Proving in KeYmaeraD
- Strategy Language
- Example: Instantiation
- Arithmetic
- Input Formulas
- Case Study
- Conclusions and Future Work
- References
- Towards a Model Checker for NesC andWireless Sensor Networks
- Distributed Theorem Proving for Distributed Hybrid Systems
- Introduction
- Related Work
- Preliminaries: Quantified Differential Dynamic Logic
- Revised Proof Calculus
- Working Outside-In
- A Note about Capture
- Assignment
- Equality Substitution
- Differential Equations
- Eliminating Index Variables
- Real Arithmetic
- Proving in KeYmaeraD
- Strategy Language
- Example: Instantiation
- Arithmetic
- Input Formulas
- Case Study
- Conclusions and Future Work
- References
- Introduction
- Preliminaries
- The NesC Language
- TinyOS and Its Execution Model
- Formalizing Sensors with NesC Programs
- Formalizing Wireless Sensor Networks
- Implementation and Evaluation
- Conclusion
- References
- Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks
- Introduction
- Related Work
- Preliminaries
- Formalization of Discrete Random Variables and Verification of their PMF
- Formalization and Verification of Expectation Properties for Discrete Random Variables in HOL
- Coverage-Based Randomized Scheduling Algorithm
- Overview of the Coverage-Based Randomized Scheduling Algorithm
- Formalization of the Network Coverage Intensity
- Formalization of the Average Detection Delay
- Formal Verification of the Random Scheduling Algorithm
- Formal Verification of the Network Coverage Intensity
- Formal Verification of the Average Detection Delay
- Conclusions
- References
- An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres
- Introduction
- Abstract Model
- Traffic Snapshot
- View
- A Multi-lane Spatial Logic
- Controllers
- Changing Lanes with Perfect Knowledge
- A More Realistic Approach for Changing Lanes
- Safety Proof
- Safety Proof for Changing Lanes with Help
- Conclusion
- References
- Event-B
- Formal Derivation of a Distributed Program in Event B
- Introduction
- Background
- Modelling and Refinement in Event B
- Modelling Modular Systems in Event B
- Modelling of a Leader Election Protocol
- Abstract Model of Leader Election
- Decentralising Leader Election
- Refining Inter-process Communication
- Deriving Distributed Implementation
- System Architecture
- Decomposition of the Leader Election Model
- Towards Runnable Code
- Proof Statistics
- Conclusions
- References
- From Requirements to Development: Methodology and Example
- Introduction
- Methodology
- The Requirement Document
- The Refinement Strategy
- Some Rules
- Modeling with Event-B [1] and Proving with the Rodin Platform [2]
- AfterModeling
- The Example
- Main Purpose of System
- The Requirement Document
- Comments about the Previous Requirements
- Refinement Strategy
- Refinement Strategy Synthesis
- Formal Development
- Proof Statistics
- Timing and Determinism Issues
- Related Work
- Conclusion
- References
- Reasoning about Liveness Properties in Event-B
- Introduction
- Background
- The Event-B Modelling Method
- Temporal Logic
- Proof Rules
- Proof Obligations
- Proof Rules
- Tool Support
- Examples
- Peterson's Algorithm
- Device Calibration
- Related Work
- Conclusions
- FutureWork
- References
- Verification, Analysis and Testing
- Extracting Significant Specifications from Mining through Mutation Testing
- Introduction
- Background
- Past-Time Temporal Specification
- Specification Significance
- Identifying Significant Specifications
- Mutation Testing
- Simulating Specification Violation through Program Mutation
- Generating Replacement Objects
- Exploring Early Pruning
- Specification Refinement
- Evaluation
- Java API Rules
- Verification Using Java API Rules
- Related Work
- Conclusion
- References
- Developer-Oriented Correctness Proofs A Case Study of Cheney's Algorithm
- Introduction
- Dissecting Cheney's Algorithm
- The Three Main Aspects of the Algorithm
- Implementation
- Values, Pointers, and Objects
- The Structure of the Half-Spaces
- Queue Structure
- The Object Graph
- The Forwarding Pointers
- Remaining Free Space
- Assembling the Correctness Proof
- The Specification of collect
- The Loop Invariant and Proof of collect
- The copy ref Function
- Related Work
- Conclusion
- References
- Static Analysis of String Values
- Introduction
- Running Examples
- Abstract Interpretation
- Syntax
- Concrete Domain and Semantics
- Concrete Domain
- Semantics
- Abstract Domains and Semantics
- Character Inclusion
- Prefix and Suffix
- Bricks
- String Graphs
- Discussion: Relations between the Four Domains
- RelatedWork
- Conclusion and FutureWork
- References
- A Theory of Classes from the Theoretical Foundations of LePUS3
- Introduction
- Typed Predicate Logic
- Propositions
- Types
- Specifications
- Toward a Theory of Classes
- Classes and Hierarchies
- Methods and Clans
- Predicates
- Reasoning about Design Patterns
- Conclusion
- References
- Differencing Labeled Transition Systems
- Introduction
- Related Work
- A Motivating Example
- The SpecDiff Approach
- Overview of SpecDiff
- Syntax of CSP#
- Operational Semantic of CSP#
- Comparing Configuration Graphs and Labeled Transition Systems
- Analyzing the LTS Differences
- Evaluation
- The Effectiveness of SpecDiff
- The Robustness of SpecDiff
- Threats to Validity
- Conclusions and Future Work
- References
- Refinement
- Developing a Consensus Algorithm Using Stepwise Refinement
- Introduction
- The Floodset Algorithm
- Event-B
- Development
- The Initial Machine
- The First Refinement: Introducing Phase Specifications
- Identifying Live Processes: X2
- Homogenising the Events: X3
- Refining Out the Saturation Assumption: X4
- Implementing the Round Event: X5
- Discussion and Conclusions
- References
- Refining Nodes and Edges of State Machines
- Introduction
- State Machines
- Refinement
- Development of a Sequential Algorithm
- Design of a Controller
- Conclusion
- References
- Managing Complexity through Abstraction: A Refinement-Based Approach to Formalize Instruction Set Architectures
- Introduction
- Event-B and the Rodin Development Platform
- Literature Review
- The MIDAS and CRISP ISA Models
- Refinement Strategy
- Modeling the MIDAS ISA in Event-B
- Modeling the CRISP ISA in Event-B
- The Generic Modeling Template
- Structure of the Generic Modeling Template
- Generalization of Internal Storage Options
- Modeling the XCore ISA in Event-B
- Summary
- Conclusion
- References
- A Language for Test Case Refinement in the Test Template Framework
- The Process of Model-Based Testing
- The Test Template Framework
- A Method for Test Case Refinement
- Fastest Test Case Refinement Language
- An Example of a Refinement Rule
- The Basic Structure of a Refinement Rule
- Refinement Laws
- More Examples and Features
- A Case Study
- Related Work
- Conclusions
- References
- Theorem Proving and Rewriting.
- Automating Algebraic Methods in Isabelle
- Introduction
- Preliminaries
- Warm-Up: Three Proofs in Kleene Algebra
- Modal Semirings and Kleene Algebras
- Dynamic Algebras and Segerberg's Formula
- TerminationandL¨ob's Formula
- Discussion and Conclusion
- References
- Term Rewriting in Logics of Partial Functions
- Introduction
- Abstract Syntax
- Types and Terms
- An Example Signature
- Semantics
- Isabelle/HOL
- Option Types
- Denotations of Types and Terms
- An Example Structure
- Substitutions
- Term Rewriting
- Rewriting Terms to Equivalent Terms
- Directed Rewriting
- Rewriting Subterms
- Safety
- Practical Relevance
- Proving User Supplied Rules Sound
- Related Work
- Conclusions and Future Work
- References
- Synchronous AADL and Its Formal Analysis in Real-Time Maude
- Introduction
- Preliminaries on AADL, Real-Time Maude, and PALS
- Synchronous AADL
- An Avionics Example
- Real-Time Maude Semantics of Synchronous AADL
- Formal Analysis of Synchronous AADL Models
- Verifying the Active Standby System
- The SynchAADL2Maude Tool
- Related Work
- Concluding Remarks
- References
- Author Index
