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 the authors 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. The authors then specify an abstract controller for a subset of BART using this language.