Click on a theme or a project in the table below for more information.
Project leader:
Dr. Mariëlle Stoelinga (UT)
Consortium:
UT
Total FTE: 3.4 (heads: 8 faculty: 0.4, PD: 2, other: 1)
Key BRICKS publications:
| • |
Brandán Briones, Brinksma and Stoelinga. A Semantic Framework for Test Coverage. Proceedings ATVA 2006.
|
| • |
Chatterjee, de Alfaro, Faella, Henzinger, Majumdar, and Stoelinga. Quantitative Compositional Reasoning. Proceedings of QEST 2006.
|
| • |
Cloth, Haverkort. Five Performability Algorithms: A Comparison, Proceedings Markov Anniversary Meeting 2006.
|
| • |
Remke, Haverkort, Cloth. A Versatile Infinite-State Markov Reward Model to Study Bottlenecks in 2-Hop Ad Hoc Networks, Proceedings of QEST 2006.
|
| • |
Baier, Cloth, Haverkort, Kuntz, Siegle. Model Checking Markov Chains with Actions and State Labels, forthcoming in IEEE TSE, 2007.
|
|
Project AFM7: MOQS: Modeling and Analysis of QoS for Component-Based Designs
With software becoming more and more complex, its development
shifts towards component-based design (CBD). In this way, the
complexity of a large system is broken down into several small and
manageable pieces. An ubiquitous challenge in CBD is the prediction
of global system properties from the individual component
properties, especially for extra-functional requirements such as
quality of service (QoS), reliability and responsiveness. This
project develops methods and tools for the design-time analysis of
QoS properties of component-based systems. Since QoS properties are
usually stochastic in nature, we base our techniques on stochastic
modeling and analysis methods. In particular, we summarize a
component's QoS requirements in an interface automaton. To
verify the compliance of a component with its interface, we extend
(stochastic) model checking, model-driven testing (MDT) and
abstraction techniques. We implement these techniques into a tool
environment based on existing tools like TorX, Modest/Motor and
MRMC.
Modeling of system reliability
This subproject investigates dynamic fault trees (DFTs), a language
to model and analyze the reliability of component-based systems. We
formalize the syntax and the semantics of DFTs in terms of
Input/Output interactive Markov chains (I/O-IMC). These extend I/O
automata by including transitions that represent stochastic delay
actions. This formalization allows us to analyze DFTs with existing
I/O-IMC analysis techniques in a modular fashion.
QoS analysis with MRMs
Markov Reward Models (MRMs) have a long tradition in the evaluation
of performance and dependability attributes, also referred to as
QoS attributes. For a convenient tool-based evaluation of such
attributes, we are developing a formal and easy-to-use language for
the specification of QoS properties, based on temporal logics.
These specifications, together with a behavioral specification of
the system, are written using stochastic process algebra or
stochastic Petri nets. They allow us to fully automatically
evaluate whether a system conforms to its specification. We develop
new numerical techniques to do these evaluations efficiently and
apply our techniques to real-world case studies, recently, among
others, on a wireless LAN multi-hop ad hoc network.
Industrial cooperation
In this project, we cooperate with a variety of high-profile
industrial parties, including ASML, Thales and ESI.
International cooperation
In the context of BRICKS we actively collaborate with a wide
variety of internationally well-renowned research institutes,
including University of California at Santa Cruz, RWTH Aachen,
Technische Universität Dresden, Universität der Bundeswehr München,
Radboud Universiteit Nijmegen.
Highlights 2004-2006
As a part of the second phase of the BRICKS program (financed
through the first open round July 2005), the project is only
currently in full swing.
Research highlights
A variety of
ground-breaking research results have been obtained in many areas,
including the following: 1.A framework to measure and optimize how
well a specification is covered by a test suite. 2.A compositional
semantics for analyzing DFTs in terms of I/O-IMCs. 3.A framework to
analyze quantitative system properties in a compositional way. 4.A
set of model checking algorithms for extended logics (like asCSL)
as well as prototypical implementations.
Economic & societal impact
Various results on model-driven testing and the tool TorX are
applied within Axini, a spin off company from a previous STW
project that helps its customers to improve their testing process.
Future work 2007-2009
We plan to extend our test coverage techniques with more powerful
optimization techniques and the DFT to a richer class of DFTs. The
new algorithms for QoS evaluation will be further developed and
integrated in the MRMC model checking tool.
AFM7 Researchers funded by BRICKS
- Prof.dr. Ed Brinksma (UT/ESI)
- Prof.dr.ir Boudewijn Haverkort (UT)
- Prof.dr.ir. Joost-Pieter Katoen (UT/RWTH)
- Prof.dr. H. Hermanns (UT)
- Dr. Marielle Stoelinga (UT)
- Dr. Hichem Boudali (UT)
- Dr. Lucia Cloth (UT)
- Andre Nijmeijer (UT)
For more information, please refer to the publications and posters of this project.
|
