Software Model Checking: The Bandera approach.- Verifying Authentication Protocol Implementations.- A Semantic Framework for Specifying and Reasoning about Composable Distributed Middleware Services.- Formal Semantics for Interacting UML Subsystems.- A Compositional Formalism for Object Viewpoints.- Interpreting ODP Viewpoint Specification: Observations from a Case Study.- Checking Behavioural Subtypes via Refinement.- Behavioural Subtyping and Property Preservation for Active Objects.- A Formal Service Specification for HOP Based on ISO/IEC 14752.- Mobile Objects “Must” Move Safely.- A Theory of May Testing for Actors.- Computer-Aided Specification and Verification of Annotated Object-Oriented Programs.- Foinial Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm.- Control Flow Analysis of Mobile Ambients with Security Boundaries.- Generating Adapters for Concurrent Component Protocol Synchronisation.- A Feature Manager Approach to the Analysis of Component-Interactions.- Supporting Collaborative Design.- A Visual Modeling Framework for Distributed Object Computing.- Author Index.

GPSR Compliance The European Union's (EU) General Product Safety Regulation (GPSR) is a set of rules that requires consumer products to be safe and our obligations to ensure this. If you have any concerns about our products you can contact us on ProductSafety@springernature.com. In case Publisher is established outside the EU, the EU authorized representative is: Springer Nature Customer Service Center GmbH Europaplatz 3 69115 Heidelberg, Germany ProductSafety@springernature.com