The group Formal methods for coordination languages (SEN3.2) is a subgroup of the research group Coordination Languages (SEN3)
Coordinator of Formal methods for coordination languages: Frank de Boer
The general research in this subtheme concerns the development and application of formal methods for coordination languages. Current research and future plans concentrate on the integration of testing and verification techniques for the validation of software models. Special emphasis is on software models which integrate a coordination model based on mobile channels. In particular, software models for object-oriented and multi-agent systems are considered, for which additionally the synthesis of application specific schedulers is investigated.
The objective of the Credo project is the development and application of an integrated suite of tools for compositional modelling, testing, and validation of software for evolving networks of dynamically reconfigurable components.
The problem that the Trust4All project aims to solve is how to establish and maintain correct operation of a system, while the software embedded in the system is being upgraded and extended (while the system is in use by a customer).
The main problem addressed in the CoCoMAS project is how to design and develop executable coordination models at various levels within multi-agent systems and how to integrate these models.
The aim of the BRICKS AFM3.1 project is the development of compositional methods, tools, and formal techniques for the dynamic composition of components, the validation of their composition, and the validation of components themselves.
The MobiJ project aims at the development of a programming environment which supports component-based design and verification of Java programs.
Key publications
- F.S. de Boer and C. Pierik, A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts. In Proceedings of Formal Methods for Open Object-based Distributed Systems (FMOODS), LNCS, 2003.
- E. Abraham-Mumm, F.S. de Boer, W.P. de Roever, and M. Steffen, Inductive Proof Outlines for Monitors in Java. In Proceedings of Formal Methods for Open Object-based Distributed Systems (FMOODS), LNCS, 2003.
- E. Abraham-Mumm, F.S. de Boer, W.P. de Roever, and M. Steffen, A Tool-supported Proof System for Multithreaded Java. In Proceedings of the First International Symposium on Formal Methods for Components and Objects (FMCO 2002), LNCS, Vol. 2852, 2003.
