Towards a Denotational Semantics of Timed RSL Using Duration Calculus

The Timed RAISE Specification Language (Timed RSL) is an extension of RAISESpecification Language by adding time constructors for specifyingreal-time applications. Duration Calculus (DC) is a real-time interval logicwhich can be used to specify and reason about timing and logicalconstraints on duration properties of Boolean states in a dynamicsystem. This paper gives a denotational semantics to a subset of TimedRSL expressions, using Duration Calculus extended with super-dense chopmodality and notations to capture time point properties of piecewisecontinuous states of arbitrary types. Using this semantics, thepaper presents a proof rule for verifying Timed RSL iterative expressions andimplements the rule to prove the satisfaction by a sample Timed RSLspecification of its real-time requirements.