Towards a denotational semantics of timed RSL using duration calculus

• DOI: 10.1007/bf02948854
• Publication Date: 2008-09-13T00:20:43Z
• Authors: Li Li
• Keywords: 0202 electrical engineering, electronic engineering, information engineering; 02 engineering and technology

The Timed RAISE Specification Language (Timed RSL) is an extension 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 duration properties of Boolean states in a dynamic system. This paper gives a denotational semantics to a subset of Timed RSL expressions, using Duration Calculus extended with super-dense chop modality and notations to capture time point properties of piecewise continuous states of arbitrary types. Using this semantics, the paper presents a proof rule for verifying Timed RSL iterative expressions and implements the rule to prove the satisfaction by a sample Timed RSL specification of its real-time requirements.