|
|
|---|
|
|
|
|---|
R. S. Boyer, M. W. Green, and J S. Moore, “The
Use of a Formal Simulator to Verify a Simple Real Time Control
Program”, in W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and
J. Misra, editors, Beauty is Our Business: A Birthday Salute to Edsger
W. Dijkstra, Springer-Verlag Texts and Monographs in Computer Science,
pp. 54-66, 1990.
Relevance: operational semantics modeling a hybrid
physical/digital system
Abstract
We present an initial and elementary investigation of the formal specification and mechanical verification of programs that interact with environments. We describe a formal, mechanically produced proof that a simple real time control program keeps a vehicle on a straightline course in a variable crosswind. To formalize the specification we define a mathematical function which models the interaction of the program and its environment. We then state and prove two theorems about this function: the simulated vehicle never gets farther than three units away from the intended course and homes to the course if the wind remains steady for at least four sampling intervals.
It is easiest to think of the problem as a one-dimensional control problem, e.g., a thermostat or speed control. But the problem was posed as follows. Consider the task of steering a vehicle along the x-axis with a crosswind along the y-axis. The wind speed varies. The vehicle carries a sensor that indicates whether the vehicle is above, on, or below the x-axis. The vehicle also has actuators that can adjust the sideways velocity of vehicle by a fixed amount. Write, specify, and verify a control program that never allows the vehicle to drift too far from the x-axis and homes to the x-axis when the wind stays steady sufficiently long.
This can be modeled as a “clocked” state machine, except the clock is a sequence of changes in wind velocity. The “physics” is modeled extremely simply because the prover only supported natural numbers; but anybody who has ever written a simulator of a physical system will recognize it. The proof involved defining and verifying an invariant on the state, under the assumption that the wind changed sufficiently smoothly.
The work was done at SRI, probably between 1979 and 1980. It was submitted for publication at that time but rejected because its formal approach to real-time control was too unconventional. The reviewers overlooked the fact that this approach accommodated a hybrid system, where the control program was digital but the “simulator” was describing the physical world. It was eventually published about a decade after the work was done, when the authors were invited to submit a paper to a volume in honor of Edsger Dijkstra.
See the Nqthm script