A Standard for Finite TAM1

David Scholefield, Hussein Zedan
Formal Systems Research Group
Department of Computer Science
University of York
Heslington, York, YO1 5DD

August 12, 1993

Abstract

Since its inception in 1991, the Temporal Agent Model theory (TAM) has undergone a number of changes; some of these changes have been minor (such as a change in the style of semantic presentation) and some have been more major (such as the addition or subtraction of programming constructs from the TAM language). Throughout these changes however, the computational model underlying the theory has remained constant, allowing for a comparison of different flavours of the language. This has proved a fruitful area of research, but has also meant that references to the TAM theory may be ambiguous. In this paper we present a standard TAM theory, including a language syntax, semantics, and refinement calculus, and propose that this standard be used in future TAM projects. We also discuss refinement hueristics for ensuring implementable programs.

1 Introduction

In January 1992 the first version of TAM was presented at the Nijmegen workshop on the formal development of real-time and fault tolerant systems [8]. The semantics of the wide-spectrum refinement language were described using extended weakest preconditions (which were later presented in [9]), and the underlying logic was based upon conservative extensions to first-order predicate logic. This version of TAM had single untimed guards, full recursion, but no refinement calculus (although a refinement relation was presented). The main problems with this language stemmed from the lack of any construct with which to define agents which were released as a result of an event occurring (enabling the user to model sporadic real-time tasks), and the complexity involved with trying to find a refinement law for the recursive agent operator. Also, the guards were untimed, which we believed was unrealistic: it led to the execution constraint that guard evaluation had to be instantaneous2.

In 1992 a version of the TAM language, along with a full refinement calculus, was presented [6]. This version of TAM used the same underlying logic and weakest precondition style of the previous version, but it contained a number of important differences. The guards were given an evaluation period, recursion was replaced with bounded iteration, the deadline and sequence operators were coalesced into a single operator, and a timeout operator was added (which modelled the release of an agent in response to an event). This version of the language also appeared in the Fourth Euromicro Workshop on Real-Time Systems along with a small case study [7]. At this stage, although the language

1This work is supported by SERC grant GR/H39611
2We discuss this issue in some detail with respect to refinement hueristics.