A Real-time Action Logic of

It aims to extend the Object Calculus of Fiadeiro and Maibaum 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 modal action logic (MAL) and real-time logic (RTL) for reasoning about concurrent object-oriented programs 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++. 1 Introduction A variety of semantics for object-orientation have been developed, from the perspectives of logic [5], set theory [18], type theory [2], category theory [6, 17] and process algebra [8]