Formal Methods for Open Object-Based Distributed Systems: 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008 Proceedings (Lecture Notes in Computer Science, 5051)

✍ Scribed by Gilles Barthe (editor)

• Publisher: Springer
• Year: 2008
• Tongue: English
• Leaves: 268
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 10th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2008, held in Oslo, Norway, in June 2008. The 14 revised full papers presented together with 1 invited lecture were carefully reviewed and selected from 35 submissions. The papers cover topcics such as semantics of object-oriented programming; formal techniques for specification, analysis, and refinement; model checking; theorem proving and deductive verification; type systems and behavioral typing; formal methods for service-oriented computing; integration of quality of service requirements into formal models; formal approaches to component-based design; and applications of formal methods.

✦ Table of Contents

Title Page
Preface
Organization
Table of Contents
Guiding Distributed Systems Synthesis with Language-Based Security Policies
Termination Analysis of Java Bytecode
Introduction
Java Bytecode and Its Rule-Based Representation
From Bytecode to Control Flow Graphs
Rule-Based Representation
Proving Termination
Abstracting the Rules
Input Output Size-Relations
Call-to Pairs
Proving Termination of the Binary Program CA
Improving Termination Analysis by Extracting Nested Loops
Experimental Results
Conclusions and Related Work
Sessions and Pipelines for Structured Service Programming
Introduction
The close-Free Fragment of CaSPiS
Syntax
Operational Semantics
Well-Formedness
CaSPiS at Work
The Full Calculus
Syntax and Operational Semantics of the Full Calculus
Programming Graceful Termination
Conclusion, Related Work and Future Work
Modular Preservation of Safety Properties by Cookie-Based DoS-Protection Wrappers
Introduction
Preliminaries
Cookie-Based DoS Protection
Kripke Structures, Safety Properties and Stuttering Simulation
Rewriting Logic
Underlying Protocol
Cookie Wrapper and Its Preservation Properties
Simulation
Security with a Man-in-the-Middle Intruder
Rewrite Theory for the Dolev-Yao Intruder
Simulation
Modular Reasoning with Cookies in IKEv2
Related Work
Conclusions and Future Work
Behavioural Theory atWork: Program Transformations in a Service-Centred Calculus
Introduction
SSCC
Common Sequence Diagram Patterns
Bisimilarity in SSCC
Breaking Sequential Sessions
Correctness of the Transformations
Conclusions
Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack
Introduction
The Stack and Its Lock-Free Implementation
The Refinement Methodology
Application to the Stack Example
Linearizability as Refinement
Possibilities and Forward Simulation
Conclusion
Symbolic Step Encodings for Object Based Communicating State Machines
Introduction
Systems and Semantics
Object Based State Machine Models
Symbolic Encoding
State Variables
State Machines and Queues
Effects and Data
Step Constraints
Size of the Encodings
Experimental Results
Conclusions and Future Work
Modeling and Model Checking Software Product Lines
Introduction
Product-Line CCS
Product Lines
PL-CCS – Syntax
Semantics of a PL-CCS Program
Model Checking Product Lines
Specification and Verification of a Sample Product-Line
Conclusion
References
Semantic Foundations and Inference of Non-null Annotations
Introduction
Syntax and Semantics
Null-Pointer Analysis
Abstract Domains
Inference Rules
Example
Correctness
Inference
Fähndrich and Leino's Type System
Towards a Null-Pointer Analyzer for Java Bytecode
Conclusions and Future Work
Redesign of the LMST Wireless Sensor Protocol through Formal Modeling and Statistical Model Checking
Introduction
The Idealized Local Minimum Spanning Tree Protocol
Idealized LMST Model in Real-Time Maude
Modeling Wireless Networks in Real-Time Maude
Idealized Model of LMST in Real-Time Maude
Probabilistic Modeling and Analysis of LMST
Probabilistic Rewrite Theories, QuaTEx, and VeStA
Refinement 1: Unsynchronized Timers
Refinement 2: Delay Uncertainty
A New Realistic Design of LMST
A Formally-Based System Redesign Methodology
Redesign of the LMST Protocol
Related Work and Conclusions
A Minimal Set of Refactoring Rules for Object-Z
Introduction
Object-Z
Introduce Generic Parameter
Example
Introduce Polymorphism
Example
Introduce Inheritance
Example
Completeness
Conclusion
Formal Modeling of a Generic Middleware to Ensure Invariant Properties
Introduction
Applying Formal Methods to Middleware
Middleware Architectures
Modeling Middleware with Z
Verifying Invariants in the Middleware Specification
Conclusion and Future Work
CoBoxes: Unifying Active Objects and Structured Heaps
Introduction
Related Work and Motivation
Programming with Concurrent Boxes
CoBoxes as Active Objects
Nested CoBoxes and Internal Concurrency
Multiple Entry Objects
Controlling Reentrant Calls
Formal Semantics
Syntax
Semantic Entities
Transition Rules
Program Execution
Properties
Conclusions
VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language
Introduction
Preventing Data Races
Programming Model
Annotations
Verification
Soundness
Data Abstraction
Annotations
Verification
Read-Write Locks
Related Work
Conclusion
Translation of Expressions
Contracts for Runnable and Thread
Translation of Statements
Concurrent Iterator
A Caller-Side Inline Reference Monitor for an Object-Oriented Intermediate Language
Introduction
Problem Statement
Base System
Execution System
The Inlining Algorithm
Properties of the Inlining Algorithm
Virtual Methods
Delegates
Implementation
Related Work
Conclusions
Operational Semantics
Author Index