Project factsheet
CREDO ― Modeling and analysis of evolutionary structures for distributed services
- Project description
-
The objective of the CREDO project is to develop an integrated suite of tools for compositional modeling, testing, and validation of software, aimed at evolving networks of dynamically reconfigurable components. The project will develop a new high-level modelling language Creol, and integrate a formal component model based on concurrent objects. 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 that forms the basis for the development and integration of simulation, testing and validation tools for the compositional analysis of functional, timing, and resource requirements. Two case studies are part of the project: the ASK system, and biomedical sensor networks.
- NR's contribution
-
NR's researchers work on Case Study 2 – Biomedical sensor networks. The requirements from this case study have been collected and used as a basis for the specification of the CREDO tool suite. Biomedical sensor networks are modeled in Creol, and other formalisms developed in the project. Selected properties of the biomedical sensor networks will be simulated and model-checked. The results from this work will be compared with results obtained with existing simulation tools.
- Benefit for customers
-
NR works as a mediator between the university research and the end user (e.g., health care unit or hospital). NR's researchers have profound knowledge of the technical sides of the application area of wireless networks, and of the use of formal methods for model checking and simulation.
- Benefit for society
-
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.
-
Project results
(preliminary)
-
Several formalisms, e.g., the Creol language, timed automata, REO, constrained automata, were developed by the academic partners based on the requirements from the case studies. Aspects from the case studies are modeled using these formalisms. Simulations and model checking is used to retrieve valuable information about complex systems that the case studies represent.
