On the Construction of a Domain Language for a Class of Reactive Systems

A key step in the construction of high consequence software is its specification in a formal framework. In order to minimize the difficulty and potential for error, a specification should be expressed in a domain language supporting operators and structures that are intrinsic to the class of algorithms one wishes to specify.In this paper we describe a language that is suitable for the algorithmic specification of software controllers for a class of reactive systems of which the Bay Area Rapid Transit (BART) system is an instance. We then specify an abstract controller for a subset of BART using this language.