GRaphs for Object-Oriented VErification (GROOVE)

Background and Motivation

Design- and compile-time models and their transformation

The Extensible Markup Language (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.

• Verification. Since we 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.
  
• Refinement. The core 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).
• Refactoring. Small-scale, design-time, semantics-preserving architectural changes.
• Evolution. 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.
  
• Serialization. Model storage and interchange.
  

Run-time models and dynamic semantics

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 context:

• Execution. In the 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.
  
• Abstraction. The process 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 transformations

Project aims

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.

Project results

Previous work

• 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. (PDF, BibTeX)
• 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. (BibTeX)
• Model 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. (PDF, BibTeX)
• 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 Twente. (PostScript, BibTeX)

Project publications

• 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 appear. (PDF)
• 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, BibTeX)
• 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, BibTeX)
• 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, BibTeX)
• 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 3^rd Workshop on Automated Verification of Critical Systems, Technical Report DSSE-TR-2003-2, pp. 150-160, University of Southampton, 2003. (PDF, BibTeX)

Tool set

• 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 formats):
• Through manual simulation, including backtracking
• Through automatic exploration, using linear, branching or full exploration
  
• A set of sample graph production systems, modelling (among others)
• A list append function
• Circular and sequential buffers
  
• The ferryman problem

In development 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 simulation