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

Damien Rouhling 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
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.
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01639819
Contributeur : Damien Rouhling <>
Soumis le : dimanche 26 novembre 2017 - 18:30:49
Dernière modification le : jeudi 11 janvier 2018 - 16:56:56

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01639819, version 1

Collections

Citation

Damien Rouhling. A Formal Proof in Coq of a Control Function for the Inverted Pendulum. 2017. 〈hal-01639819〉

Partager

Métriques

Consultations de la notice

56

Téléchargements de fichiers

129