Time interval semantics and implementation of a real-time programming language

The authors present a real-time programming language, including concurrency, which could be used in the formal development of embedded systems. The semantics of the language is provided in the form of a time interval semantics and also a number of algebraic refinement laws. The laws allow convenient reasoning and transformation of programs. In particular, a compiler for a sequential subset of the language is defined as a set of theorems relating high-level program constructs to a low-level machine specified as an interpreter in the high-level language. In addition, a prototype compiler may be produced very directly from Ihe lheorems in Ihe form of a logic program.