Duration Calculus (DC) is an interval-based real-time logic, which can be used in capturing and eliciting users’ real-time
requirements. The Timed RAISE Specification Language (TRSL) is an extension of the RAISE Specification Language with real-time
features. This paper links DC and TRSL together in a method for real-time developments. An operational semantics with behavior is specified for TRSL. It is defined what its means for a TRSL process to satisfy a DC requirement, and a method for verifying whether the satisfaction relation holds or not is provided. Our contribution
also demonstrates a general approach for linking state-based real-time logics together with event-based, timed process algebra
languages.
Keywords Formal methods - RAISE - Duration Calculus - integration of specification formalisms