A Timed Specification Language for Concurrent Reactive Systems

In this paper we present a simple real-time specification language SL^time, for which we define a semantics based on timing diagrams. An example of a specification will illustrate the meaning of the single parts of SL^time. The aim of our approach is to develop and prove correct programs in an occam dialect PL^time which contains timing operators and concurrency with synchronous communication. This happens by stepwise refinement or transformation as originally advocated by Dijkstra and Wirth. We shall give the example of two rules for correct transformations. They will be applied to the example of a railway crossing