Semantic tools

Computer technology plays an ever increasing role in our lives and is at the core of many critical applications. The variety of this technology has increased over the last two decades. We now have devices ranging from mobile phones, tablets, traditional PC, servers (with varying levels of virtualisation) and supercomputers. Furthermore, the traditional CPU is being augmented as a processing unit by GPUs (Graphics Processing Units) that have a very different architecture. In addition to this, interactions between different components is becoming more complex. As the role of computers become more important, and to some extent more hidden, for example computers as engine controllers in cars, reliability and security become crucial. Traditional methods that validate the safety and reliability of this technology need to be augmented with theory based tools.

REMS (Rigorous Engineering for Mainstream Systems) is an EPSRC funded programme that seeks to apply formal methods to solving problems in the engineering of computer systems. The program is subdivided into four tasks: three of the tasks are to investigate the behaviour of multiprocessor architectures, system programming languages and concurrent software. The fourth task is to provide the tools to support the other three. These tools aim to capture the semantics and behaviour of systems in a mathematically precise language.

One such tool that has already been developed is Lem. This is a lightweight tool for developing large scale semantics and includes the ability to export to programming languages for execution and theorem provers to allow the specification and proof of properties. Lem has been used successfully to specify the semantics of CPUs and programming language concurrency and from this use a number of fundamental problems with the current implementation have been identified.

This research proposes to continue the development of these tools. To this end, it will build on ideas from three sources - mathematical theory (by applying existing theory and developing my own), application areas (the three tasks above and others as they arise) and existing tools (tools developed within the REMS project and from other initiatives).

It will investigate the mathematical ideas that can be used to model these systems and incorporate these into the tools. For example, within LEM by enhancing the language or providing a Lem library and associated backend libraries. Also working backwards from existing models and looking at how the techniques that have already been used can be formalised and enriched.

A potential area of work is enhancing Lem. The research would begin with building an understanding of the current and proposed uses of Lem and how the improvements outlined above would benefit these uses. It is also proposed to develop a deeper understanding of the underlying theory and finally implement the new version.

Another area of focus would be relations; both as a means of defining a model and also used within the model itself. Inductive relations are a key mathematical tool for describing systems and an important part of a model are the relationships between objects in the model. For example, in a concurrency model there are actions such as reads and writes and a number of different relationship types between these actions such as a relation describing data dependencies and a relation describing synchronisation. Key to the use of relations is being able to transform them from a purely logical construct into something that can in some sense be executed or queried - this is termed 'animating' the relation.