A Formal Proof in Coq of a Control Function for the Inverted Pendulum - Archive ouverte HAL Access content directly
Conference Papers Year :

A Formal Proof in Coq of a Control Function for the Inverted Pendulum

(1)
1
Damien Rouhling

Abstract

Control theory provides techniques to design controllers, or control functions, for dynamical systems with inputs, so as to grant a particular behaviour of such a system. The inverted pendulum is a classic system in control theory: it is used as a benchmark for nonlinear control techniques and is a model for several other systems with various applications. We formalized in the Coq proof assistant the proof of soundness of a control function for the inverted pendulum. This is a first step towards the formal verification of more complex systems for which safety may be critical.
Fichier principal
Vignette du fichier
poplws18cppmain-id41-p-ef0777f-34741-final.pdf (897.3 Ko) Télécharger le fichier
Origin : Explicit agreement for this submission
Loading...

Dates and versions

hal-01639819 , version 1 (26-11-2017)
hal-01639819 , version 2 (22-01-2018)

Identifiers

Cite

Damien Rouhling. A Formal Proof in Coq of a Control Function for the Inverted Pendulum. CPP 2018 - 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.1-14, ⟨10.1145/3167101⟩. ⟨hal-01639819v2⟩
263 View
874 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More