Formal Methods: Foundations and Applications

Name: Formal Methods: Foundations and Applications | 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers

Jim Davies Leila Silva Adenilso Simao(Herausgeber*in)

Springer (Verlag)

Erschienen am 17. März 2011

VIII, 291 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-19829-8 (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 Page
Preface
Organization
Table of Contents
Directed Model Checking for B: An Evaluation and New Techniques
Introduction
Combining Depth-First and Breadth-First for Improved Model Checking
Depth-First versus Breadth-First: An Empirical Evaluation
The Models
The Results
Evaluating Directed Model Checking
Future and Related Work and Conclusion
References
Midlet Navigation Graphs in JML
Introduction
MIDP Infrastructure
Navigation Graphs
Navigation Graphs in JML
Relevant API Methods
Midlet Annotations - The Mobius Case Study
Specification and Verification Issues
Evaluation and Discussion
References
Runtime Verification for Generic Classes with CONGU2
Introduction
Overview of the ConGu Approach
Runtime Conformance of Programs against Modules
Object Properties Induced by Specifications
Checking Object Properties
The New ConGu Tool
Analysis of Refinement Mappings
Bytecode Instrumentation
Generation of Property-Monitoring Classes
Conclusions
References
A High-Level Language for Modeling Algorithms and Their Properties
Introduction
Evaluation of PlusCal
Introducing a New Version of PlusCal
Structure of an Algorithm
PlusCal Statements
The PlusCal Compiler
Comparison with Lamport's PlusCal
Experiments
Related Work
Conclusion
References
A Formal Environment Model for Multi-Agent Systems
Introduction
Environment Model
Underlying Elementary p-Calculus Events
Operations
Environment Structures
Semantics
Convenience Elements and Operations
Composition Operators
Core Operations
Example
Conclusion
References
A Modal Interface Theory with Data Constraints
Introduction
Modal I/O-Transition Systems with Data Constraints
Refinement of MIODs
Composition and Compatibility of MIODs
Conclusion
References
Synchronizing Model and Program Refactoring
Introduction
Languages
Model Refactoring
Program Refactoring
Synchronization
Synchronizers
Consistency Relationship
Examples of Synchronizers
Soundness
Discussion
Invariants as Basis for Refactoring Automation
Quality of Refactorings
Consistency and Synchronizers
Related Work
Conclusions
References
A Type-Theoretic Framework for Certified Model Transformations
Introduction
Outline of the Approach
The CIC as a Technical Space
The Framework at a Glance
A Running Example
Formalization of Metamodels and Models
Translation of the Model Transformation
Verification of Properties
Conclusions and Further Work
References
Simulating Truly Concurrent CSP
Introduction
CSP
The Transformation $T$
Assembling the System
Properties
Examples
Choice versus Concurrency
One-Place Buffer
Dining Philosophers
Related and Further Work
Conclusion
References
Statistical Verification of Probabilistic Properties with Unbounded Until
Introduction
Probabilistic Model Checking
Stochastic Processes and Discrete-Time Markov Chains
Temporal Stochastic Logic
Error Control
Sampling-Based Verification of Unbounded Until
Sampling-Based Method with Reachability Analysis
Sampling-Based Method with Termination Probability
Related Work
Empirical Evaluation
Modified Polling System
Tandem Queuing Network
Discussion
References
Reasoning about Assignments in Recursive Data Structures
Introduction
Preliminaries
The Model
The Heap
Expressions, Statements and Compositions
Assignments
The Effect of Assignments on Multidot Expressions
Looking at the Heap Before the Assignment
Looking at the Heap After the Assignment
PVS Formalisation
Linearised Abstractions
Paths
Example: Verification of an In-Place List Reversal Algorithm
Other Data Structures
Evaluation and Future Work
Related Work
Conclusions
References
Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned
Introduction
Background
KAOS Method
Event-B Method
Experience with the Specification of a Localization Software Component
Abstract Model
First Refinement
Second Refinement
Third Refinement
Synthesis
Lessons Learned
Related Work
Conclusion and Further Work
References
A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence
Introduction
Case Study and Notations
Case Study
Notation B
Logs and Claims
System Information
Logs and Distribution
Properties and Claims
Log Functions
Log Extraction
Log Merge
Log Analysis
Log Analyzer
Incremental Analysis
Conclusion
Related Works
Future Work
References
Formal Development of a Cardiac Pacemaker: From Specification to Code
Introduction
The Pacemaker
Pacemaker in Z
Moving into Code
From Z to Perfect Developer
Analysis of Results
Conclusions
References
A Decision Procedure for Bisimilarity of Generalized Regular Expressions
Introduction
Regular Expressions for Polynomial Coalgebras
An Algebraic View on the Coalgebra of Generalized Regular Expressions
A Decision Procedure for Bisimilarity
A CIRC-Based Tool
Conclusions and Future Work
References
Normalization of Linear Horn Clauses
Introduction
Normalization of Finite Sets of Linear Horn Clauses
Basics
The Normalization Semi-procedure
Instantiation
An Application: Backward Reachability Analysis for Constrained Dynamic Pushdown Networks
Conclusion
References
A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs
Introduction
rCOS
Language
Mechanized Refinement
Graph Representation
State Graph
Graph Implementation
Graph Operations
Refinement of rCOS Designs
Primitive Designs
Composite Designs
Application
Tool Refinement
Provided Lemmas
Example
Conclusion
References
Automating Refinement of $Circus$ Programs
Introduction
Preliminaries
Mechanisation of $Circus$
ArcAngelC
Managing Well-Definedness
Reducing Constraints in the Semantic Encoding
A Semantic Formalisation of Well-Formedness
ExtensionstotheArcAngelC Implementation
Extended Refinement Theorems
Structural Combinators
Practical Experiences
Conclusions
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken