current work

Externally funded projects

We have been awarded several grants. Details can be found on the Projects page.

Expressiveness and Decidability

Formalisation

The main thrust of our work on the modelling side is the development of diagrammatic notations for use with the Unified Modelling Language (UML) notations in software development.  One such notation is constraint diagrams, which was designed to express visually mathematical constraints such as system invariants and operation preconditions and postconditions. The group is currently completing the formalisation of constraint diagrams and developing a reading algorithm for the notation.

Modelling

We are developing case studies using the notations and comparing the results with similar systems developed using UML or mathematical notations.
This work is in collaboration with Steve Schuman at Brighton.

Diagrammatic reasoning

Out of the investigation into constraint diagrams arose the visual notation spider diagrams. These are based on Venn and Euler diagrams and build on a long tradition of such notations. The group has given formal semantics to the notation in terms of set theory/first-order predicate logic. Diagrammatic reasoning rules have been developed for spider diagram systems and these have been proved to be sound and complete. The group is now investigating reasoning rules for constraint diagram systems.

Automated reasoning

We have developed tools to automate reasoning with diagrammatic logics. We have implemented theorem provers for Euler diagrams and spider diagrams.

Abstract and concrete diagrams

Diagrammatic notations can be given a formal concrete syntax in terms of, for example, topological elements such as Jordan curves and a formal abstract syntax in terms of, for example, many-sorted algebras. An abstract diagram is independent of any drawn representation, but any concrete diagram, or token, must comply with its abstract diagram, or type. The group is investigating the relationships between abstract and concrete diagrams and believe that this area is important in the understanding the nature of formal diagrammatic notations and how they differ from textual and symbolic notations.
This work is in collaboration with Sun-Joo Shin of Yale University, USA.

Usability

We are investigating applying cognitive dimensions to study the usability of the notations.
This work is in collaboration with Lyn Pemberton of the Usability Group at Brighton.

Generating diagrams

The group has developed and implemented an algorithm that takes an abstract Euler diagram and delivers a concrete diagram. The paper describing this work was voted best paper at the Diagrams 2002 conference in Georgia.
This work is in collaboration with Peter Rodgers of UKC.

Implementation in PVS

The group is working in collaboration with Manuel Barrio Solorzano of the University of Valladolid in Spain on implementing the spider diagram system SD2 in PVS.

Projections

A projection within a diagram based on Venn or Euler diagrams is a device for removing clutter and focusing attention appropriately. They may also be important in modularising and nesting diagrams. We are investigating the properties and applications of projections.

Textual languages

The group also has interests in UML's (textual) assertion language OCL and in languages designed for run-time checking of logical assertions such as Eiffel's assertion language and the Java Modelling Language (JML) and also in mathematically-based notations such as Larch and Z.

Combinatorics

We have been counting abstract Euler diagrams and the number of labelled and unlabelled concrete diagrams satisfying different well-formedness criteria.