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.
|Title of host publication||IFM'2000 2nd Int. Conf. on Integrated Formal Methods, no. 1945|
|Publication status||Published - 2000|
|Event||IFM'2000 2nd Int. Conf. on Integrated Formal Methods - |
Duration: 1 Jan 2000 → …
|Conference||IFM'2000 2nd Int. Conf. on Integrated Formal Methods|
|Period||01/01/2000 → …|