A Logic Theory Pattern for Linearized Control Systems

Andrea Domenici
(U. of Pisa)
Cinzia Bernardeschi
(U. of Pisa)

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.

In José Proença and Andrei Paskevich: Proceedings of the 6th Workshop on Formal Integrated Development Environment (F-IDE 2021), Held online, 24-25th May 2021, Electronic Proceedings in Theoretical Computer Science 338, pp. 46–52.
Published: 6th August 2021.

ArXived at: http://dx.doi.org/10.4204/EPTCS.338.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org