Henri B. Weinberg. Correctness of Vehicle Control Systems: A Case Study. Master of Science Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, February 1996. .pdf Also, Technical Report MIT/LCS/TR-685, Laboratory for Computer Science, Massachusetts Institute of Technology.

Abstract

A hybrid system is one in which digital components and analog components interact. Typical examples of hybrid systems are real-time process-control systems such as automated factories or automated transportation systems, in which the digital components monitor and control continuous physical processes in the analog components. The computer science community has developed formal models and methods for reasoning about digital systems, while the control theory community has done the same for analog systems. However, systems that combine both types of activity appear to require new methods. The development and application of such methods is an active area of current research.

One of the formal tools that has been developed is the hybrid I/O automaton (HIOA) model LynchSVW95-dimacs. In this case study, we show how this model can be used to specify and verify part of an automated transportation system --- a vehicle deceleration maneuver. We investigate how techniques such as automata composition, invariant assertions, and simulation mappings can be applied to systems of communicating digital and analog components. The purpose of the case study is to test the applicability of these computer science based techniques to the area of automated transit. In particular, we are concerned that HIOA techniques express hybrid systems faithfully and that they allow clear and scalable proofs of significant properties of these systems.

In the deceleration maneuver, digital controller slows a train to a target velocity range within a given distance. We examine four versions of the deceleration maneuver, each with a different model of the communication between controller and train: plain, delay, feedback, and feedback with delay. For each case we give a model of the non-controller portion of the system, define correctness of a controller, give an example of a correct controller, and prove that it is correct. This case study contains full proofs of the correctness of the various controllers. However, some of the proofs are only sketched, when similar formal proofs appear in other chapters.