White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Formal Design and Verification of Digital PID Gain Scheduling Controllers

Ordóñez Aguileta, Pablo Armando (2018) Formal Design and Verification of Digital PID Gain Scheduling Controllers. PhD thesis, University of Sheffield.

Text (A model checking approach to gain scheduling control design and verification)
PAOA Thesis - Formal Design and Verification of Digital PID Gain Scheduling Controllers.pdf
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (4Mb) | Preview


The verification process of embedded systems is fundamental for their correct development. Embedded control is a popular choice among the engineering community, making the relationship between control systems and computer science very close. Gain scheduling is a typical approach for safety-critical systems (e.g. jet-engines). It is preferred due to a known route to certification. Nonetheless, stability and performance are hard to prove analytically. Consequently, safety and airworthiness are achieved by extensive testing, and therefore a new way for verification is desirable. Model checking, an exhaustive verification technique, is a part of formal methods. Model checking can aid in detecting ambiguities and collisions in requirements, increasing and improving testing coverage and error detection rate. However, there are still limitations and challenges to model checking. The state-space explosion problem limits its use to realistic dynamic control systems: Computational memory runs out or available data types are not appropriate for modelling. This thesis addresses the formal design and verification of discrete PID gain-scheduled control systems. By the means of a novel abstraction methodology the control problem is resolved in a model checking environment; formally tuning the controller whilst systematically constructing a control schedule. The work in this overcomes typical constraints imposed by model checking. In this manner, the gain-scheduled controller can be efficiently generated and the resulting schedule is correct-by-construction with respect to high level performance requirements. This novel methodology incorporates computer science and control systems tools, proposing an a priori verification approach in contrast to current a posteriori testing activities. By combining computer science and control engineering, the gap between formal methods and control systems is reduced. The next step in this line of research is to analyse the scalability of the approach using more realistic models and design cases; in this manner the state-space explosion problem can be addressed with a divide and conquer approach. Also, a trade-off analysis between benefits and the required effort learning the new approach in a real development cycle must be conducted to assess feasibility and capabilities of the approach.

Item Type: Thesis (PhD)
Keywords: Formal Methods, Model Checking, Gain Scheduling, Safety Critical Software
Academic Units: The University of Sheffield > Faculty of Engineering (Sheffield) > Automatic Control and Systems Engineering (Sheffield)
Identification Number/EthosID: uk.bl.ethos.736572
Depositing User: Mr Pablo Armando Ordóñez Aguileta
Date Deposited: 14 Mar 2018 12:23
Last Modified: 12 Oct 2018 09:52
URI: http://etheses.whiterose.ac.uk/id/eprint/19465

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)