Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | IFM'2000 2nd Int. Conf. on Integrated Formal Methods, no. 1945 |
| Publisher | Springer Verlag |
| Publication date | 2000 |
| Pages | 25-44 |
| Publication status | Published - 2000 |
| Event | IFM'2000 2nd Int. Conf. on Integrated Formal Methods - Duration: 1 Jan 2000 → … |
Conference
| Conference | IFM'2000 2nd Int. Conf. on Integrated Formal Methods |
|---|---|
| Period | 01/01/2000 → … |
Cite this
Haxthausen, A. E., & Yong, X. (2000). Linking DC together with TRSL. In IFM'2000 2nd Int. Conf. on Integrated Formal Methods, no. 1945 (pp. 25-44). Springer Verlag.