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.
|Title of host publication||Proceedings of 10th ESSLLI|
|Place of Publication||Sarbrücken|
|Publication status||Published - 1998|
|Event||ESSLLI-98 Workshop on Duration Calculus: A Logical Approach to Real-Time Systems - Saarbrücken|
Duration: 1 Jan 1998 → …
|Conference||ESSLLI-98 Workshop on Duration Calculus: A Logical Approach to Real-Time Systems|
|Period||01/01/1998 → …|