A Denotational Semantics of Timed RSL Using Duration Calculus
使用延时演算的时间化RSL的指称语义

This paper provides a denotational semantics to a subset of Timed RAISE Specification Language (RSL) using Extended Duration Calculus (EDC) model. It adds some novel features into the EDC model and explore their algebraic laws which play the vital role in formalising real time programs and verification of real time properties. Some algebraic laws of Timed RSL are presented, which can be proved from the denotational semantics, and be used in program transformation and optimization.