%0 Journal Article
%T Towards a denotational semantics of timed RSL using duration calculus<br>Towards a Denotational Semantics of Timed RSL Using Duration Calculus
%A Li Li
%A <br>李黎
%J 计算机科学技术学报
%D 2001
%I 
%X 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 dura- tion 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.
%K duration calculus
%K RAISE specification language
%K denotational
%K semantics
%K real-time system<br>软件开发
%K 持续时间算法
%K RAISE语言
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=F57FEF5FAEE544283F43708D560ABF1B&aid=30533C69E971A1AEF351DB786152C957&yid=14E7EF987E4155E6&vid=7801E6FC5AE9020C&iid=CA4FD0336C81A37A&sid=2B25C5E62F83A049&eid=2B25C5E62F83A049&journal_id=1000-9000&journal_name=计算机科学技术学报&referenced_num=1&reference_num=8