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 |