Formal verification of computer controlled systems

This dissertation discusses the application of formal verification methods to reasoning about the correctness of computer controlled systems. Due to the switching that is introduced by the computer controller, the differential equations associated with such systems may consist of discontinuous vector fields. The physical system may also experience switching due to physical interaction, such as impact. Such system models may exhibit an infinite number of switches in finite time. For example, using rigid body modeling assumptions, a bouncing ball may have infinitely many elastic impacts, but come to rest in finite time. Using nonstandard analysis, we present a model for computer controlled systems which accommodates discontinuous vector fields as well as infinite switches in finite time. This model includes both the semantics of the computer program as well as the ordinary differential equations governing the physical system behavior. We develop a nonstandard definition of a solution for such a model and formally prove that the solution exists. Using this nonstandard definition of solution, we develop proof procedures whereby one may reason about safety and progress properties of the system. The soundness of these proof procedures is formally shown. We conclude with the presentation of a simple example computer controlled system using the presented model, for which safety and progress properties are shown using the respective proof procedures.