Formal Methods for Components and Objects

1. Front Matter

   PDF

2. The BIONETS Project

   1. A Framework for Reasoning on Component Composition

      • Ludovic Henrio, Florian Kammüller, Muhammad Uzair Khan

      Pages 1-20

3. The COMPAS Project

   1. Verification of Context-Dependent Channel-Based Service Models

      • Natallia Kokash, Christian Krause, Erik P. de Vink

      Pages 21-40

4. The CREDO Project

   1. The Credo Methodology

      • Immo Grabe, Mohammad Mahdi Jaghoori, Joachim Klein, Sascha Klüppelholz, Andries Stam, Christel Baier et al.

      Pages 41-69

5. The DEPLOY Project

   1. Patterns for Refinement Automation

      • Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky

      Pages 70-88

   2. Applying Event-B Atomicity Decomposition to a Multi Media Protocol

      • Asieh Salehi Fathabadi, Michael Butler

      Pages 89-104

6. The FM-SOA Working Group

   1. Abstract Certification of Global Non-interference in Rewriting Logic

      • Mauricio Alba-Castro, María Alpuente, Santiago Escobar

      Pages 105-124

7. The HATS Project

   1. Interleaving Symbolic Execution and Partial Evaluation

      • Richard Bubel, Reiner Hähnle, Ran Ji

      Pages 125-146

8. The INESS Project

   1. The Use of Model Transformation in the INESS Project

      • Osmar M. dos Santos, Jim Woodcock, Richard F. Paige, Steve King

      Pages 147-165

   2. Suitability of mCRL2 for Concurrent-System Design: A 2 × 2 Switch Case Study

      • Frank P. M. Stappers, Michel A. Reniers, Jan Friso Groote

      Pages 166-185

9. The MOGENTES Project

   1. Mapping UML to Labeled Transition Systems for Test-Case Generation

      • Willibald Krenn, Rupert Schlick, Bernhard K. Aichernig

      Pages 186-207

   2. Mutation-Based Test Case Generation for Simulink Models

      • Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer et al.

      Pages 208-227

   3. Model-Based Mutation Testing of Hybrid Systems

      • Bernhard K. Aichernig, Harald Brandl, Elisabeth Jöbstl, Willibald Krenn

      Pages 228-249

10. The PROTEST Project

    1. Property-Based Testing - The ProTest Project

       • John Derrick, Neil Walkinshaw, Thomas Arts, Clara Benac Earle, Francesco Cesarini, Lars-Ake Fredlund et al.

       Pages 250-271

    2. Incrementally Discovering Testable Specifications from Program Executions

       • Neil Walkinshaw, John Derrick

       Pages 272-289

11. The QUASIMODO Project

    1. Methodologies for Specification of Real-Time Systems Using Timed I/O Automata

       • Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Andrzej Wąsowski

       Pages 290-310

    2. The How and Why of Interactive Markov Chains

       • Holger Hermanns, Joost-Pieter Katoen

       Pages 311-337

12. Back Matter

    PDF

All modern industries rely on large and complex software systems. In order to construct such large systems in a systematic manner, the focus of the development methodologies has switched in the last two decades from functional to structural issues. 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 a greater emphasis on specification, modeling, 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 8th Symposium on Formal Methods for Components and Objects, held in Eindhoven, The Netherlands, in November 2009. The volume contains 17 revised contributions submitted after the symposium by speakers from each of the following European IST projects: the IST-FP6 project BIONETS on biologically inspired services evolution for the pervasive age; the IST-FP7 project COMPAS on compliance-driven models, languages, and architectures for services; the IST-FP6 project CREDO on modelling and analysis of evolutionary structures for distributed services; the IST-FP7 DEPLOY on industrial deployment of advanced system engineering methods for high productivity and dependability; the IST-FP7 project HATS on highly adaptable and trustworthy software using formal methods; the IST-FP7 project INESS on integrated European railway signalling system; the IST-FP7 project MOGENTES on model-based generation of tests for dependable embedded systems; the IST-FP6 project PROTEST on property based testing; and the IST-FP7 project QUASIMODO on quantitative system properties in model-driven-design of embedded systems.

• component systems
• formal specification
• formal verification
• process analysis
• systems modeling

• Centre for Mathematics and Computer Science, CWI, Amsterdam, The Netherlands

  Frank S. Boer

• Leiden Institute of Advanced Computer Science, Leiden University, Leiden, The Netherlands

  Marcello M. Bonsangue

• Heinrich-Heine University of Dusseldorf, Dusseldorf, Germany

  Stefan Hallerstede

• Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, Düsseldorf, Germany

  Michael Leuschel

Policies and ethics