Linking DC together with TRSL

In this talk we present a method for linking the Duration Calculus together with the Timed RAISE Specification Language. Duration Calculus (DC) [ZHR91] is an interval-based real time logic, which can be used naturally in capturing and eliciting users' real time requirements in the form of constraints on the durations of states of the system, i.e. at a high level of abstraction.However, as a state-based logic, it lacks the ability to specifysequential programs and communicating concurrent processes at a concrete level. The Timed RAISE Specification Language (TRSL) [XG99] has this ability.TRSL is a real-time extension of the RAISE Specification Language (RSL) [Rlg92] which together with its associated method [Rmg95]and tools has shown to be very useful in the industrial development of software systems. Therefore, a promising approach for the development of real-time systemscould be to use DC for high-level specifications of real-time requirementsand TRSL for specifying real-time implementations in the form of timed communicating concurrent processes.In order to link DC and TRSL together in a well-founded way, we formally define what it means for a TRSL process to satisfy a DC requirement. Furthermore, we provide a method for verifying whether the satisfaction relation holds or not. The method is illustrated on an example.Our approach for linking DC and TRSL together has been to extend the configurations in the operational semantics of TRSLwith behaviours, which are DC formulas describing (parts of) the history of the observables of the system,and then define a satisfaction relation in terms of behaviours. DC has previously been linked together with subsets of other event-based process algebra languages, but using another approach:the event-based languages were given a denotational semantics in terms of DC formulas. However, for larger languages like TRSL our approach is easier. One of the reasons for thisis that the behaviors only record the necessary observations.This also implies that the resulting DC formulas are much shorter,and hence it becomes easier to verify that a satisfaction relation holds.