A Real-time Action Logic of Objects

This paper presents work performed in the EPSRC ''Object-oriented Specification of Reactive and Real-time Systems'' project. It aims to extend the Object Calculus of Fiadeira and Mailbaum to cover durative actions and real-time constraints. We define a core logic, termed ''Real-time action logic'' (RAL) which can provide an axiomatic semantics and reasoning framework for concurrent, real-time and object-oriented specification languages. The logic could also be viewed as providing the basis of a specification language in its own right. We show how a model action logic (MAL) and real-time logic (RTL) for reasoning about concurrent object-oriented pograms and specifications can be derived from RAL, and indicate how this formalism can be used to provide an axiomatic semantics for a large part of the object-oriented specification language VDM++.