Project code: CREDO
Research group: Formal methods for coordination languages (SEN3.2)

Start: 2006-09-01
End: 2009-09-01

Coordinator of this project: Frank de Boer

The objective of this project is the development and application of an integrated suite of tools for compositional modeling, testing, and validation of software for evolving networks of dynamically reconfigurable components. These are featured by our case studies, the ASK system and biomedical sensor networks, provided by the industrial partners.

The ASK system is a system for connecting people to other people or for automated response systems (e.g., interactive voice response IVR). The specific problem of this case study, addressed by this project, is to model and verify specific dynamically reconfigurable parts of the complete system using the compositional modeling and verification techniques developed in this project, in the setting of the services provided by other preexisting components.

Biomedical sensors are increasingly used to detect abnormal biological changes and monitor biological parameters in tissues and organs. Advanced hospitals are using an array of biomedical sensors for diagnostics, surgical, and post-operative phases. The outcome of this case study is a framework useful for the design of future sensor network solutions, as well as evaluation of their suitability and correctness. The framework will be designed to meet the needs towards better monitoring devices and network solutions.

The project will develop a new high-level modeling language Credo for the dynamic composition of highly reconfigurable component-based software systems, and light-weight and automated verification techniques and tools supporting this language. Credo integrates a formal component model based on concurrent objects which support run-time updates with a new model of component connectors based on mobile channels. Credo supports rapid prototyping and automated validation of networks of distributed services implemented by components, focusing on analyzing the effect of dynamic reconfiguration. The kernel of the Credo tool suite is an abstract interpreter for the language. The abstract interpreter forms the basis for the development and integration of simulation, testing and validation tools for the compositional analysis of functional, timing,

Members
Farhad Arbab, Frank de Boer, Marcello Bonsangue, David Clarke, Jan Rutten

Cooperation

• University of Oslo, Norway (Einar Broch Johnsen and Olaf Owe)
• University of Kiel, Germany (Willem- Paul de Roever)
• University of Bonn, Germany (Christel Baier)
• Uppsala University, Sweden (Wang Yi and Bengt Jonsson)
• United Nations University, Macao (Bernhard Aichernig)
• Almende, Netherlands (Peet van Tooren)
• Rikshospitalet, Norway (Ilangko Balasingham)
• Norsk Regnesentral, Norway (Wolfgang Leister)