A Logic Theory Pattern for Linearized Control Systems

TL;DR

This paper presents a method to translate linearized control system models into logic theories for formal verification, integrating theorem proving into control system development.

Contribution

It introduces a systematic procedure for converting control system equations into logic theories suitable for computer-assisted verification.

Findings

The method successfully verified a control theory case study.

It facilitates formal requirement verification for control systems.

The approach integrates with existing model-driven development processes.

Abstract

This paper describes a procedure that system developers can follow to translate typical mathematical representations of linearized control systems into logic theories. These theories are then used to verify system requirements and find constraints on design parameters, with the support of computer-assisted theorem proving. This method contributes to the integration of formal verification methods into the standard model-driven development processes for control systems. The theories obtained through its application comprise a set of assumptions that the system equations must satisfy, and a translation of the equations into the logic language of the Prototype Verification System theorem-proving environment. The method is illustrated with a standard case study from control theory.