Formal verification of control software

Formal methods;LMI;Lyapunov;Static analysis;Control software;Theorem proving

Jobredeaux, Romain J. ; Feron, Eric M. Aerospace Engineering Garoche, Pierre Loic Goodloe, Alwyn Holzinger, Marcus Johnson, Eric ; Feron, Eric M.

University:Georgia Institute of Technology

Department:Aerospace Engineering

关键词: Formal methods;    LMI;    Lyapunov;    Static analysis;    Control software;    Theorem proving;   

Others  :  https://smartech.gatech.edu/bitstream/1853/53841/1/JOBREDEAUX-DISSERTATION-2015.pdf

美国|英语

来源: SMARTech Repository

【 摘 要 】

In a context of heightened requirements for safety-critical embedded systems andever-increasing costs of verification and validation, this research proposes toadvance the state of formal analysis for control software. Formal methods are afield of computer science that uses mathematical techniques and formalisms torigorously analyze the behavior of programs. This research develops a frameworkand tools to express and prove high level properties of control lawimplementations. One goal is to bridge the gap between control theory andcomputer science. An annotation language is extended with symbols and axioms todescribe control-related concepts at the code level. Libraries of theorems,along with their proofs, are developed to enable an interactive proof assistantto verify control-related properties. Through integration in a prototype tool,the process of verification is made automatic, and applied to several example systems.In a context of heightened requirements for safety-critical embedded systems andever-increasing costs of verification and validation, this research proposes toadvance the state of formal analysis for control software. Formal methods are afield of computer science that uses mathematical techniques and formalisms torigorously analyze the behavior of programs. This research develops a frameworkand tools to express and prove high level properties of control lawimplementations. One goal is to bridge the gap between control theory andcomputer science. An annotation language is extended with symbols and axioms todescribe control-related concepts at the code level. Libraries of theorems,along with their proofs, are developed to enable an interactive proof assistantto verify control-related properties. Through integration in a prototype tool,the process of verification is made automatic, and applied to several example systems.