Object-Oriented VErification (GROOVE)
GROOVE is a project centered around
the use of simple graphs for
modelling the design-time, compile-time, and run-time structure of
object-oriented systems, and graph transformations as a basis for model
transformation and operational semantics. This entails a formal
foundation for model transformation and dynamic semantics, and
the ability to verify model transformation and dynamic semantics
through an (automatic) analysis of the resulting graph transformation
systems, for instance using model checking.
Background and Motivation
compile-time models and their transformation
) offers a wealth of diagrammatic
modelling techniques for various
design aspects of object-oriented systems. These include especially
models for the static structure (class diagrams) and for the dynamic
behaviour (sequence, activity and state diagrams). In addition,
in a later stage of the development there are various types of models
used in program analysis, such as flow graphs, call graphs and
dependency graphs. There is, of course, a clear overlap between the
various types of models, both within and across development phases.
(XML) provides a way to model
(essentially) arbitrary kinds of data, by
imposing a certain tree-like structure upon it. Using this structure,
the data can then be stored and interchanged in a standardized textual
format. The structure itself, however, irrespective of its
representation, functions as a model of the data in question. As soon
as one uses XML to encode also UML-type diagrams, this results in a
multiplication of models of essentially the same thing.
In addition to these explicit types of
models, there is always the
actual source code of the system. We believe that it is useful to
regard this, too, as a model of the system - one that is executable.
Seeing it in this light puts a more uniform perspective on the area,
since here, too, there is overlap between models (e.g., between the
design model and the code), and consequently, the issues regarding
explicit, UML- end XML-type models, also apply to explicit models and
source code - arguably even to a stronger degree.
The need to reason about and transform models is felt in
have different types of models for overlapping aspects of a system,
inconsistencies between them may easily arise. This is a problem not to
be underestimated, and given the complexity of systems, it is not
enough to rely on manual consistency checks. Tool support is both
necessary and feasible; but what should the tools support? For
starters, it is imperative to check
consistency across models in a generic way, not ad hoc for a predefined set of
models but systematically from an externally provided set of
consistency constraints, so that this can be extended easily to new
(e.g., domain-specific) models with their own specific constraints.
Ideally, though, one would also want to maintain consistency
automatically, by carrying transformations in one model through to
other, overlapping ones.
activity in software development is to take the current stage at which
a system has been developed to the next stage, where each stage
provides more design decisions and/or implementation details. This
process is often called refinement.
In a context where the "current state" and "next stage" are described
through models, refinement becomes a model transformation activity.
This may involve, on the one hand, transformations within models of the
same types, or transformations across models of different types. If the
"next stage" model is a more implementation-oriented one than the
"current state", then we have a transformation of the type studied in
the approach of Model
Driven Architecture (MDA).
design-time, semantics-preserving architectural changes.
It is nowadays
recognized that virtually no computer system is developed once and for
all and stable ever after. Adaptation and extension are the norm - not
to mention corrective maintenance. More often than not, the current
practice is to take the source code of
an existing system and modify it, without regarding other, overlapping
models (see above). The dangers of this are widely
recognized. In fact, MDA, is effectively a large scale effort to
improve this practice: a major component of MDA is
to preach model transformation, rather than code modification, as the
level on which evolution should take place.
storage and interchange.
Run-time models and
A run-time model is an abstraction of
the state of a system at
run-time; i.e., a snapshot. Run-time models can be combined into transition systems that represent
the dynamic semantics of the sytem, by describing it in terms of states
and transitions between them. It is typically upon such transition
systems that verification of dynamic properties is carried out, through
model checking. This involves checking that a given invariant property
holds on all states, or more generally, that a temporal safety or
liveness property holds across states. The properties to be checked can
be predefined or user-provided.
Because state spaces tend to be
extremely (in general unboundedly)
large, the choice of modelling technique, and of abstraction level on
which to model the behaviour, are crucial to the success of this type
of verification. Choosing the right modelling technique may help to see
symmetries or similarities between distinct states, which allows them
to be combined, leading to a state space reduction; likewise,
abstraction removes detail from the individual states, which in turn
may give rise to new symmetries over the remaining structure. Since, in
general, abstraction leads to a loss of precision in the verification
results, it is often done in conjunction with the property to be
checked, so as to ensure that the details relevant to that property are
disturbed as little as possible.
We thus recognize at least two types of
model transformation in this
transition system approach, each transition represents an execution
step taking the system from one state to the next. The target state is
effectively a transformation of the source state.
of removing details from the individual states, described above,
entails a transformation from concrete to abstract run-time models.
State space reduction through similarity checking can be seen as a
special case of abstraction.
Graphs and graph
Within the GROOVE project we take the
point of view that graphs are a
very good basis for both design-time and run-time models of (software)
systems. Graphs have the advantage of a visual representation (even
though this tends to remain practical only for small-scale exmples)
and, more importantly, a rich formal foundation; in addition, they are
flexible enough to deal with all kinds of models without a priori constraining them.
Finally, in the long-standing theory of graph transformation we find a mathematical tool to formalize
many, most, or even all of the types of transformation discussed above.
For UML models, it is immediately clear
the the diagrams are, in
fact, highly structured graphs. We strongly believe that most of this
structure can be seen as logical constraints upon simpler graphs; that
is, UML models are structured views upon (a set of) more extensive,
more detailed and more primitive models that are simple graphs. (In
fact, the relation between the simple graph model and the more
structured UML view upon it is itself nothing but a transformation.)
For XML models, the step in viewing them as graphs is almost as
immediate: the heart of the models is a tree structure, possibly with
additional links. Viewing source code as graphs, too, is a well known
concept: on a trivial level, every program can be equated with its
syntax tree, but more sophisticated instruments such as call graphs,
flow graphs and dependency graphs are heavily used in all types of
source code metrics and static analysis.
Regarding run-time modelling, we
believe that graphs are very well
suited for modelling state snapshots of systems that involve
dynamic allocation and de-allocation of storage space and dynamic
method invocation. In traditional, implementation-oriented terminology,
we see graphs as a generic solution to model both the heap and the stack of programs; and so both
heap analysis and stack inspection (to name but two active research
areas) are verification techniques that can be understood very well as
constraint checking upon graphs.
The following publications and tools arose, directly or indirectly, out
of the work in this project.
The work described in the following papers provided us with much
of the motivation underlying this project:
- Who is
pointing when to whom: On model-checking pointer structures
(Dino Distefano, Arend Rensink and Joost-Pieter Katoen).
CTIT Technical Report TR-CTIT-03-12, Department of Computer Science,
University of Twente, September 2003.
- Model checking birth and death (Dino
Distefano, Arend Rensink and Joost-Pieter Katoen).
In R.A. Baeza-Yates, U. Montanari and N. Santoro, editors, Foundations
of Information Technology in the Era of Network and Mobile Computing,
volume 223 of IFIP Conference Proceedings, pages 435-447.
Kluwer Academic Publishers, 2002.
checking dynamic allocation and deallocation (with Dino
Distefano and Joost-Pieter Katoen).
CTIT Technical Report TR-CTIT-01-40, Department of Computer Science,
University of Twente, March 2002.
- On a temporal logic for object-based systems (Dino
Distefano, Joost-Pieter Katoen and Arend Rensink).
In S. F. Smith and C. L. Talcott, editors, Formal
Methods for Open Object-based Distributed Systems, pages
305-326. Kluwer Academic Publishers, 2000.
Report version: TR-CTIT-00-06, Faculty of Informatics, University of
- Model Checking Dynamic States in GROOVE (Harmen
Kastenberg and Arend Rensink). In Proceedings of the 13th
International Workshop on Software Model Checking (SPIN'06),
Volume 3925 of Lecture Notes in Computer Science, Springer-Verlag,
2006. To appear. (PDF)
- Towards Attributed Graphs in GROOVE (Harmen Kastenberg).
In Proceedings of the International Workshop on Graph
Transformation for Verification and Concurrency (GT-VC),
Electronic Notes on Theoretical Computer Science, Elsevier, 2005. To
- Canonical graph shapes (Arend Rensink). In European
Symposium on Programming (ESOP), Volume 2986 of Lecture Notes in
Computer Science, Springer-Verlag, pp. 401-415, 2004. (PDF,
- State space abstraction using shape
graphs (Arend Rensink). In Automatic Verification of
Infinite-State Systems (AVIS), Electronic Notes in Theoretical
Computer Science. Elsevier, 2004. To appear. (PDF,
- The GROOVE simulator: A tool for state space generation
(Arend Rensink). In M. Nagl and J. Pfalz, editors, Applications
of Graph Transformations with Industrial Relevance (AGTIVE),
Volume 3062 of Lecture Notes in Computer Science, Springer-Verlag, pp.
479-485, 2003. (PDF,
- A logic of local graph shapes (Arend
Rensink). CTIT Technical Report TR-CTIT-03-35, Faculty of Informatics,
University of Twente, August 2003. (PDF, BibTeX)
- Towards model checking graph grammars
(Arend Rensink). In M. Leuschel, S. Gruner and S. Lo
Presti, editors, Proceedings of the 3rd Workshop on
Automated Verification of Critical Systems, Technical Report
DSSE-TR-2003-2, pp. 150-160, University of Southampton, 2003. (PDF, BibTeX)
As discussed above, a major outcome of this project is a tool
environment supporting the use of graphs for the purposes described
here. The most recent version of the tool can be found here. Currently it
the tool was assisted by the use of the Yourkit Java Profiler
- A graph editor, capable of producing plain graphs and graph
transformation rules in GXL format;
- A graph grammar simulator, capable of generating a transition
system from a graph production system (given in either of several XML
- Through manual simulation, including backtracking
- Through automatic exploration, using linear, branching or full
- A set of sample graph production systems, modelling (among others)
- A list append function
- Circular and sequential buffers
- The ferryman problem
In development are:
Planned future extension are:
- A translator from Java source code to graph production systems
- A translator from Java byte code to graph production systems
- A metrics tool suite for Java programs
- Automatic abstraction
- A model checker for the graph transformation system generated by