School of Computing

A Real-time Action Logic of Objects

K. Lano, J. Bicarregui, and S. Kent

In Proceedings of ECOOP'96 Workshop on Proof Theory of Concurrent Object-oriented Programming, pages 182-196. Linz, Austria, July 1996.

Abstract

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++.

Download publication 142 kbytes (PostScript)

Bibtex Record

@inproceedings{797,
author = {K. Lano and J. Bicarregui and S. Kent},
title = {{A Real-time Action Logic of Objects}},
month = {July},
year = {1996},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1996/797},
    booktitle = {Proceedings of ECOOP'96 Workshop on Proof Theory of Concurrent Object-oriented Programming},
    publisher = {Linz, Austria},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014