A RAISE Specification Framework and Justification assistant for the Duration Calculus

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

    Abstract

    RAISE is a product consisting of a development method, an associated formal specification language (RSL) and a collection of computer-based tools. RAISE has turned out to be useful in the development of many kinds of software systems.However, RSL has no ``real-time'' features, and hence, it is difficult to specify real-time applications using RSL. The Duration Calculus (DC) is aformalism which can be used for that. However, DC is ``just'' a logic,and for practical purposes it would be nice to have a richer language providing modules, facilities for declaring symbols to beused in DC formulas etc. The goal of our work is two-fold:(1) to extend RSL with real-time features, and (2) to provide a specification language and tools support (e.g. a syntax and type checker, a justification assistant, etc.) for DC. A first step towards this goal, could be to combine DC and RSL achieving the power of both.So far, we have encoded DC in RSL and set up a proof assistant tool to verify (encoded) DC formulas using the RAISE Justification tools. This paper first introduces a RAISE specification framework for DC, and then explains how the justification assistant is set up.
    Original languageEnglish
    Title of host publicationProceedings of 10th ESSLLI
    Place of PublicationSarbrücken
    Publication date1998
    Publication statusPublished - 1998
    EventESSLLI-98 Workshop on Duration Calculus: A Logical Approach to Real-Time Systems - Saarbrücken
    Duration: 1 Jan 1998 → …

    Conference

    ConferenceESSLLI-98 Workshop on Duration Calculus: A Logical Approach to Real-Time Systems
    CitySaarbrücken
    Period01/01/1998 → …

    Fingerprint Dive into the research topics of 'A RAISE Specification Framework and Justification assistant for the Duration Calculus'. Together they form a unique fingerprint.

    Cite this