Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

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

doi:10.1007/978-3-319-63387-9_23

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

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

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

24 Citations (Scopus)

77 Downloads (Pure)

Abstract

We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.

Original language	English
Title of host publication	Computer Aided Verification
Subtitle of host publication	29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I
Editors	Rupak Majumdar, Viktor Kunčak
Publisher	Springer, Cham
Pages	462-482
ISBN (Electronic)	9783319633879
ISBN (Print)	9783319633862
DOIs	https://doi.org/10.1007/978-3-319-63387-9_23
Publication status	Published - 13 Jul 2017
Event	32nd IEEE/ACM International Conference on Automated Software Engineering - University of Illinois at Urbana-Champaign, Illinois, USA, Urbana-Champaign, Illinois, United States Duration: 30 Oct 2017 → 3 Nov 2017 Conference number: 32 http://ase-conferences.org/ase/past/ase2017/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer, Cham
Number	10426

Conference

Conference	32nd IEEE/ACM International Conference on Automated Software Engineering
Abbreviated title	ASE 2017
Country/Territory	United States
City	Urbana-Champaign, Illinois
Period	30/10/17 → 3/11/17
Internet address	http://ase-conferences.org/ase/past/ase2017/

Research Groups and Themes

Programming Languages

Access to Document

10.1007/978-3-319-63387-9_23

Full-text PDF (author’s accepted manuscript)
This is the author accepted manuscript (AAM). The final published version (version of record) is available online via Springer at https://doi.org/10.1007/978-3-319-63387-9_23 . Please refer to any applicable terms of use of the publisher.
Accepted author manuscript, 426 KB

Handle.net

Persistent link

Dr Cristina David
- cristina.davidbristol.acuk
- School of Computer Science - Senior Lecturer
Person: Academic

Cite this

Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D., & Polgreen, E. (2017). Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. In R. Majumdar, & V. Kunčak (Eds.), Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I (pp. 462-482). (Lecture Notes in Computer Science ; No. 10426). Springer, Cham. https://doi.org/10.1007/978-3-319-63387-9_23

Abate, Alessandro ; Bessa, Iury ; Cattaruzza, Dario et al. / Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. editor / Rupak Majumdar ; Viktor Kunčak. Springer, Cham, 2017. pp. 462-482 (Lecture Notes in Computer Science ; 10426).

@inproceedings{3a93df5859bf4e469a77e4559b24c1ca,

title = "Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants",

abstract = "We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.",

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

year = "2017",

month = jul,

day = "13",

doi = "10.1007/978-3-319-63387-9\_23",

language = "English",

isbn = "9783319633862",

series = "Lecture Notes in Computer Science ",

publisher = "Springer, Cham",

number = "10426",

pages = "462--482",

editor = "Majumdar, \{Rupak \} and Kun{\v c}ak, \{Viktor \}",

booktitle = "Computer Aided Verification",

address = "Switzerland",

note = "32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017 ; Conference date: 30-10-2017 Through 03-11-2017",

url = "http://ase-conferences.org/ase/past/ase2017/",

}

Abate, A, Bessa, I, Cattaruzza, D, Cordeiro, L, David, C, Kesseli, P, Kroening, D & Polgreen, E 2017, Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. in R Majumdar & V Kunčak (eds), Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Computer Science , no. 10426, Springer, Cham, pp. 462-482, 32nd IEEE/ACM International Conference on Automated Software Engineering, Urbana-Champaign, Illinois, United States, 30/10/17. https://doi.org/10.1007/978-3-319-63387-9_23

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. / Abate, Alessandro ; Bessa, Iury ; Cattaruzza, Dario et al.
Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. ed. / Rupak Majumdar; Viktor Kunčak. Springer, Cham, 2017. p. 462-482 (Lecture Notes in Computer Science ; No. 10426).

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

TY - GEN

T1 - Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

AU - Abate, Alessandro

AU - Bessa, Iury

AU - Cattaruzza, Dario

AU - Cordeiro, Lucas

AU - David, Cristina

AU - Kesseli, Pascal

AU - Kroening, Daniel

AU - Polgreen, Elizabeth

N1 - Conference code: 32

PY - 2017/7/13

Y1 - 2017/7/13

N2 - We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.

AB - We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.

U2 - 10.1007/978-3-319-63387-9_23

DO - 10.1007/978-3-319-63387-9_23

M3 - Conference Contribution (Conference Proceeding)

SN - 9783319633862

T3 - Lecture Notes in Computer Science

SP - 462

EP - 482

BT - Computer Aided Verification

A2 - Majumdar, Rupak

A2 - Kunčak, Viktor

PB - Springer, Cham

T2 - 32nd IEEE/ACM International Conference on Automated Software Engineering

Y2 - 30 October 2017 through 3 November 2017

ER -

Abate A, Bessa I, Cattaruzza D, Cordeiro L, David C, Kesseli P et al. Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. In Majumdar R, Kunčak V, editors, Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Springer, Cham. 2017. p. 462-482. (Lecture Notes in Computer Science ; 10426). doi: 10.1007/978-3-319-63387-9_23

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

Abstract

Publication series

Conference

Research Groups and Themes

Access to Document

Handle.net

Fingerprint

Profiles

Dr Cristina David

Cite this