Theorem-proving analysis of digital control logic interacting with continuous dynamics

DOI10.1016/J.ENTCS.2015.10.008MaRDI QIDQ2520681zbMATH OpenOpenAlexWikidataFDO

Authors Geoffrey C. Hulette, Robert C. Armstrong, Jackson R. Mayo, Joseph R. Ruthruff

Publication date 16 December 2016

Full work available at URL https://doi.org/10.1016/j.entcs.2015.10.008

zbMATH Keywords

cyber-physical systemsformal methodshybrid systemstheorem proving

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Thermodynamics and heat transfer (80A99) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Recommendations

• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• Proving the Correctness of the Implementation of a Control-Command Algorithm
• Logical approach to control theory and applications
• Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
• Automated formal synthesis of provably safe digital controllers for continuous plants

Cites work

• Buridan's principle
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)

Cited in

(2)

• Proving the Correctness of the Implementation of a Control-Command Algorithm
• scientific article; zbMATH DE number 1956625 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq
• KeYmaera

This page was built for publication: Theorem-proving analysis of digital control logic interacting with continuous dynamics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2520681)