Software Engineering and Formal Methods
9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011, Proceedings
Published on 26. October 2011
XIV, 504 pages
978-3-642-24690-6 (ISBN)
Description
This book constitutes the refereed proceedings of the 9th International Conference on Software Engineering and Formal Methods, SEFM 2011, held in Montevideo, Uruguay, in November 2011.
The 22 revised regular papers presented together with 1 short paper, 2 tool papers, and 4 keynote talks were carefully reviewed and selected from 105 initial abstracts and 85 full submissions. Besides the regular session the conference held a special track devoted to "Modeling for Sustainable Development" with 5 accepted papers - selected from 7 submissions - that are also part of this volume. The aim of SEFM is to advance the state of the art in formal methods, to scale up their application in software industry and to encourage their integration with practical engineering methods.
The 22 revised regular papers presented together with 1 short paper, 2 tool papers, and 4 keynote talks were carefully reviewed and selected from 105 initial abstracts and 85 full submissions. Besides the regular session the conference held a special track devoted to "Modeling for Sustainable Development" with 5 accepted papers - selected from 7 submissions - that are also part of this volume. The aim of SEFM is to advance the state of the art in formal methods, to scale up their application in software industry and to encourage their integration with practical engineering methods.
More details
Other editions
Additional editions
Gilles Barthe | Alberto Pardo | Gerardo Schneider
Software Engineering and Formal Methods
9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011, Proceedings
Book
10/2011
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Conference Organization
- Table of Contents
- Keynote Talks
- Formal Methods in Energy Informatics
- Reference
- Formal Methods as a Link between Software Code and Legal Rules
- Motivation
- Formal Methods as a Link between ICT and Law
- Liability Issues in Software Engineering
- Privacy
- Compliance
- Further Challenges
- Conclusion: Interdisciplinarity in Practice
- References
- Developing Model-Checking Mechanisms for ASSL: An Experience Report
- Introduction
- ASSL
- Model Checking with ASSL
- Consistency Checking
- Built-in Model Checker
- External Model Checker
- Post-Implementation Model Checker
- Case Study: Checking Liveness Properties with ASSL
- Conclusion and Future Work
- References
- Models and Communication in the Policy Process
- References
- Regular Papers
- Distributed Implementation of Systems with Multiparty Interactions and Priorities
- Introduction
- Distributed System with Priorities
- Protocol Description
- Correctness
- Experimental Results
- Sensitivity to the Choice of Negotiators
- Example with Priorities: Jukebox System
- Related Work
- Conclusion
- References
- Verification of PLC Properties Based on Formal Semantics in Coq
- Introduction
- Programmable Logic Controller
- Instruction Lists
- Syntax
- Semantics
- Formalization
- Sequential Function Charts
- Syntax
- Semantics
- Tool Support for PLC Verification and Proving Principles
- The CertPLC Tool
- Proof Structure for Inductive Properties
- Case Study
- Related Work
- Conclusions and Future Works
- References
- Broadcast Psi-calculi with an Application to Wireless Protocols
- Introduction
- Psi-calculi
- Broadcast Semantics
- Modelling Network Topology Changes
- The LUNAR Protocol in Psi
- Related Work
- Conclusion
- References
- A Formalisation of Java Strings for Program Specification and Verification
- Introduction
- Background
- Java Strings
- Dynamic Logic for Sequential Java
- Specification of Java Strings
- The Abstract Datatype CharList
- Connecting String and CharList
- String Literals and the String Pool
- Regular Expressions for CharList
- Specification of the Java String API
- Case Studies
- String Distance Measure
- Hash Set
- String Sanitization
- Related Work
- Conclusion and Future Work
- References
- dCTL: A Branching Time Temporal Logic for Fault-Tolerant System Verification
- Introduction
- Preliminaries
- Kripke Structures
- Computation Tree Logic
- A Deontic Computation Tree Logic: dCTL
- Fault Tolerance Reasoning in dCTL
- A Memory Cell
- A Token Ring Protocol
- Expressivity and Complexity of dCTL
- Conclusions and Future Work
- References
- A Machine-Checked Framework for Relational Separation Logic
- Introduction
- Formalization of Relational Separation Logic
- Relational Calculus
- Total Correctness
- Verification of the Schorr-Waite Algorithm
- Beyond Structurally Equivalent Programs
- Related Work
- Conclusion
- References
- A Dataflow Analysis to Improve SAT-Based Bounded Program Verification
- Introduction
- Tight Bounds for Improved SAT-Solving
- Problem Statement
- Propagating Values in DynAlloy Programs
- Effective Removal of Variables Using Dataflow Analysis
- Loop Optimization
- Empirical Evaluation
- Conclusions and Further Work
- References
- Reverse Hoare Logic
- Introduction
- Definitions
- Program Logic
- Case Studies
- Picking Random Numbers
- Arrays
- Iteration
- Shuffle
- Weakest Postcondition Calculus
- Soundness and Completeness
- Related Work
- Conclusions
- References
- Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods
- Introduction
- The iSAT Algorithm for SAT Modulo ODE
- Overview of VNODE-LP
- Using Bracketing Systems as Enclosures
- Deducing Trajectory Directions
- Experiments
- Conclusion
- References
- Verification of B+ Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving
- Introduction
- B+ Trees and Approach
- Algorithms
- Verification Approach
- Algebraic Formalization of Pointer Structures
- Introduction to Parametric Shape Analysis
- Formalization and Verification of B+ Tree Invariants
- Tree Shape
- Balance
- Sorting
- Elements
- Node Sizes
- Results and Experiences
- Conclusion
- References
- Runtime Verification of Component-Based Systems
- Introduction
- BIP - Behavior Interaction Priority
- Component-Based Construction
- An RV Framework for Component-Based Systems
- Specifications for Component-Based Systems (CBS)
- Verification Monitors DBLP:conf/rv/FalconeFM09
- Runs and Traces of BIP Systems
- Verifying the Runtime Behavior of BIP Systems
- Extraction of Needed Information
- Instrumentation of Atomic Component
- Creating an Atomic Component from a Monitor
- Connections
- Summary and Discussion
- Implementation and Evaluation
- RV-BIP: A Tool for Runtime Verification of BIP Systems
- Case Study: A Robotic Application
- Related Work
- Conclusion and Future Work
- References
- Translating Alloy Specifications to UML Class Diagrams Annotated with OCL
- Introduction
- Alloy
- Alloy and UML+OCL Integration in MDE
- Related Work
- Model Transformation from Alloy to UML+OCL
- Characterizing Source Models
- From Alloy to UML Class Diagrams
- From Alloy to OCL
- Concluding Remarks and Future Work
- References
- Safe Distribution of Declarative Processes
- Introduction
- Related Work
- Dynamic Condition Response Graphs
- Projection and Composition
- Projection
- Composition
- Safe Distributed Synchronous Execution
- Example
- Conclusion
- References
- Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving
- Introduction
- Rule Verification in Atelier B
- The B Set Theory
- The Atelier B Proof Assistant
- The BCARe Environment
- Rationale for Designing BCARe
- The BCoq Embedding
- Rewrite Rule Verification
- Rule Typechecking
- Well-Definedness Verification
- Rule Verification
- Examples
- Automated Verification of Proof Rules
- Verification Using Ltac
- Verification Using Zenon
- Benchmarks
- Conclusion
- References
- Hybrid Specification of Reactive Systems: An Institutional Approach
- Introduction
- A Specification Methodology
- Hybrid Specifications (Stage I)
- States-as-Algebras Models (Stage II)
- Foundations
- Going ``institutional
- Translating to FOL (Stage III)
- Tool Support
- Conclusions
- References
- Leveraging State-Based User Preferences in Context-Aware Reconfigurations for Self-Adaptive Systems
- Introduction
- Motivating Scenario
- Approach
- Basic Models
- Operative Context Model
- System and System Variants
- User Context Model
- Problem Formalization
- Evaluation
- Case Study
- Experiment
- Related Work
- Conclusions
- References
- Context-Bounded Model Checking of LTL Properties for ANSI-C Software
- Introduction
- From LTL to Monitor Threads
- Linear-Time Temporal Logic
- Büchi Automata
- Monitor Threads
- Model-Checking LTL Properties with ESBMC
- ESBMC
- Checking LTL Properties against a C Program
- Optimizing State Space Exploration
- Hashing Symbolic States
- Selection of Hash Function
- Comparison with Partial Order Reductions
- Experimental Evaluation
- Related Work
- Conclusions and Future Work
- References
- Modular Modelling of Software Product Lines with Feature Nets
- Introduction
- Software Product Line Modelling Challenge
- Feature Nets
- Modular Modelling
- Feature Net Composition
- Correctness
- Mathematical Preliminaries
- Preservation of the Core Behaviour for the Original Features
- Preservation of the Delta Behaviour for the Combined Features
- Safety of the Core Behaviour for the Combined Features
- Related Work
- Conclusion and Future Work
- References
- Synchronizing Asynchronous Conformance Testing
- Introduction
- Preliminaries
- Adapting IOCO to Asynchronous Setting
- Test Cases for Internal Choice Implementations
- Asynchronous Communication
- Sound Verdicts of Internal Choice Test Cases
- Adapting Asynchronous Setting to IOCO
- Input Output Conformance
- Synchronizing Theorem for ioco
- Necessary and Sufficient Conditions
- Conclusions
- References
- Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications
- Formalizing MapReduce Applications
- Formalizing MapReduce Applications in Coq
- Abstract Model of Hadoop MapReduce Computation
- Proving WordCount Specifications
- Proving InvertedIndex Specifications
- Extracting Haskell Programs from Coq Proofs
- Verification of Java Programs by Krakatoa
- Experiments
- Related Work
- Conclusion and Future Work
- References
- ProMoVer: Modular Verification of Temporal Safety Properties
- Introduction
- ProMoVer: A User's View
- Framework for Modular Specification and Verification
- Program Model and Logic
- Compositional Verification
- The ProMoVer Tool
- Experimental Results with ProMoVer
- Conclusion
- References
- Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques
- Verification as a Matter of Course
- An Example Session with Eve
- Related Work
- The Tools of Eve
- The Advantages of Being Static and Dynamic
- The Design of an Integrated Verification Environment
- Correctness Scores for Proofs and Testing
- Usage Scenarios
- Conclusions
- References
- Short Papers
- Efficient Computation of Dominance in Component Systems (Short Paper)
- Introduction
- Strong Dependencies and Dominators
- Dominance in Strong Dependency Graphs and Flow Control Graphs
- Discussion
- References
- Tool Papers
- The Boogie Verification Debugger (Tool Paper)
- High-Level architecture
- BVD
- Insert example
- Computing Memory Contents
- Displaying States and Access-Path Values
- Complex Data Types and Search
- Plug-in Programmer Interface
- Related Work
- Conclusions and Future Work
- References
- Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude
- Introduction
- Real-Time Maude
- Effort/Flow Modeling of Interacting Hybrid Systems
- Executing Interacting Hybrid Systems
- The HI-Maude Tool
- Representing Continuous Values
- Modeling
- Formal Analysis in HI-Maude
- Soundness and Completeness of HI-Maude Analyses
- The Real-Time Maude Semantics of HI-Maude
- Case Study: The Human Thermoregulatory System
- The Human Thermoregulatory System
- Effort/Flow Modeling of the Human Thermoregulatory System
- Formal Analysis
- Concluding Remarks
- References
- Special Track: "Modelling for Sustainable Development"
- Towards an Agent-Based Methodology for Developing Agro-Ecosystem Simulations
- Introduction
- Agent-Based Simulations of Agro-Ecosystems
- The Methodological Framework
- Case Study
- Case Study Conclusions
- Conclusions
- References
- Development Policy Analysis in Mali: Sustainable Growth Prospects
- Introduction
- An Integrated Resource-Based Approach
- Approach and Method
- The Model
- Base Run
- Data and Validation
- Business as Usual Scenario
- Alternative Scenarios
- Conclusions
- References
- Using System Dynamics to Assess the Role of Socio-economic Status in Tuberculosis Incidence
- Introduction
- System Dynamics Modeling in Public Health
- Model Proposal
- Social Determinants and Risk Factors
- Model Components
- Simulation Results
- Conclusions
- References
- Energy Consumption and CO2 Emissions of Beijing Heating System: Based on a System Dynamics Model
- Introduction
- Case study of Beijing City
- Model Structure
- Major Assumptions
- Construction of the Model
- Check on Model
- Scenario Analysis
- Baseline Scenario
- Less Building Scenario
- Energy Efficiency Scenario
- Conclusions
- References
- A Formal Approach to Analysing Knowledge Transfer Processes in Developing Countries
- Introduction
- Related Work
- Current Understanding of Knowledge Transfer
- A Formal Approach for Knowledge Transfer
- A Formal Model for Knowledge Transfer
- CSP
- Formalising Interactions
- Knowledge Seeker Process
- Knowledge Recipient Process
- Knowledge Provider Process
- Needs Recipient Process
- Needs Transmitter Process
- Knowledge Repository Process
- Formal KT Model
- Analysing the Knoweldge Transfer Model
- A Case Study at Lotus
- A KT System with a Shy Seeker
- A KT System with an Unwilling Provider
- A KT System without a Repository
- Analysing Transfer Deadlocks and Livelocks
- Conclusion and Future Work
- References
- Author Index
