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)

Annotation 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 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 Gilles Barthe, Frank S. De Boer (eds.). ... The 10th Ifip Working Group 6.1 International Conference On Formal Methods For Open Object-based Distributed Systems (fmoods 2008).--pref. Includes Bibliographical References And Index.