Towards a Denotational Semantics of Timed RSL Using Duration Calculus

摘要

The Timed RAISE Specification Language (Timed RSL) is an ex- tension of RAISE Specification Language by adding time constructors for specifying real-time applications. Duration Calculus (DC) is a real-time interval logic, which can be used to specify and reason about timing and logical constraints on dura- tion properties of Boolean states in a dynamic system. This paper gives a deno- tational semantics to a subset of Timed RSL expressions, using Duration Calculus extended with super-dense chop modality and notations to capture time point pro- perties of piecewise continuous states of arbitrary types. Using this semantics, the paper presents a proof rule for verifying Timed RSL iterative expressions and imple- ments the rule to prove the satisfaction by a sample Timed RSL specification of its real-time requirements.