CREDO – Modeling and analysis of evolutionary structures for distributed services
CREDO – Modeling and analysis of evolutionary structures for distributed services
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
The project results achieved at NR are described in an article (external link).
Publications
- Leister, Wolfgang; Bjørk, Joakim; Schlatte, Rudolf; Johnsen, Einar Broch; Griesmayer, Andreas (2012). Exploiting Model Variability in ABS to Verify Distributed Algorithms. International Journal On Advances in Telecommunications. ISSN 1942-2601. 5(1&2)
- Grabe, Immo; Jaghoori, Mohammad Mahdi; Klein, Joachim; Klüppelholz, Sascha; Stam, Andries; Baier, Christel; Blechmann, Tobias; Aichernig, Bernhard; de Boer, Frank; Griesmayer, Andreas; Johnsen, Einar Broch; Kyas, Marcel; Leister, Wolfgang; Schlatte, Rudolf; Steffen, Martin; Tschirner, Simon; Liang, Xuedong; Yi, Wang (2010). The Credo Methodology (Extended Version). Lecture Notes in Computer Science = Lecture notes in artificial intelligence. ISSN 0302-9743. Full-text . Review
- Grabe, Immo; Jaghoori, Mohammad Mahdi; Aichernig, Bernhard; Baier, Cristel; Blechmann, Tobias; de Boer, Frank; Griesmayer, Andreas; Johnsen, Einar Broch; Klein, Joachim; Klüppelholz, Sascha; Kyas, Marcel; Leister, Wolfgang; Schlatte, Rudolf; Stam, Andries; Steffen, Martin; Tschirner, Simon; Liang, Xuedong; Yi, Wang (2010). Credo Methodology: Modeling and Analyzing A Peer-to-Peer System in Credo. Electronical Notes in Theoretical Computer Science. ISSN 1571-0661.
- Leister, Wolfgang; Bjørk, Joakim; Schlatte, Rudolf; Griesmayer, Andreas (2011). Verifying Distributed Algorithms with Executable Creol Models. PESARO 2011 Conference, Budapest, Hungary. Full-Text.
- Leister, Wolfgang; Bjørk, Joakim; Schlatte, Rudolf; Griesmayer, Andreas (2010). Validation of Creol Models for Routing Algorithms in Wireless Sensor Networks. NR Report 1024, ISBN: 978-82-539-0534-1
- Leister, Wolfgang; Liang, Xuedong; Klüppelholz, Sascha; Klein, Joachim; Owe, Olaf; Kazemeyni, Fatemeh Sadat; Bjørk, Joakim; Østvold, Bjarte Mayanja (2009). Modelling of Biomedical Sensor Networks using the Creol Tools. NR Report 1022, ISBN: 978-82-539-0532-7
Contact information
Project period
Financing
EU IST 6th Framework programme - contract no. 33826