Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 8, Issue 5, pp. 679-711: Abstract.

Logical specification of reactive and real-time systems

K Lano

Department of Computing, Imperial College, London, UK. E-mail: kcl@doc.ic.ac.uk

This paper provides a uniform specification and reasoning framework for reactive and real-time systems, which combines the formalisms of real-time logic (RTL) and linear temporal logic to provide an event-based logical system suitable for analysing properties of liveness, fairness, safety and responsiveness. It will be shown that this logic is sound with respect to a natural semantics, and that interval logic and linear temporal logic formalisms can be embedded within the framework. We give an application of the logic to the formalisation of the VDM++ language.

Key words: Real-time temporal logic, formal specification, object-oriented specification, reactive systems.

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 1998.