veriGEM (NWO/Focus)

A Verification Grid for Enhanced Model Checking

Project Manager: Prof. dr. ir. Boudewijn Haverkort

Faculty of Electrical Engineering, Mathematics and Computer Science

Tel.: +31 53 489 3766

Project website:

Project Summary

In this project we aim to design and build a distributed model-checking infrastructure for verifying system properties. Designing and studying (software) systems using abstract behavioural models is becoming more and more feasible due to the increased capabilities of verication techniques that have lately been developed. The most important of such techniques is model checking, where the validity of formally-specied requirements can be checked on the model. Both these improved methods and increased capabilities of computers are a driving force behind the increased feasibility and applicability. In this project we want to push the limits of verication technology further by employing networks of workstations on a large scale. Concretely, we want to arrive at the situation where we can verify practical modal formulas (containing data and/or stochastic information) on large models using the storage and processing capacity of interconnected networks of workstations. We will not only employ standard model checking algorithms, but will especially also develop new model checking algorithms for extended model classes, and will combine them with algorithms for model reduction, symbolic reasoning and theorem proving techniques. In particular, we will develop variants of these new algorithms that can be executed effciently on a nation-wide interconnected networks of workstations (a grid).

Publications

Project duration: 1-9-2005 / 1-9-2008

Project budget: 497 k-€ / CTIT-budget: appr. 185 k-€

Number of person/years: 3.2 fte / year

Project Coordinator: UT/CTIT

Participants: UT/CTIT, CWI, TU/e

CTIT Strategic Research Orientation: DSN - Dependable Systems and Networks