Verification of advanced controllers for safety-critical systems

In order to design and deploy a feedback controller in a real application, one must determine suitable specifications that the design must meet ("validate"), and then ensure that the chosen specifications have been met ("verify"). In this thesis, we investigate a verification paradigm based on formal methods, such as the Satisfiability Modulo Theories (SMT) and quantifier elimination (Weispfenning’s virtual term substitution and quantifier elimination by cylindrical algebraic decomposition) algorithms. Any control design requirement (such as satisfactory performance, robustness to uncertainties, stability, etc.) that can be expressed in a first order logic formula can be (in principle) verified by using one of these methods. Consequently, in principle, this allows us to consider problems like general non-convex optimisation, exact computation of structured singular value, and synthesis of non-convex feasible parameter sets. In practice, the generality of algorithms like quantifier elimination by cylindrical algebraic decomposition come with a downside of high running time when applied to more complex systems with more parameters. This, in some cases, limits the complexity of the system that we could consider. Therefore, we focused our attention on control problems such as obtaining an explicit MPC law for a linear time invariant system with a quadratic objective and polytopic constraints, or computation of the structured singular value for a system under parametric (and not norm-bounded) uncertainty. Such problems can be expressed as quantifier elimination problems with a particular quantification structure that allows us to take advantage of a specialised quantifier elimination algorithm - the quantifier elimination by Weispfenning’s virtual term substitution procedure that has much lower worst-case running time on these types of problems than quantifier elimination by cylindrical algebraic decomposition algorithm. Despite these constraints, we were able to apply a quantifier-elimination-based verification framework to clearance of a flight control law developed for a real world industrial system from the aerospace field not only at particular combination of parameters but throughout the whole flight envelope. In conclusion, while in principle formal methods are applicable to a large body of problems arising in control theory, more widespread practical application depends on further research in efficiency and running time improvement in the implementation of these algorithms.

Name dc:type.qualificationname

Doctor of Philosophy (PhD)

Level dc:type.qualificationlevel

Doctoral

Grantor dc:publisher.institution

University of Cambridge

Year dc:date.issued

2019

Author dc:creator

• Siaulys, Kestutis

Advisor dc:contributor.advisor

• Maciejowski, Jan

• Model Predictive Control (MPC)
• Formal Methods
• Quantifier Elimination
• Cylindrical Algebraic Decomposition
• Weispfenning’s virtual term substitution
• Satisfiability Modulo Theories (SMT)
• Robust Flight Control
• Why3
• MetiTarski
• Exclusion Regions
• Structured Singular Value
• Explicit Model Predictive Control
• Linear Temporal Logic
• RECONFIGURE
• Simulink

Licence

• https://www.repository.cam.ac.uk/bitstreams/7ebaff0c-53f4-495f-b06d-e018b704826f/download
• https://www.rioxx.net/licenses/all-rights-reserved/

Language dc:language

en

DOI dc:identifier.doi

https://doi.org/10.17863/CAM.45913

OAI identifier oai:identifier

oai:www.repository.cam.ac.uk:1810/298858