Affordable Access

A RAISE Specification Framework and Justification assistant for the Duration Calculus

Publication Date
Online Research Database In Technology
External links


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.


Seen <100 times