Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System

• Interactive theorem proving is the verification of assertions with the assistance of an automatic theorem prover.
• Formal verification is an important tool in the development of control systems.
• In this paper, the PVS (Prototype Verification System) is used to prove properties of the level control of a storage tank.

Interactive, or computer-assisted, theorem proving is the verification of statements in a formal system, where the proof is developed by a logician who chooses the appropriate inference steps, in turn executed by an automatic theorem prover. In this paper, interactive theorem proving is used to verify safety properties of a nonlinear (hybrid) control system.