Transformational design of real-time systems. II: From program specifications to programs (Q1127814)

In the two parts of this article we present a transformational approach to the design of real-time systems. The overall starting point are requirements formulated in a subset of Duration Calculus called \textit{implementables} and the target are programs in an \textbf{occam} dialect PL. In the first part we have shown how the level of program specifications represented by a language SL can be reached. SL combines regular expressions with action systems and time conditions. In the second part we show the transformation from SL to PL. It relies On the `Expansion strategy' by which certain transformations can be applied in an almost automatic fashion. In many places transformations consist of algebraic reasoning by laws for operations on programs. Both parts of our transformational calculus rely on the mixed term techniques in which syntax pieces of two languages are mixed in a semantically coherent manner. In the first part of the article mixed terms between implementables and SL have been used, in the present part mixed terms between SL and PL are used. The approach is illustrated by the example of a computer controlled gas burner from part I again.