Formal Design and Verification of Digital PID Gain Scheduling Controllers

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.