More Web Proxy on the site http://driver.im/

research-article

Open access

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Authors:

Alessandro Abate,

Dario Cattaruzza,

Lucas Cordeiro,

Cristina David,

Pascal Kesseli,

Daniel KroeningAuthors Info & Claims

HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control

Pages 197 - 206

https://doi.org/10.1145/3049797.3049802

Published: 13 April 2017 Publication History

Abstract

Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counterexample guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and its rounding errors. We have implemented our new algorithm in a tool called DSSynth, and are able to automatically generate stable controllers for a set of intricate plant models taken from the literature within minutes.

Supplementary Material

ZIP File (hscc014.zip)

Directory structure * benchmark-runner: experiment scripts * benchmarks: benchmark set * cbmc: CBMC/CEGIS source directory "compile-and-run-experiment.sh" compiles CBMC/CEGIS, runs the full benchmark set with the two-stage engine and displays the results in CSV format on the console output. To execute it, type the following comands: chmod +x compile-and-run-experiment.sh./compile-and-run-experiment.sh

Download
26.15 MB

References

[1]

R. Alur, D. Fisman, R. Singh, and A. Solar-Lezama. SyGuS-Comp 2016: Results and analysis. In Workshop on Synthesis, volume 229 of EPTCS, 2016.

[2]

R. Alur, S. Moarref, and U. Topcu. Compositional synthesis with parametric reactive controllers. In HSCC. ACM, 2016.

Digital Library

[3]

A. Anta, R. Majumdar, I. Saha, and P. Tabuada. Automatic verification of control system implementations. In Embedded Software (EMSOFT), pages 9--18, 2010.

Digital Library

[4]

K. Åström and B. Wittenmark. Computer-controlled systems: theory and design. 1997.

[5]

K. J. Astrom and R. M. Murray. Feedback Systems: An Introduction for Scientists and Engineers. 2008.

[6]

A. Bemporad, M. Morari, V. Dua, and E. N. Pistikopoulos. The explicit linear quadratic regulator for constrained systems. Automatica, 38(1), 2002.

Digital Library

[7]

I. Bessa, H. Ismail, L. Cordeiro, and J. Filho. Verification of fixed-point digital controllers using direct and delta forms realizations. Design Autom. for Emb. Sys., 20(2), 2016.

[8]

I. Bessa, H. Ismail, R. Palhares, L. Cordeiro, and J. E. C. Filho. Formal non-fragile stability verification of digital control systems with uncertainty. IEEE Transactions on Computers, 66(3):545--552, 2017.

Digital Library

[9]

E. M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS, volume 2988, 2004.

[10]

S. Das, I. Pan, K. Halder, S. Das, and A. Gupta. LQR based improved discrete PID controller design via optimum selection of weighting matrices using fractional order integral performance index. Applied Mathematical Modelling, 37(6), 2013.

[11]

C. David, D. Kroening, and M. Lewis. Using program synthesis for program analysis. In LPAR, LNCS, 2015.

Digital Library

[12]

J. C. Doyle, B. A. Francis, and A. R. Tannenbaum. Feedback Control Theory. 1991.

[13]

P. S. Duggirala and M. Viswanathan. Analyzing real time linear control systems using software verification. In IEEE Real-Time Systems Symposium, Dec 2015.

Digital Library

[14]

C. Economakos, G. Economakos, M. Skarpetis, and M. Tzamtzi. Automated synthesis of an FPGA-based controller for vehicle lateral control. In MATEC Web of Conferences, volume 41, 2016.

[15]

S. Fadali and A. Visioli. Digital Control Engineering: Analysis and Design, volume 303 of Electronics & Electrical. 2009.

[16]

I. J. Fialho and T. T. Georgiou. On stability and performance of sampled-data systems subject to wordlength constraint. IEEE Trans. on Automatic Control, 39(12), 1994.

[17]

G. Franklin, D. Powell, and A. Emami-Naeini. Feedback Control of Dynamic Systems. 7th edition, 2015.

[18]

S. Ghosh, R. K. Barai, S. Bhattarcharya, P. Bhattacharyya, S. Rudra, A. Dutta, and R. Pyne. An FPGA based implementation of a flexible digital PID controller for a motion control system. In Computer Communication and Informatics (ICCCI). IEEE, 2013.

[19]

H. Ismail, I. Bessa, L. C. Cordeiro, E. B. de Lima Filho, and J. E. C. Filho. DSVerifier: A bounded model checking tool for digital systems. In SPIN, volume 9232, 2015.

Digital Library

[20]

R. Istepanian and J. F. Whidborne. Digital controller implementation and fragility: A modern perspective. 2012.

[21]

S. Itzhaky, S. Gulwani, N. Immerman, and M. Sagiv. A simple inductive synthesis methodology and its applications. In ACM Sigplan Notices, volume 45. ACM, 2010.

Digital Library

[22]

S. Jha and S. A. Seshia. Synthesis of optimal fixed-point implementations of numerical software routines. In Numerical Software Verification (NSV), 2013.

[23]

L. Keel and S. Bhattacharyya. Robust, fragile, or optimal? IEEE Trans. on Automatic Control, 42(8), 1997.

[24]

L. Keel and S. Bhattacharyya. Stability margins and digital implementation of controllers. In Proc. American Control Conference, volume 5, 1998.

[25]

G. Klein and B. Moore. Eigenvalue-generalized eigenvector assignment with state feedback. IEEE Trans. on Automatic Control, 22(1), 1977.

[26]

U. Konigorski. Pole placement by parametric output feedback. Systems & Control Letters, 61(2), 2012.

[27]

Y. Li, K. Ang, G. Chong, W. Feng, K. Tan, and H. Kashiwagi. CAutoCSD--evolutionary search and optimisation enabled computer automated control system design. Int J Automat Comput, 1(1), 2004.

[28]

R. E. Moore. Interval analysis, volume 4. 1966.

[29]

A. K. Oudjida, N. Chaillet, A. Liacha, M. L. Berrandjia, and M. Hamerlain. Design of high-speed and low-power finite-word-length PID controllers. Control Theory and Technology, 12(1), 2014.

[30]

J. Park, M. Pajic, I. Lee, and O. Sokolsky. Scalable verification of linear controller software. In TACAS. Springer, 2016.

Digital Library

[31]

H. Ravanbakhsh and S. Sankaranarayanan. Counter-example guided synthesis of control Lyapunov functions for switched systems. In Conference on Decision and Control, CDC, 2015.

[32]

P. Roux, R. Jobredeaux, and P. Garoche. Closed loop analysis of control command software. In HSCC, 2015.

Digital Library

[33]

R. Schmid, L. Ntogramatzidis, T. Nguyen, and A. Pandey. A unified method for optimal arbitrary pole placement. Automatica, 50(8), 2014.

[34]

A. Solar-Lezama, L. Tancau, R. Bodık, S. A. Seshia, and V. A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, pages 404--415. ACM, 2006.

Digital Library

[35]

K. Tan and Y. Li. Performance-based control system design automation via evolutionary computing. Engineering Applications of Artificial Intelligence, 14(4), 2001.

[36]

T. E. Wang, P. Garoche, P. Roux, R. Jobredeaux, and E. Feron. Formal analysis of robustness at model and code level. In HSCC, 2016.

Digital Library

[37]

W. Wonham. On pole assignment in multi-input controllable linear systems. IEEE Trans. on Automatic Control, 12(6), 1967.

[38]

J. Wu, G. Li, S. Chen, and J. Chu. Robust finite word length controller design. Automatica, 45(12), 2009.

Digital Library

Cited By

Matos Jde Lima Filho EBessa IManino ESong XCordeiro L(2024)Counterexample Guided Neural Network Quantization RefinementIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.333531343:4(1121-1134)Online publication date: Apr-2024
https://doi.org/10.1109/TCAD.2023.3335313
Matos JBessa IManino ESong XCordeiro L(2022)CEG4N: Counter-Example Guided Neural Network Quantization RefinementSoftware Verification and Formal Methods for ML-Enabled Autonomous Systems10.1007/978-3-031-21222-2_3(29-45)Online publication date: 16-Dec-2022
https://doi.org/10.1007/978-3-031-21222-2_3
Banerjee SSamynathan BAbraham JChatterjee A(2021)Real-Time Error Detection in Nonlinear Control Systems Using Machine Learning Assisted State-Space EncodingIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2019.290304918:2(576-592)Online publication date: 1-Mar-2021
https://doi.org/10.1109/TDSC.2019.2903049
Show More Cited By

Index Terms

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Recommendations

DSSynth: an automated digital controller synthesis tool for physical plants
ASE '17: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering

We present an automated MATLAB Toolbox, named DSSynth (Digital-System Synthesizer), to synthesize sound digital controllers for physical plants that are represented as linear time-invariant systems with single input and output. In particular, DSSynth ...
PI-Fuzzy controllers for integral plants to ensure robust stability

New PI-fuzzy controllers comprising Takagi-Sugeno and Mamdani fuzzy systems to control a class of integral plants specific to servo systems are proposed in this paper. Linear PI controllers are designed in the first phase. They are tuned using the ...
Stabilizing Sets of PI/PID Controllers for Unstable Second Order Delay System

In this paper, the problem of stabilizing an unstable second order delay system using classical proportional-integral-derivative (PID) controller is considered. An extension of the Hermite-Biehler theorem, which is applicable to quasi-polynomials, is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control

April 2017

288 pages

ISBN:9781450345903

DOI:10.1145/3049797

Program Chairs:
Goran Frehse
University Grenoble Alpes
,
Sayan Mitra
University of Illinois at Urbana Champaign

Copyright © 2017 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 April 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

HSCC '17

Sponsor:

SIGBED

HSCC '17: 20th International Conference on Hybrid Systems: Computation and Control

April 18 - 20, 2017

Pennsylvania, Pittsburgh, USA

Acceptance Rates

HSCC '17 Paper Acceptance Rate 29 of 76 submissions, 38%;

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
553
Total Downloads

Downloads (Last 12 months)97
Downloads (Last 6 weeks)4

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Matos Jde Lima Filho EBessa IManino ESong XCordeiro L(2024)Counterexample Guided Neural Network Quantization RefinementIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.333531343:4(1121-1134)Online publication date: Apr-2024
https://doi.org/10.1109/TCAD.2023.3335313
Matos JBessa IManino ESong XCordeiro L(2022)CEG4N: Counter-Example Guided Neural Network Quantization RefinementSoftware Verification and Formal Methods for ML-Enabled Autonomous Systems10.1007/978-3-031-21222-2_3(29-45)Online publication date: 16-Dec-2022
https://doi.org/10.1007/978-3-031-21222-2_3
Banerjee SSamynathan BAbraham JChatterjee A(2021)Real-Time Error Detection in Nonlinear Control Systems Using Machine Learning Assisted State-Space EncodingIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2019.290304918:2(576-592)Online publication date: 1-Mar-2021
https://doi.org/10.1109/TDSC.2019.2903049
Ravanbakhsh HSankaranarayanan SSeshia S(2019)Formal Policy Learning from Demonstrations for Reachability Properties2019 International Conference on Robotics and Automation (ICRA)10.1109/ICRA.2019.8793828(6037-6043)Online publication date: May-2019
https://doi.org/10.1109/ICRA.2019.8793828
Chaves LIsmail HBessa ICordeiro Lde Lima Filho E(2019)Verifying fragility in digital systems with uncertainties using DSVerifier v2.0Journal of Systems and Software10.1016/j.jss.2019.03.015153:C(22-43)Online publication date: 1-Jul-2019
https://dl.acm.org/doi/10.1016/j.jss.2019.03.015
Abate ABessa ICordeiro LDavid CKesseli PKroening DPolgreen E(2019)Automated formal synthesis of provably safe digital controllers for continuous plantsActa Informatica10.1007/s00236-019-00359-1Online publication date: 6-Dec-2019
https://doi.org/10.1007/s00236-019-00359-1
David CKesseli PKroening DLewis M(2018)Program Synthesis for Program AnalysisACM Transactions on Programming Languages and Systems10.1145/317480240:2(1-45)Online publication date: 28-May-2018
https://dl.acm.org/doi/10.1145/3174802
De Oliveira Junior JGuez Assuncao WCavalcanti Jeronymo D(2018)Multi-objective Tuning of Generalized Predictive Controller: A Trade-Off Between Performance and Robustness2018 VIII Brazilian Symposium on Computing Systems Engineering (SBESC)10.1109/SBESC.2018.00034(178-183)Online publication date: Nov-2018
https://doi.org/10.1109/SBESC.2018.00034
Abate ABessa ICattaruzza DChaves LCordeiro LDavid CKesseli PKroening DPolgreen ERosu GDi Penta MNguyen T(2017)DSSynth: an automated digital controller synthesis tool for physical plantsProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155678(919-924)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155678
Abate ATalpin JDerler PSchneider K(2017)Formal verification of complex systemsProceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3127041.3131362(91-93)Online publication date: 29-Sep-2017
https://dl.acm.org/doi/10.1145/3127041.3131362
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents