An operational semantics for timed RAISE

Abstract

The reliability of software is an increasingly important demand, especially for safety critical systems. RAISE is a mathematically based method which has been shown to be useful in the development of many kinds of software systems. However, RAISE has no particular features for specifying real-time requirements, which often occur in safety critical systems. Adding timing features to RAISE makes a new specification language, Timed RAISE Specification Language (TRSL), and gives it the power of specifying real-time applications. We then have to find a theoretical foundation for TRSL. In this paper, an operational semantics of TRSL is first introduced. Then we define a pre-order and test equivalence relation for TRSL. Some proof rules for TRSL are listed, and their soundness corresponding to our operational model is also explained.