Invited Talks.- Modelling of Complex Software Systems: A Reasoned Overview.- The ?+?CAL Algorithm Language.- Semantic-Based Development of Service-Oriented Systems.- Services.- JSCL: A Middleware for Service Coordination.- Analysis of Realizability Conditions for Web Service Choreographies.- Web Cube.- Presence Interaction Management in SIP SOHO Architecture.- Middleware.- Formal Analysis of Dynamic, Distributed File-System Access Controls.- Analysing the MUTE Anonymous File-Sharing System Using the Pi-Calculus.- Towards Fine-Grained Automated Verification of Publish-Subscribe Architectures.- A LOTOS Framework for Middleware Specification.- Composition and Synthesis.- Automatic Synthesis of Assumptions for Compositional Model Checking.- Refined Interfaces for Compositional Verification.- On Distributed Program Specification and Synthesis in Architectures with Cycles.- Generalizing the Submodule Construction Techniques for Extended State Machine Models.- Logics.- Decidable Extensions of Hennessy-Milner Logic.- Symbolic Verification - Slicing.- Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness.- A New Approach for Concurrent Program Slicing.- Reducing Software Architecture Models Complexity: A Slicing and Abstraction Approach.- Unified Modeling Languages.- Branching Time Semantics for UML 2.0 Sequence Diagrams.- Formalizing Collaboration Goal Sequences for Service Choreography.- Composition of Use Cases Using Synchronization and Model Checking.- Petri Nets.- PN Standardisation: A Survey.- Resource Allocation Systems: Some Complexity Results on the S4PR Class.- Optimized Colored Nets Unfolding.- Parameterized Verification.- Liveness by Invisible Invariants.- Real Time.- Extending EFSMs to Specify and Test TimedSystems with Action Durations and Timeouts.- Scenario-Based Timing Consistency Checking for Time Petri Nets.- Effective Representation of RT-LOTOS Terms by Finite Time Petri Nets.- Testing.- Grey-Box Checking.- Integration Testing of Distributed Components Based on Learning Parameterized I/O Models.- Minimizing Coordination Channels in Distributed Testing.- Derivation of a Suitable Finite Test Suite for Customized Probabilistic Systems.
