DSSynth: An automated digital controller synthesis tool for physical plants

Alessandro  Abate; Lury Bessa; Dario Cattaruzza; Lennon Chaves; Lucas  Cordeiro; Cristina David; Pascal Kesseli; Daniel  Kroening; Elizabeth  Polgreen

doi:10.1109/ASE.2017.8115705

DSSynth: An automated digital controller synthesis tool for physical plants

Alessandro Abate, Lury Bessa, Dario Cattaruzza, Lennon Chaves, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

5 Citations (Scopus)

133 Downloads (Pure)

Abstract

We present an automated MATLAB Toolbox, named DSSynth (Digital-System Synthesizer), to synthesize sound digital controllers for physical plants that are represented as linear timeinvariant systems with single input and output. In particular, DSSynth synthesizes digital controllers that are sound w.r.t. stability and safety specifications. DSSynth considers the complete range of approximations, including time discretization, quantization effects and finite-precision arithmetic (and its rounding errors). We demonstrate the practical value of this toolbox by automatically synthesizing stable and safe controllers for intricate physical plant models from the digital control literature. The resulting toolbox enables the application of program synthesis to real-world control engineering problems. A demonstration can be found at https://youtu.be_hLQslRcee8.

Original language	English
Title of host publication	ASE 2017
Subtitle of host publication	Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering
Publisher	Association for Computing Machinery (ACM)
Pages	919–924
Number of pages	6
ISBN (Electronic)	978-1-5386-2684-9
DOIs	https://doi.org/10.1109/ASE.2017.8115705
Publication status	Published - 23 Nov 2017

Keywords

Formal Synthesis
Digital Control Systems
MATLAB Toolbox
Finite-Word Length
Veriﬁcation

Access to Document

10.1109/ASE.2017.8115705

Full-text PDF (accepted author manuscript)
This is the author accepted manuscript (AAM). The final published version (version of record) is available online via IEEE at https://ieeexplore.ieee.org/document/8115705/authors#authors. Please refer to any applicable terms of use of the publisher.
Accepted author manuscript, 793 KB

Handle.net

Persistent link

Cite this

Abate, A., Bessa, L., Cattaruzza, D., Chaves, L., Cordeiro, L., David, C., Kesseli, P., Kroening, D., & Polgreen, E. (2017). DSSynth: An automated digital controller synthesis tool for physical plants. In ASE 2017: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering (pp. 919–924). Association for Computing Machinery (ACM). https://doi.org/10.1109/ASE.2017.8115705

@inproceedings{e46416bd33df46d292a0728cb8065779,

title = "DSSynth: An automated digital controller synthesis tool for physical plants",

abstract = "We present an automated MATLAB Toolbox, named DSSynth (Digital-System Synthesizer), to synthesize sound digital controllers for physical plants that are represented as linear timeinvariant systems with single input and output. In particular, DSSynth synthesizes digital controllers that are sound w.r.t. stability and safety specifications. DSSynth considers the complete range of approximations, including time discretization, quantization effects and finite-precision arithmetic (and its rounding errors). We demonstrate the practical value of this toolbox by automatically synthesizing stable and safe controllers for intricate physical plant models from the digital control literature. The resulting toolbox enables the application of program synthesis to real-world control engineering problems. A demonstration can be found at https://youtu.be_hLQslRcee8.",

keywords = "Formal Synthesis, Digital Control Systems, MATLAB Toolbox, Finite-Word Length, Veriﬁcation",

author = "Alessandro Abate and Lury Bessa and Dario Cattaruzza and Lennon Chaves and Lucas Cordeiro and Cristina David and Pascal Kesseli and Daniel Kroening and Elizabeth Polgreen",

year = "2017",

month = nov,

day = "23",

doi = "10.1109/ASE.2017.8115705",

language = "English",

pages = "919–924",

booktitle = "ASE 2017",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

}

Abate, A, Bessa, L, Cattaruzza, D, Chaves, L, Cordeiro, L, David, C, Kesseli, P, Kroening, D & Polgreen, E 2017, DSSynth: An automated digital controller synthesis tool for physical plants. in ASE 2017: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering. Association for Computing Machinery (ACM), pp. 919–924. https://doi.org/10.1109/ASE.2017.8115705

DSSynth: An automated digital controller synthesis tool for physical plants. / Abate, Alessandro ; Bessa, Lury; Cattaruzza, Dario et al.
ASE 2017: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering. Association for Computing Machinery (ACM), 2017. p. 919–924.

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

TY - GEN

T1 - DSSynth

T2 - An automated digital controller synthesis tool for physical plants

AU - Abate, Alessandro

AU - Bessa, Lury

AU - Cattaruzza, Dario

AU - Chaves, Lennon

AU - Cordeiro, Lucas

AU - David, Cristina

AU - Kesseli, Pascal

AU - Kroening, Daniel

AU - Polgreen, Elizabeth

PY - 2017/11/23

Y1 - 2017/11/23

N2 - We present an automated MATLAB Toolbox, named DSSynth (Digital-System Synthesizer), to synthesize sound digital controllers for physical plants that are represented as linear timeinvariant systems with single input and output. In particular, DSSynth synthesizes digital controllers that are sound w.r.t. stability and safety specifications. DSSynth considers the complete range of approximations, including time discretization, quantization effects and finite-precision arithmetic (and its rounding errors). We demonstrate the practical value of this toolbox by automatically synthesizing stable and safe controllers for intricate physical plant models from the digital control literature. The resulting toolbox enables the application of program synthesis to real-world control engineering problems. A demonstration can be found at https://youtu.be_hLQslRcee8.

AB - We present an automated MATLAB Toolbox, named DSSynth (Digital-System Synthesizer), to synthesize sound digital controllers for physical plants that are represented as linear timeinvariant systems with single input and output. In particular, DSSynth synthesizes digital controllers that are sound w.r.t. stability and safety specifications. DSSynth considers the complete range of approximations, including time discretization, quantization effects and finite-precision arithmetic (and its rounding errors). We demonstrate the practical value of this toolbox by automatically synthesizing stable and safe controllers for intricate physical plant models from the digital control literature. The resulting toolbox enables the application of program synthesis to real-world control engineering problems. A demonstration can be found at https://youtu.be_hLQslRcee8.

KW - Formal Synthesis

KW - Digital Control Systems

KW - MATLAB Toolbox

KW - Finite-Word Length

KW - Veriﬁcation

U2 - 10.1109/ASE.2017.8115705

DO - 10.1109/ASE.2017.8115705

M3 - Conference Contribution (Conference Proceeding)

SP - 919

EP - 924

BT - ASE 2017

PB - Association for Computing Machinery (ACM)

ER -

DSSynth: An automated digital controller synthesis tool for physical plants

Abstract

Keywords

Access to Document

Handle.net

Fingerprint

Cite this