© 1998 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Logical Specification of Reactive and Real-time Systems
Department of Computing, Imperial College London, UK. E-mail: kcl{at}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.
Keywords: Real-time temporal logic; formal specification; object-oriented specification; eactive systems