poster

CODEV: Automated Model Predictive Control Design and Formal Verification

Authors:

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 281 - 282

https://doi.org/10.1145/3178126.3187003

Published: 11 April 2018 Publication History

Get Access

Abstract

No abstract available.

References

[1]

Alessandro Abate, Iury Bessa, Dario Cattaruzza, et al. 2017. Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. In CAV.

Google Scholar

[2]

Alessandro Alessio and Alberto Bemporad. 2009. A Survey on Explicit Model Predictive Control.

Google Scholar

[3]

A. Bemporad. 2015. A Multiparametric Quadratic Programming Algorithm With Polyhedral Computations Based on Nonnegative Least Squares. IEEE Trans. Automat. Control (2015).

Google Scholar

[4]

A. Bemporad, F. Borrelli, and M. Morari. 2000. The explicit solution of constrained LP-based receding horizon control. In IEEE Conf. on Decision and Control.

Google Scholar

[5]

F. Borrelli, A. Bemporad, and M. Morari. 2017. Predictive Control for Linear and Hybrid Systems.

Digital Library

Google Scholar

[6]

E.F. Camacho and C.A. Bordons. 2012. Model Predictive Control in the Process Industry.

Google Scholar

[7]

Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In CAV.

Google Scholar

[8]

Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, and Matthew Potok. 2015. C2E2: A Verification Tool for Stateflow Models. In TACAS.

Google Scholar

[9]

Chuchu Fan and Sayan Mitra. 2015. Bounded Verification with On-the-Fly Discrepancy Computation. In Automated Technology for Verification and Analysis.

Google Scholar

[10]

Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, and Parasara Sridhar Duggirala. 2016. Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2. In CAV.

Google Scholar

[11]

Ansgar Fehnker and Franjo Ivančić. 2004. Benchmarks for Hybrid Systems Verification. In HSCC.

Google Scholar

[12]

Goran Frehse, Colas Le Guernic, Alexandre Donzé, et al. 2011. SpaceEx: Scalable Verification of Hybrid Systems. In CAV.

Digital Library

Google Scholar

[13]

Sicun Gao, Soonho Kong, and Edmund M Clarke. {n. d.}. dReal: An SMT solver for nonlinear theories over the reals. In Automated Deduction-CADE-24.

Digital Library

Google Scholar

[14]

M. Herceg, M. Kvasnica, C.N. Jones, and M. Morari. 2013. Multi-Parametric Toolbox 3.0. In European Control Conf.

Google Scholar

CODEV: Automated Model Predictive Control Design and Formal Verification
1. Computing methodologies
  1. Artificial intelligence
    1. Control methods

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...

Comments

Information & Contributors

Information

Published In

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

April 2018

296 pages

ISBN:9781450356428

DOI:10.1145/3178126

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Check for updates

Qualifiers

Poster
Research
Refereed limited

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

0
Total Citations
120
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)0

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

View Options

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

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

Formal verification of ASMs using MDGs

Transition predicate abstraction and fair termination

Comments

Information

Published In

Sponsors

Publisher

Publication History

Check for updates

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations