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 | Second International Conference on Integrated Formal Methods - Dagstuhl Castle, Wadern, Germany Duration: 1 Nov 2000 → 3 Nov 2000 |
Conference
| Conference | Second International Conference on Integrated Formal Methods |
|---|---|
| Location | Dagstuhl Castle |
| Country/Territory | Germany |
| City | Wadern |
| Period | 01/11/2000 → 03/11/2000 |