Formal Methods: Foundations and Applications
13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers
Published on 17. March 2011
VIII, 291 pages
978-3-642-19829-8 (ISBN)
Description
This book constitutes the thoroughly refereed post-conference
proceedings of the 13th Brazilian Symposium on Formal Methods, SBMF
2010, held in Natal, Brazil, in November 2010.
The 18 revised full papers were carefully reviewed and selected from
55 submissions. The papers presented cover a broad range of foundational
and methodological issues in formal methods for the design and analysis
of software and hardware systems as well as applications in various
domains.
More details
Other editions
Additional editions
Jim Davies | Leila Silva | Adenilso Simao
Formal Methods: Foundations and Applications
13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers
Book
03/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- 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
