This work is part of the DisCo project. It covers main themes of my licentiate thesis published June 16., 1995.
Tommi Mikkonen
Tampere University of Technology
BOX 553, SF-33101 Tampere, Finland
tjm@cs.tut.fi
The implementation of a formal specification is a complicated task. In case of DisCo, the task is even more complicated, since every DisCo specification is closed. In a closed specification, there can be outside observers, but no interactions between the system and the outside world. Thus, the specification is complete in sense that it contains everything that can affect its operation. The activity of the environment is modelled by using nondeterministic features.
However, no matter how sophisticated a specification is, it must be implemented before it can be used. An implementation of an interactive system is always an open one. It has a specific implementation environment and the environment can interact with the implementation. Thus, when implementing a specification, an environment must be presented to it.
The long-term goal of this work is to provide a generator that would implement DisCo specifications. This generator would use some kind of generic implementation environment, which could easily be modified. However, there are still unanswered issues in the implementation area.
The thesis is structured as follows.
An introduction to the formal methods and their use in general is presented in the first chapter. The motivation to use formal methods is discussed to show that they provide more trust on the systems under construction. The distinction between a closed and an open system is also presented in this chapter. Basicly, the difference is that a closed system has no interactions with the outside world but it is a complete description of its own universe. An open system is one that is in continuous interaction with its environment. When a closed specification is to be implemented, then it must be partitioned into a system part which is to be implemented and into an environment part which is the implementation environment.
In the second chapter I introduce the the temporal logic of actions (TLA) that will be the specification method used in the thesis. Some of the aspects, such as inference rules, are not presented, since the aim is to introduce the properties that are needed in the following chapters. DisCo specifications are based on TLA, and therefore, TLA is used in the following chapters instead of DisCo to achieve a more solid basis for implementation decisions.
The third chapter will present how partitioning of specifications should be done in order to split the specification into implementation and its environment. The chapter lists requirements for implementation in terms of the logic. Also,I introduce a way by which the environment can interact with an implementation. The approach is based on TLA specification and uses the features of C language in the implementation.
Sometimes the granularity of the specification may be wrong when implementation phase should start. In the fourth chapter, I present a way to break the atomicity proposed to the actions of the specification. A set of requirements is presented for correct implementation.
The underlying model of specification in my thesis is DisCo. Therefore, the fifth chapter discusses the above solutions from the viewpoint of DisCo method. Although DisCo is formalized in terms of TLA, it is not that clear that the above refinements can be applied to DisCo because of restrictions when refining DisCo specifications.
Some comments and remarks are presented in the last chapter.