Integrated Formal Methods

Name: Integrated Formal Methods | 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings

John Derrick Stefania Gnesi Diego Latella Helen Treharne(Herausgeber*in)

Springer (Verlag)

1. Auflage

Erschienen am 26. Juni 2012

XII, 360 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-30729-4 (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
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

Systemvoraussetzungen

Als PDF speichern Als Link merken