Tools for PSF
G.J. Veltink

Abstract:
This thesis describes the PSF Toolkit, a set of software tools for specifying concurrent processes based on the specification language PSF (Process Specification Formalism). It is divided into three main parts: languages, tools and case studies.

The first part of this thesis describes the languages that play a role in the implementation of the PSF Toolkit. Chapter 1 describes PSF; the main high-level language used to describe concurrent processes in this thesis. The different language constructs are introduced in an incremental way and their usage is illustrated by means of a running example that gets more complicated as more language constructs are introduced. Along with the syntax of each language construct its semantics is defined.

Although PSF is a suitable language for humans to express the behaviour of parallel processes, it is not the optimal language to be used as an interface between different computer tools. A tooling environment can strongly benefit from a layered design using different languages at different levels of abstraction. The low-level Tool Interface Language (TIL) used in the PSF Toolkit is introduced in Chapter 2.

Chapter 3 describes the process of translating PSF into TIL. Apart from transforming expressions from one syntax into another there is one more important transformation that is described in this chapter, namely the process of removing the modular structure from a PSF specification, also called normalization. PSF supports the use of modules to group related parts of a specification into a hierarchical design. The module concept is mainly there to be able to organize large specifications in the high-level design and as such is an aid in keeping an overview. However, on the level of computer tools such a modular structure is of no importance and one large specification, without any extra structuring mechanisms, is preferred.

The second part of the thesis focuses on the tools in the PSF Toolkit. Chapter 4 is dedicated to the simulator, a tool that simulates the behaviour of a specification. The simulator is an interactive tool, which means that, in order to study the response of a specified system in different situations, the user can influence the behaviour of the simulated system in real- time by supplying different external events. Chapter 4 starts with a description of the basic algorithmic operation of a simulator, namely calculating the head normal form of a process expression. This description is an algebraic specification written in PSF itself. Then the actual implementation of the simulator along with its user interface is described.

In chapter 5 the proof assistant of the PSF Toolkit is described. The proof assistant is a tool that allows to construct proofs through a step by step transformation of process expressions. The great benefit of the tool is that it is capable of suggesting to the user all transformations possible according to the semantics of the process operators. This tool also incorporates so-called tactics which are special sequences of frequently used proof steps. The user interface and the implementation of the proof assistant is discussed and an example of its use is given.

Chapter 6 shortly discusses all other tools in the PSF Toolkit, including the term rewriter, the compiler driver and library manager, the initial algebra generator, the transition system generator and the equivalence tester.

The third part of this thesis deals with two case studies which have been carried out using the language PSF and the tools from the PSF Toolkit. The first case study, described in chapter 7, deals with a courseware project that evolved from a course in Software Engineering. This project aims at offering a so-called software harness for giving an algebraic specification of a compiler for a simple programming language.

Chapter 8 gives a specification of part of the GKS (Graphics Kernel System) ISO Standard using an existing specification in CSP as starting point. Here it is shown that the availability of a set of tools is of great importance for checking both the syntax and correctness of a specification.

Finally chapter 9 concludes this thesis with an evaluation of the development of PSF and the PSF Toolkit. It shows the weak and strong points of the design and its implementation and gives some suggestions for improvements and future developments.