Formal Methods for Open Object-Based Distributed Systems

This volume contains the proceedings of FMOODS 2003, the 6th IFIP WG 6. 1 International Conference on Formal Methods for Open Object-Based Distributed Systems. The conference was held in Paris, France on November 19-21, 2003. The event was the sixth meeting of this conference series, which is held roughly every year and a half, the earlier events having been held in Paris, Canterbury, Florence, Stanford, and Twente. ThegoaloftheFMOODSseriesofconferencesistobringtogetherresearchers whose work encompasses three important and related ?elds: - formal methods; - distributed systems; - object-based technology. Such a convergence is representative of recent advances in the ?eld of distributed systems,andprovideslinksbetweenseveralscienti?candtechnologicalcommu- ties, as represented by the conferences FORTE/PSTV, CONCUR, and ECOOP. The objective of FMOODS is to provide an integrated forum for the p- sentation of research in the above-mentioned ?elds, and the exchange of ideas and experiences in the topics concerned with the formal methods support for open object-based distributed systems. For the call for papers, aspects of int- est of the considered systems included, but were not limited to: formal models; formal techniques for speci?cation, design or analysis; component-based design; veri?cation, testing and validation; semantics of programming, coordination, or modeling languages; type systems for programming, coordination or modelling languages; behavioral typing; multiple viewpoint modelling and consistency - tween di?erent models; transformations of models; integration of quality of s- vice requirements into formal models; formal models for security; and appli- tions and experience, carefully described.

Inhalt

Invited Talk.- Java's Integral Types in PVS.- Models.- Towards Object-Oriented Graphs and Grammars.- A Rewriting Based Model for Probabilistic Distributed Object Systems.- Engineering the SDL Formal Language Definition.- Logic and Verification.- A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts.- Inheritance of Temporal Logic Properties.- Temporal Logic Based Static Analysis for Non-uniform Behaviours.- Calculi.- The Kell Calculus: Operational Semantics and Type System.- A Calculus for Long-Running Transactions.- Formal Analysis of Some Timed Security Properties in Wireless Protocols.- Java and .NET.- Inductive Proof Outlines for Monitors in Java.- Proof Scores in the OTS/CafeOBJ Method.- Managing the Evolution of .NET Programs.- UML.- On Mobility Extensions of UML Statecharts. A Pragmatic Approach.- New Operators for the TURTLE Real-Time UML Profile.- Checking Consistency in UML Diagrams: Classes and State Machines.- Composition and Verification.- Compositional Verification Using CADP of the ScalAgent Deployment Protocol for Software Components.- Verification of Distributed Object-Based Systems.- Design and Verification of Distributed Multi-media Systems.