Software Engineering and Formal Methods

Name: Software Engineering and Formal Methods | 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011, Proceedings

Gilles Barthe Alberto Pardo Gerardo Schneider(Herausgeber*in)

Springer (Verlag)

Erschienen am 26. Oktober 2011

XIV, 504 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-24690-6 (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
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

Systemvoraussetzungen

Als PDF speichern Als Link merken