Formal Methods: Foundations and Applications
14th Brazilian Symposium, SBMF 2011, Sao Paulo, September 26-30 2011, Proceedings
Published on 10. November 2011
X, 205 pages
978-3-642-25032-3 (ISBN)
Description
This book constitutes the thoroughly refereed post-conference proceedings of the 14th Brazilian Symposium on Formal Methods, SBMF 2011, held in Sao Paulo, Brazil, in September 2011; co-located with CBSoft 2011, the second Brazilian Conference on Software: Theory and Practice. The 13 revised full papers were carefully reviewed and selected from 37 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
Adenilso Simao | Carroll Morgan
Formal Methods: Foundations and Applications
14th Brazilian Symposium, SBMF 2011, Sao Paulo, September 26-30 2011, Proceedings
Book
10/2011
Springer
€53.49
Shipment within 7-9 days
Content
- Intro
- Title
- Preface
- Organization
- Table of Contents
- Model Transformation and Induced Instance Migration: A Universal Framework
- Introduction
- An Introductory Example
- Migration Framework
- Application of the Framework
- Models with Component Structure
- Data Models Axiomatically
- Related Work
- Conclusion and Outlook
- References
- SPARKSkein: A Formal and Fast Reference Implementation of Skein
- Introduction
- Skein
- SPARK
- Implementing SPARKSkein
- Verification of SPARKSkein
- Static Verification and Proof
- Reference Test Vectors
- Platform Testing
- Coverage Analysis
- Performance Testing
- Further Work and Challenges
- GCC
- The SPARK Tools
- Comparison with Other Verification Tools
- Conclusions
- References
- Full Abstraction at Package Boundaries of Object-Oriented Languages
- Introduction
- Formalization of LPJava and Source Compatibility
- Trace Characterization of Component Behavior
- Enhanced Operational Semantics
- Most General Context
- Full Abstractness
- Simulations
- Well-Formed Runtime Configurations
- Preorder Relations $\cpre{\rho}{\cmpctxt}$
- Small-Step Semantics
- Large-Step Semantics
- Proving Compatibility
- Conclusion and Future Work
- References
- B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design
- Introduction
- Methodology
- A Case Study
- Transformation of B Specifications
- Systems with Replicated Machines
- Synchronized Inputs and Execution Frames
- Translating the Main System
- Verification
- Conclusions
- References
- Simulation and Verification of Synchronous Set Relations in Rewriting Logic
- Introduction
- Abstract Synchronous Set Relations
- Synchronous Set Relations in Rewriting Logic
- A Brief Overview of Rewriting Logic
- The Synchronous Language L
- Simulation of sL
- Executable Semantics of a Simple Synchronous Language
- Verification of Synchronous Relations
- Conclusion
- References
- PiStache: Implementing p-Calculus in Scala
- Introduction
- Background
- -Calculus
- Scala
- PiStache: An Application Programming Interface (API)
- Core Elements
- Operators
- Internal Representation
- Execution Model
- API Usage
- Conclusions
- References
- Sound and Complete Abstract Graph Transformation
- Introduction
- Background
- Shape Constraints
- Soundness and Completeness
- Conclusion
- References
- On the Specification, Verification and Implementation of Model Transformations with Transformation Contracts
- Introduction
- Related Work
- Model-Driven Development with Transformation Contracts
- Specifying Transformation Contracts
- Verifying and Validating Transformation Contracts
- Model Consistency Reasoning and Description Logic
- Model Consistency Verification in Model Transformations with Transformation Contracts
- Verifying and Validating Access Control Models
- A Design Pattern for the Implementation of Model Transformations with Transformation Contracts
- Final Remarks
- References
- Modular Embedding of the Object Constraint Language into a Programming Language
- Introduction
- Motivation for Reusing OCL
- soil by Example
- Embedding of OCL into SOIL
- Formal Representation of OCL Expressions
- Statements
- Local Variables
- Operations with Side Effects
- State Manipulation Statements
- Consequences of a Modular Embedding
- Conclusion
- References
- Algebra of Monotonic Boolean Transformers
- Introduction
- Monotonic Boolean Transformers
- Algebra of Monotonic Boolean Transformers
- Assertions and Assumptions
- Weakest Precondition, Guards, Hoare Triples, and Data Refinement
- Conclusions
- References
- Behavioural Preservation in Fault Tolerant Patterns
- Introduction
- Overview of HOL
- Fault Tolerant Patterns
- Specification
- Implementation
- Homogeneous Redundancy
- Heterogeneous Redundancy
- Triple Modular Redundancy
- Case Study
- Related Work
- Conclusion
- References
- A Formal Approach to Fixing Bugs
- Introduction
- Methodology and Application
- Example Bug Patterns and Categories
- Placing Debugging within Software Development
- A Language for Detecting and Fixing Bugs
- Basis: The TRANS Language
- From TRANS to TRANSfix
- Actions
- Type System
- Specification Examples
- Prototype Implementation
- Silhouettes
- Implementation Details
- Analysis
- Related Work
- Correctness Issues
- References
- A Formal Treatment of Agents, Goals and Operations Using Alternating-Time Temporal Logic
- Introduction
- The Khi Language
- The Metamodel
- Actors and Goals
- Actors and Capabilities
- Assignment of Roles to Coalitions
- Semantics
- Formal Background: Temporal and Multi-agent Logics
- Semantics of Khi in ATLKhi
- Application to Our Toy Example
- Related Work
- Conclusion
- References
- Author Index
