|
Click on a theme or a project in the table below for more information.
Project leader:
Prof.dr.ir. Boudewijn Haverkort (UT)
Consortium:
UT, CWI and TU/e
Related projects:
BRICKS AFM8
Total FTE: 4.3 (heads: 7, faculty: 0.3, PD: 3, PhD: 1)
Key BRICKS publications:
| • |
J.-F. Groote, A.H.J. Mathijssen, M.A. Reniers, Y.S. Usenko and M.J. Van Weerdenburg. Analysis of distributed systems with mCRL2. In: M. Alexander, W. Gardner (Eds.), Process Algebra for Parallel and Distributed Processing, pages 99-128. Chapman and Hall, 2008.
|
| • |
J.-F. Groote, T.A.C. Willemse. Parameterised Boolean Equation Systems. Theoretical Computer Science 343: 332-369, 2005.
|
| • |
A. Bell, B.R. Haverkort. Distributed disk-based solution of very large Markov chains. Formal Methods in System Design 29(2): 177-196, 2006.
|
| • |
L. Brim, B.R. Haverkort, M. Leucker, J. van de Pol, editors. Formal Methods: Applications and Technology. Lecture Notes in Computer Science 4346, 2006.
|
| • |
M. Hammer, M. Weber. "To store or not to store" reloaded: Reclaiming memory on demand. Lecture Notes in Computer Science 4346: 52-67, 2006.
|
|
Project AFM6: A Verification Grid for Enhanced Model Checking
Designing and studying (software) systems using abstract
state-based behavioural models is becoming more and more feasible
due to the increased capabilities of verification techniques that
have recently been developed. The most important verification
technique is model checking. The VeriGEM project will push the
limits of model checking by employing work-station clusters and
GRIDs to perform the verification task. Concretely, we aim to
arrive at the situation where we can verify logically specified
system characteristics (possibly containing data, time and
stochastics) on large models using the storage and processing
capacity of clusters of workstations on a nation-wide scale.
Starting point for our work are well-studied sequential algorithms
for CTL model checking and Boolean equation systems (which are used
for verifying properties specified using the mu-calculus). Research
is based on experience gathered by the project members, for
instance on distributed state-space generation, distributed CTL
model checking and distributed bi-simulation reduction.
The project has three important focal areas. First, the techniques
of distributed model checking are geared towards models that are
stochastic. This implies that the underlying state-based models
become, in essence, stochastic processes for which distributed
numerical algorithms have to be employed as part of the model
checking process. Second, these distributed algorithms are extended
to cope with data. As data generally implies infinite state spaces,
e.g., unbounded sequence numbers, infinite queues, this calls for
the development of distributed symbolic techniques. Third, we
investigate distributed abstraction techniques. We base ourselves
on recently developed distributed bi-simulation algorithms for
state-space reduction, thus making classical sequential techniques
applicable to much larger models.
Industrial cooperation
The participants in this project cooperate with a variety of
industrial parties, among others with Thales, ASML, Philips,
TNO-ICT and Océ, NXP Semiconductors and Imtech ICT Technical Systems.
International cooperation
The three research groups involved in this project maintain a large
network of international cooperation. For VeriGEM, the cooperation
with the TU München (Leucker), the University in Brno (Brim) and
INRIA Rhône-Alpes, Grenoble (Garavel) deserve attention. In 2006,
we organised several international workshops on parallel and
distributed model checking. At CWI, an EU project started (EC-MOAN)
which includes a work-package on distributed model checking.
Highlights 2006
This project is financed through the first open call of the BRICKS program (July 2005) and started only in the last months of 2005.
Research highlights
- Development of theory and an implementation for a model checking tool based on external memory.
- A study of the use of cluster and GRID technology for application in model checking context.
- A study of the potential for distributed algorithms for CSL and CSRL model checking.
- Definition (and implementation) of a translation of the validity of modal logic formulas with time and data for parallel processes to Boolean equation systems.
Economic & societal impact
Complex engineering requires abstract models for the objects that
are constructed. Through model analysis, the strengths of designs
can be ascertained before construction. For computer-based systems,
such model-based design did not really take off, since there are no
generally accepted modelling techniques, nor strong means to
analyse these models. This is the major reason why most software
projects do not deliver as intended; correct software construction
has become the weakest link in many engineering projects! The
VeriGEM project focuses exactly on improving these analysis
techniques, thereby emphasizing on increasing the size of models
that can effectively be handled, using clusters and grids.
Future work 2007-2009
We will refine the developed theory and implement tools that allow
us to use and compare distributed algorithms for CTL and CS[R]L
model checking, as well as for distributed mu-calculus and pBES
solvers. We will also integrate the developed approaches toward
distributed bi-simulation reduction as a pre-processing step before
model checking
AFM6 Researchers funded by BRICKS
- Prof.dr.ir. B. Haverkort (UT)
- Dr. M. Weber (CWI)
- Dr. G.W.M. Kuntz (UT)
- Prof.dr. J. van de Pol (UT)
- Prof.dr. J.F. Groote (TU/e)
- Dr.ir. Aad Mathijssen (TU/e)
For more information, please refer to the publications and posters of this project.
|
