|
Click on a theme or a project in the table below for more information.
Project leader:
Dr.ir. Tim Willemse (TU/e)
Consortium:
TU/e
Industrial partners (non-exhaustive):
Techniques currently under development in the project have attracted the attention of industrial partners (e.g. Philips Medical Systems, ASML), but these techniques are currently too premature for a successful application in the industry.
Related projects:
BRICKS AFM6
Total FTE: 2.2 (heads: faculty: 7, assistant prof.: 3)
Key BRICKS publications:
| • |
S.M. Orzan, J.W. Wesselink and T.A.C. Willemse. Static Analysis techniques for Parameterised Boolean Equation Systems. In S. Kowalewski and A. Philippou, editors, Proc. TACAS 2009, volume 5505 of Lecture Notes in Computer Science, pages 230-245, 2009.
|
| • |
S.M. Orzan and T.A.C. Willemse. Invariants for Parameterised Boolean Equation Systems (extended abstract). In F. van Breugel and M. Chechick, editors, Proc. CONCUR 2008, volume 5201 of Lecture Notes in Computer Science, pages 187-202, 2008.
|
| • |
A. van Dam, B. Ploeger and T.A.C. Willemse. Instantiation for Parameterised Boolean Equation Systems. In J.S. Fitzgerald, A.E. Haxthausen and H. Yenigun, editors, Proc. ICTAC 2008, volume 5160 of Lecture Notes in Computer Science, pages 440-454, 2008.
|
| • |
T. Chen, B. Ploeger, J. van de Pol and T.A.C. Willemse. Equivalence checking for infinite systems using Parameterized Boolean Equation Systems. In Proc. CONCUR 2007, volume 4703 of Lecture Notes in Computer Science, pages 120-135, 2007.
|
| • |
S. Orzan and J.F. Groote. Parameterised Anonymity. In Proc. FAST'08, Lecture Notes in Computer Science, 2009.
|
|
Project AFM8: A Common Framework for the Analysis of Reactive and Timed Systems
The field of analysis of computerised systems is scattered with
theories that have been obtained in narrow classes of models. Prime
examples are decidable model checking techniques for real-time
systems, and sophisticated reasoning techniques such as the Cones
and Foci technique for proving two data-intensive systems
equivalent. A faithful specification of complex computerised
systems typically requires one to express a combination of
real-time, data and sometimes even hybrid aspects. Such complex
systems are currently not well supported with the required powerful
analysis techniques. As a result, many complex systems fail to live
up to their potentials.
A unifying framework
We observe that the strict boundaries between many classes of
models has impaired the cross-fertilisation of techniques from one
area to another. A solution to this problem is to recast known
techniques into a single framework. Parameterised Boolean Equation
Systems (PBESs), a theory of fixpoint equations, have been
fundamental in the context of model checking both data-dependent
systems and real-time systems. In particular, it is known that
these model-checking problems can be rephrased as a PBES solution
problem. A specialisation of PBESs, called Boolean Equation Systems
can be used to code many well-studied behavioural equivalence
relations. This suggests the framework of PBESs is well-suited for
investigating the unification of existing techniques and theories.
Studying techniques from different areas in a single framework
ultimately leads to cross-fertilisation and is bound to give rise
to larger classes of systems that can be analysed effectively.
Solution techniques for PBES
The techniques that have so far been coded in the PBES framework
essentially rely on being able to solve a PBES; we expect this also
holds for most other techniques that can be cast into the PBES
framework. Solution techniques for PBESs are therefore crucial, but
computing a solution for a PBES is in general an undecidable
problem. For this reason, full automation can in general not be
obtained. As a result of earlier investigations, however, a host of
solution techniques is already available. Among these are the use
of patterns that allow for simple "look-up and
instantiate" operations that simplify or solve PBESs. Such
techniques have so far been the reserve of e.g. computer algebra
systems. We expect to find novel solution techniques by rephrasing
known decidable problems as solution problems for PBES.
Industrial cooperation
Many of the research problems that we address are instigated by
case-studies originating from industrial parties, including for
example Philips Medical Systems, ASML, Océ and TNO.
Tooling that has been developed in the context of this project
has been applied amongst others at Philips Healthcare, Philips Research,
VanderLande Industries, Vitatron and NBG.
International cooperation
In the context of BRICKS, we actively collaborate with renowned
international research institutes. These include, among others,
INRIA Rennes, INRIA Rhône-Alpes, ISTI, Norwegian University of
Science and Technology, Reykjavík University and
Universiteit Twente (Formal Methods and Tools).
Highlights 2004-2006
As this project is part of the third phase of the BRICKS program
(financed through the second open round July 2006), challenges
rather than results are presented.
Research challenges
A team of
three assistant professors is assigned to the project: Dr. Simona
Orzan, Dr.ir. Wieger Wesselink and Dr.ir. Tim Willemse. Dr. Simona
Orzan will be investigating partial order and symmetry reduction
techniques in the setting of data-dependent, real-time model
checking. Partial order reduction techniques have been conjectured
to be linked to techniques such as patterns and solution
strengthening and weakening for PBESs. Dr.ir. Wieger Wesselink is
in charge of developing tool support and the required theory for
PBESs. Proof-of-concept prototype tooling has thus far been a
driving force behind the progress in theoretical PBES
investigations. This tool support is indispensable for conducting
case-studies. Dr.ir. Tim Willemse investigates novel solution
techniques for PBESs by casting existing proof techniques, and
problems which are known to be decidable in the PBES framework.
Furthermore, he is incorporating real-time extensions in the
existing translation into PBESs of the model checking problem for
data-dependent systems.
Future work 2007-2009
The challenges highlighted above are planned for the next few
years. Active international collaboration will be sought to address
challenging topics.
AFM8 Researchers funded by BRICKS
- Dr.ir. Tim Willemse (TU/e)
- Dr.ir. Wieger Wesselink
- Dr. Simona Orzan
For more information, please refer to the publications and posters of this project.
|
