Exercises: Developing and Proving Algorithms with PVS (Part II)

Consider the theories UTM0, UTM, and the lecture Developing and Proving Algorithms with PVS (Part II).

1. Write a strategy called uss-tcc and use it to discharge the proofs of subscribe_j, test_0, test_1, Dos, and test_update. Hint: The strategy does the following: first apply grind, then to each generated subgoal, expand exists_op as many times as needed.
2. Define the function in_operational_volume?(uss:USS)(p:Vect3) : bool that returns TRUE if the point p is inside the operational volume of uss. Hint: Check that:
   • The vertical component of p, i.e., p`z, is below uss`op_alt.
   • The horizontal component of p, i.e., vect2(p), is inside uss`op_area.
   • Look for the names of the functions in NASALib/shapes that check if a point is inside a circle, rectangle, and triangle.
3. Define the function check_flight_plan(uss:USS,ac_op:AircraftOp) that returns:
   • OK, if every waypoint in the flight plan of ac_op lies inside the USS operational volume, or
   • Failure(wps) otherwise, where wps is the list of waypoints in its flight plan that lie outside the USS operational volume.
4. Modify the function subscribe in UTM.pvs so that only aircraft operations ac_op that satisfy check_flight_plan(uss,ac_op) = OK are subscribed. Throw an exception if check_flight_plan(uss) returns a Failure.