Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
427036 | Information Processing Letters | 2016 | 7 Pages |
Abstract
•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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Cinzia Bernardeschi, Andrea Domenici,