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.
| Original language | English |
|---|---|
| Pages (from-to) | 802-815 |
| Number of pages | 14 |
| Journal | Ruan Jian Xue Bao/Journal of Software |
| Volume | 12 |
| Issue number | 6 |
| State | Published - 2001 |
| Externally published | Yes |
Keywords
- Denotational semantics
- Duration calculus
- RAISE specification language
- Real-time system