Journal of Logic and Computation, Volume 8, Issue 5, pp. 679-711: Abstract.
Logical specification of reactive and real-time systems
Department of Computing, Imperial College, London, UK. E-mail: firstname.lastname@example.org
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.