Click on a theme or a project in the table below for more information.
Project leader:
Prof.dr. Frank de Boer (CWI)
Consortium:
CWI, TU/e
Industrial partners (non-exhaustive):
Almende (NL), Rikshospitalet Radiumhospitalet HF (N)
International partners:
University of Oslo, University of Dresden
Total FTE: 3.53 (heads: faculty: 9, PhD: 2)
Key BRICKS publications:
| • |
Andova, Baeten, Willemse: "A Complete Axiomatisation of Branching Bisimulation for Probabilistic Systems with an Application in Protocol Verification" In: CONCUR 2006, LNCS 4137
|
| • |
Arbab, Baier, de Boer and Rutten: "Models and temporal logical specifications for timed component connectors" In: Journal Software and Systems Modeling, 2006
|
| • |
Kemper and Platzer: "SAT-based Abstraction Refinement for Real-time Systems" In: Third International Workshop on Formal Aspects of Component Software 2006
|
| • |
Arbab, Baier, de Boer, Rutten and Sirjani: "Synthesis of Reo Circuits for Implementation of Component-Connector Automata Specifications" In: International Conference on Coordination Models and Languages 2005, LNCS 3454
|
| • |
Markovski and Trcka: "Lumping Markov Chains with Silent Steps" In: Third International Conference of Quantitive Evaluation of Systems 2006. IEEE Computer Society
|
| • |
Sokolova and De Vink: "Probabilistic Automata: System Types, Parallel Composition and Comparison" In: Validation of Stochastic Systems, 2004, LNCS 2925
|
|
Project AFM3: Formal Methods for Active Networking
The main aim of this project is the development and application
of formal methods for active networks. In particular we focus on:
- Dynamically evolving networks of co-operating software components
- Transmission control protocols that regulate the traffic in the Internet
The research is carried out in two subprojects by researchers from
both CWI and TU/e. On the basis of previous cooperation between
various members of both subprojects, the techniques and formal
methods developed in each of the subprojects are also applicable
in the other. In addition, the combined use of both coalgebra and
coinduction (a specialism of CWI) and that of (probabilistic)
process algebra (an important expertise with the TU/e) will lead
to further insights in each of the subprojects.
Subproject AFM3.1: Components and connectors
The aim of the present research 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 focus will be on the
connectors, rather than on the components that they connect. A
promising approach in this direction is Reo, a channel-based
coordination model recently introduced at CWI. In Reo, complex
networks, called connectors, are compositionally built out of
simpler ones. The main goal of the research is to develop a
calculus of component connectors, as a foundation for the further
development of practical tools and programming environments for the
actual deployment of Reo.
Subproject AFM3.2: Transmission control protocols for the Internet
The main goal of this subproject is to deepen the
understanding of the performance of the present Internet control
protocols, and obtain insight into the improvements required to
support new applications. One major contribution of the project
will be a formal correctness verification of variants and
enhancements of TCP. Another important contribution is a detailed
performance analysis of TCP in dynamic network environments, and of
extensions for supporting new Internet applications such as
real-time multicast traffic. Key issues in the evaluation of
communication network protocols are:
- the formal verification of their correctness
- the analysis of their performance
- iterative modelling and analysis for protocol (re)design
Industrial cooperation
In the context of the European IST project Credo on modeling and
analysis of evolutionary structures for distributed services this
project cooperates with Almende (NL) and the
Rikshospitalet-Radiumhospitalet HF (N).
International cooperation
We have established a fruitful synergy with the European IST
project Credo (with the U. of Oslo, Almende and RRHF) and the
bilateral NWO/DFG project SYANCO with the U. of Dresden.
Highlights 2004-2006
Research highlights
We have developed a formal model for the channel-based component
connectors of Reo in terms of Timed Constraint Automata and
introduced a temporal-logic for specification and verification of
their real-time properties. We developed abstraction and refinement
techniques for real-time systems based on the satisfaction of
logical formulas.
Economic & societal impact
The results of this project will have impact on industrial
applications involving complex dynamically evolving software. The
case studies provided by the industrial partners particularly
target software solutions that improve the quality of life and
health, in particular adaptive biomedical devices contribute to
citizen-centred health care system (eHealth).
Future work 2007-2009
We plan to further develop and apply abstraction and refinement
techniques for automata models of reconfigurable component
connectors and to establish a firm connection of the process
algebraic theory and verification methods for real-time systems, on
the one hand, and those for probabilistic and generally distributed
stochastic systems, on the other hand.
For more information, please refer to the publications and posters of this project.
|
