Formal Methods for Components and Objects : 7th International Symposium, FMCO 2008, Sophia Antipolis, France, October 21-23, 2008, State of the Art Survey

by Boer, Frank S. De; Bonsangue, Marcello M.; Madelaine, Eric

• ISBN13: 9783642041662
• ISBN10: 3642041663
• Edition: 1st
• Format: Paperback
• Copyright: 2009-10-01
• Publisher: Springer-Verlag New York Inc

Summary

Formal methods have been applied successfully to the verification of medium-sized programs in protocol and hardware design. However, their application to the development of large systems requires more emphasis on specification, modelling and validation techniques supporting the concepts of reusability and modifiability, and their implementation in new extensions of existing programming languages like Java.This State-of-the-Art Survey presents the outcome of the 7th Symposium on Formal Methods for Components and Objects that was held in Sophia Antipolis, France, during October 21-23, 2008. It was realized as a concertation meeting of European projects focussing on formal methods for components and objects.This book presents 15 revised papers submitted after the symposium by the speakers of each of the following European IST projects: the IST-FP7 project COMPAS, on compliance -driven models, languages, and architectures for services; the IST-FP6 project CREDO on modeling and analysis of evolutionary structures for distributed services; the IST-FP7 project DEPLOY, on industrial deployment of advanced system engineering methods for high productivity and dependability; the IST-FP6 project GridComp, on grid programming with components; and the IST-FP6 project Mobius, developing the technology for establishing trust and security for the next generation of global computers.

Table of Contents

The COMPAS Project
Reusable Architectural Decision Model for Model and Metadata Repositories	p. 1
Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems	p. 21
The CREDO Project
A Real-Time Extension of Creol for Modelling Biomedical Sensors	p. 42
Conformance Testing of Distributed Concurrent Systems with Executable Designs
Formal Verification for Components and Connectors	p. 82
The DEPLOY Project
Formal Modular Modelling of Context-Awareness	p. 102
Towards Demonstrably Correct Compilation of Java Byte Code	p. 119
Incremental System Modelling in Event-B	p. 139
The GRIDCOMP Project
An Asynchronous Distributed Component Model and Its Semantics	p. 159
Specification and Verification for Grid Component-Based Applications: From Models to Tools	p. 180
Semi-formal Models to Support Program Development: Autonomic Management within Component Based Parallel and Distributed programming	p. 204
The MOBIUS Project
Session-Based Compilation Framework for Multicore Programming	p. 226
Abstract Interpretation of Symbolic Execution with Explicit State Updates	p. 247
BML and Related Tools	p. 278
Author Index	p. 299
Table of Contents provided by Ingram. All Rights Reserved.