Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems

Date: Thursday, December 09, 2010
Speaker: Enrico Tronci
Venue: IST Austria

A control system consists of two subsystems: the controllerand the “plant” (controlled system).In an endless loop the controller measures outputs from and sends commands to theplant in order to drive it towards a given goal region.We focus on software based control systems,that is, systems where the the controllerconsists of software running on a microprocessorand measures from the plant are quantized (AD conversion)before being sent to the control software.

System requirements for control systemsare typically given as specifications for the closed loop system,that is the system consisting ofthe plant and the (to be designed) controller.

Typically, Control engineering techniques are usedto design the control law(i.e. the functional specifications for the control software)from the closed loop system requirements.Software engineering techniques are then used todesign the control software implementing the given controllaw.

Such an approach leaves open many questions about the correctnessof the control software with respect to the closed loop system requirementsand motivates investigation on methods and tools for automatic synthesis ofcorrect-by-construction control software from closed loopsystem requirements.

We present an algorithm that given a Discrete Time Linear Hybrid System(DTLHS) model for the plant P returns acorrect-by-construction software implementation Kfor a (near time optimal)robust Quantized Feedback Controllerfor P along witha suitable representation forthe set of states on which Kis guaranteed to work correctly (controllable region).Furthermore, K has a Worst Case Execution Time(WCET)guaranteed to belinear in the number of bits of the quantization schema.

We implemented our algorithm on top of the CUDD OBDD packageand of the GLPK MILP solver and present results on using such an implementation to synthesize Ccontrollers for the buck DC-DC converter,a widely used mixed-mode analog circuit.Our experimental results show that our proposed approach is viable andthe performance of the automatically synthesized controllers compare wellwith those of controllers designed using ad-hoc approaches.

************

This talk is mainly based on our CAV2010 paper:
Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci.
Synthesis of Quantized Feedback Control Software forDiscrete Time Linear Hybrid Systems.
Tayssir Touili, Byron Cook, Paul Jackson (Eds.):
Computer Aided Verification, 22nd International Conference,CAV 2010, Edinburgh, UK,
July 15-19, 2010. Proceedings. Lecture Notes in ComputerScience 6174 Springer 2010,
ISBN 978-3-642-14294-9 CiteSeerX

Posted in RiSE Seminar