| 摘要: |
| 使用扩展的持续时间演算(EDC)模型,给出了时间化的RAISE描述语言(RSL)的一个子集的指称语义.在扩展的持续时间演算模型中加入了一些新的特征,并探究了它们的代数定律.这些定律在形式化实时程序和验证实时性质中起着重要作用.最后还给出了时间化RSL的一些代数定律.这些定律可以从其指称语义证明,并用于程序的转化和优化. |
| 关键词: 延时演算 RAISE描述语言 指称语义 实时系统 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant No.69773025 (国家自然科学基金) |
|
| A Denotational Semantics of Timed RSL Using Duration Calculus |
|
LI Li,HE Ji-feng
|
| Abstract: |
| 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. |
| Key words: duration calculus RAISE specification language denotational semantics real time system |
