Linking DC together with TRSL

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    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 languageEnglish
    Title of host publicationIFM'2000 2nd Int. Conf. on Integrated Formal Methods, no. 1945
    PublisherSpringer Verlag
    Publication date2000
    Pages25-44
    Publication statusPublished - 2000
    EventIFM'2000 2nd Int. Conf. on Integrated Formal Methods -
    Duration: 1 Jan 2000 → …

    Conference

    ConferenceIFM'2000 2nd Int. Conf. on Integrated Formal Methods
    Period01/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.