Logical specification of reactive and real-time systems

Publisher Website
Google Scholar
Abstract
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.

This publication has 0 references indexed in Scilit: