The control systems we envision are large, complex assemblages of software and hardware components. The reality of software development as it is practiced today (and as it is likely to be practiced for the indefinite future) is that any system of significant complexity consists partly of components that are written for the task at hand (e.g., in our case the implementations of the critical control algorithms) and partly or even primarily of pre-existing components that are completely reused or modestly adapted from an existing software base (e.g., the operating system, standard numerical libraries, implementations of networking protocols, etc.). We expect the research directions discussed in Sections 2.2.3, 2.2.2 to yield new, robust techniques for the design and verification of core control components. However, when one wishes to reason about properties of the complete system it is necessary to reason about all system components. Such reasoning is required if we are to integrate subsystems with any confidence that a complete system performs as expected.
Because of the presence of pre-existing or legacy components, the task
of supporting system integration presents a unique set of challenges, since
1. Legacy components rarely have formal specifications.
2. A complete system is at least of the order of
100's of thousands of lines of code.
3. A complete system is rarely written in a single programming language,
which complicates the task of reasoning about component interfaces.
4. To guarantee correctness of the complete system it may be
necessary to check that a legacy component satisfies a certain
semantic property. That is, we may wish to give a partial
specification of behavior after the component has been developed
without this specification in mind, and in addition we will need to
verify that the property holds, possibly modifying the legacy
component if the property does not hold.
In light of these obstacles it is clearly impossible at the present time to perform full verification of complete systems. Fortunately, however, it appears that many important failures at the system level stem not from deep algorithmic flaws of individual components, but rather more mundane problems that stem from the inability of humans to grasp the overwhelming number of details involved in correctly interfacing complex components which were written originally for some other purpose. Examples of such problems may be the failure of a component to handle an unanticipated exception raised by a subcomponent, errors due to unforeseen byte-order problems in communication among a heterogenous collection of machines, and unintentional race conditions on state shared among components.
We believe that it is possible to automatically and systematically check for
such limited classes of errors in even the largest software systems. We plan
to develop tools using BANE (the Berkeley ANalysis Engine,
http://bane.cs.berkeley.edu/ ) to automatically detect such problems in the
control systems we study. BANE is an open architecture for rapidly
developing ad hoc software analyses tuned for a given
price/performance, where price is measured in computation time of the
analysis and performance is measured in the precision of the information
produced. BANE has been used for a number of different applications in
different programming languages and analyses written using BANE have been
demonstrated to be both scalable to large systems and useful in detecting
programming errors.