Formal Methods for Components and Objects: Second International Symposium, FMCO 2003, Leiden, The Netherlands, November 4-7, 2003. Revised Lectures

Albert Benveniste, Benoît Caillaud (auth.), Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Willem-Paul de Roever (eds.)3540229426, 9783540229421, 9783540301011

Formal methods have been applied successfully to the verification of medium-sized programs in protocol and hardware design. However, their application to more complex systems, resulting from the object-oriented and the more recent component-based software engineering paradigms, requires further development of specification and verification techniques supporting the concepts of reusability and modifiability.

This book presents revised tutorial lectures given by invited speakers at the Second International Symposium on Formal Methods for Components and Objects, FMCO 2003, held in Leiden, The Netherlands, in November 2003. The 17 revised lectures by leading researchers present a comprehensive account of the potential of formal methods applied to large and complex software systems such as component-based systems and object systems. The book makes a unique contribution to bridging the gap between theory and practice in software engineering.

Table of contents :
Front Matter….Pages –
Causality and Scheduling Constraints in Heterogeneous Reactive Systems Modeling….Pages 1-16
Machine Function Based Control Code Algebras….Pages 17-41
Exploiting Abstraction for Specification Reuse. The Java/C# Case Study….Pages 42-76
On the Verification of Cooperating Traffic Agents….Pages 77-110
How to Cook a Complete Hoare Logic for Your Pet OO Language….Pages 111-133
Behavioural Specification for Hierarchical Object Composition….Pages 134-156
Consistency Management within Model-Based Object-Oriented Development of Components….Pages 157-176
CommUnity on the Move: Architectures for Distribution and Mobility….Pages 177-196
TulaFale: A Security Tool for Web Services….Pages 197-222
A Checker for Modal Formulae for Processes with Data….Pages 223-239
Semantic Essence of AsmL: Extended Abstract….Pages 240-259
An MDA Approach to Tame Component Based Software Development….Pages 260-275
An Application of Stream Calculus to Signal Flow Graphs….Pages 276-291
Synchronous Closing and Flow Analysis for Model Checking Timed Systems….Pages 292-313
Priority Systems….Pages 314-329
Preserving Properties under Change….Pages 330-343
Tools for Generating and Analyzing Attack Graphs….Pages 344-371
Back Matter….Pages –