A refinement-based approach to developing software controllers for reactive systems
Victor Winter, Deepak Kapur, R.S. Berg · University of North Texas Digital Library (University of North Texas) · 1999
The purpose of this paper is to demonstrate how transformation can be used to derive a high integrity implementation of a train controller from an algorithmic specification. The paper begins with a general discussion of high consequence systems (e.g., software systems) and describes how rewrite-based transformation systems can be used in the development of such systems. The authors then discuss how such transformations can be used to derive a high assurance controller for the Bay Area Rapid Transit (BART) system from an algorithmic specification.