Formal Techniques for Networked and Distributed Systems - FORTE 2006 : 26th IFIP WG 6. 1 International Conference, Paris, France, September 26-29, 2006, Proceedings

by Najm, Elie; Pradat-peyre, Jean-francois; Donzeau-gouge, Veronique Viguie

• ISBN13: 9783540462194
• ISBN10: 3540462198
• Format: Paperback
• Copyright: 2006-11-14
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 26th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2006, held in Paris, France, in September 2006.The 26 revised full papers and 4 short papers presented together with 3 invited lectures were carefully reviewed and selected from 177 submissions. The papers focus on the construction of middleware and services using formalised and verified approaches, and address - in addition to the classical protocol specification, verification and testing problems - the issues of composition of protocol functions and of algorithms for distributed systems. The papers are organized in topical sections on services, middleware, composition and synthesis, logics, symbolic verification/slicing, unified modeling languages, petri nets, parameterized verification, real time, and testing.

Table of Contents

Modelling of complex software systems : a reasoned overview	p. 1
The [superscript +]CAL algorithm language	p. 23
Semantic-based development of service-oriented systems	p. 24
JSCL : a middleware for service coordination	p. 46
Analysis of realizability conditions for Web service choreographies	p. 61
Web cube	p. 77
Presence interaction management in SIP SOHO architecture	p. 93
Formal analysis of dynamic, distributed file-system access controls	p. 99
Analysing the MUTE anonymous file-sharing system using the Pi-calculus	p. 115
Towards fine-grained automated verification of publish-subscribe architectures	p. 131
A LOTOS framework for middleware specification	p. 136
Automatic synthesis of assumptions for compositional model checking	p. 143
Refined interfaces for compositional verification	p. 159
On distributed program specification and synthesis in architectures with cycles	p. 175
Generalizing the submodule construction techniques for extended state machine models	p. 191
Decidable extensions of Hennessy-Milner logic	p. 196
Symbolic verification of communicating systems with probabilistic message losses : liveness and fairness	p. 212
A new approach for concurrent program slicing	p. 228
Reducing software architecture models complexity : a slicing and abstraction approach	p. 243
Branching time semantics for UML 2.0 sequence diagrams	p. 259
Formalizing collaboration goal sequences for service choreography	p. 275
Composition of use cases using synchronization and model checking	p. 292
PN standardisation : a survey	p. 307
Resource allocation systems : some complexity results on the S[superscript 4]PR class	p. 323
Optimized colored nets unfolding	p. 339
Liveness by invisible invariants	p. 356
Extending EFSMs to specify and test timed systems with action durations and timeouts	p. 372
Scenario-based timing consistency checking for time petri nets	p. 388
Effective representation of RT-LOTOS terms by finite time petri nets	p. 404
Grey-box checking	p. 420
Integration testing of distributed components based on learning parameterized I/O models	p. 436
Minimizing coordination channels in distributed testing	p. 451
Derivation of a suitable finite test suite for customized probabilistic systems	p. 467
Table of Contents provided by Blackwell. All Rights Reserved.