HybridFluctuat: A static analyzer of numerical programs within a continuous environment

Olivier Bouissou; Eric Goubault; Sylvie Putot; Karim Tekkal; Franck Vedrine

doi:10.1007/978-3-642-02658-4_46

HybridFluctuat: A static analyzer of numerical programs within a continuous environment

Olivier Bouissou
, Eric Goubault
, Sylvie Putot
, Karim Tekkal
, Franck Vedrine

LIST-DTSI-SLA CEA
FCS Digiteo

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

A new static analyzer is described, based on the analyzer Fluctuat. Its goal is to synthetize invariants for hybrid systems, encompassing a continuous environment described by a system of possibly switched ODEs, and an ANSI C program, in interaction with it. The evolution of the continuous environment is over-approximated using a guaranteed integrator that we developped, and special assertions are added to the program that simulate the action of sensors and actuators, making the continuous environment and the program communicate. We demonstrate our approach on an industrial case study, a part of the flight control software of ASTRIUM's Automated Transfer Vehicle (ATV).

langue originale	Anglais
titre	Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings
Editeur	Springer Verlag
Pages	620-626
Nombre de pages	7
ISBN (imprimé)	3642026575, 9783642026577
Les DOIs	https://doi.org/10.1007/978-3-642-02658-4_46
état	Publié - 1 janv. 2009
Modification externe	Oui
Evénement	21st International Conference on Computer Aided Verification, CAV 2009 - Grenoble, France Durée: 26 juin 2009 → 2 juil. 2009

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5643 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	21st International Conference on Computer Aided Verification, CAV 2009
Pays/Territoire	France
La ville	Grenoble
période	26/06/09 → 2/07/09

Accès au document

10.1007/978-3-642-02658-4_46

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

Bouissou, O., Goubault, E., Putot, S., Tekkal, K., & Vedrine, F. (2009). HybridFluctuat: A static analyzer of numerical programs within a continuous environment. Dans Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings (p. 620-626). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 5643 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-02658-4_46

Bouissou, Olivier ; Goubault, Eric ; Putot, Sylvie et al. / HybridFluctuat : A static analyzer of numerical programs within a continuous environment. Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. Springer Verlag, 2009. p. 620-626 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{756d5162fa0041858fbe9fdfcb856e3c,

title = "HybridFluctuat: A static analyzer of numerical programs within a continuous environment",

abstract = "A new static analyzer is described, based on the analyzer Fluctuat. Its goal is to synthetize invariants for hybrid systems, encompassing a continuous environment described by a system of possibly switched ODEs, and an ANSI C program, in interaction with it. The evolution of the continuous environment is over-approximated using a guaranteed integrator that we developped, and special assertions are added to the program that simulate the action of sensors and actuators, making the continuous environment and the program communicate. We demonstrate our approach on an industrial case study, a part of the flight control software of ASTRIUM's Automated Transfer Vehicle (ATV).",

author = "Olivier Bouissou and Eric Goubault and Sylvie Putot and Karim Tekkal and Franck Vedrine",

year = "2009",

month = jan,

day = "1",

doi = "10.1007/978-3-642-02658-4\_46",

language = "English",

isbn = "3642026575",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "620--626",

booktitle = "Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings",

note = "21st International Conference on Computer Aided Verification, CAV 2009 ; Conference date: 26-06-2009 Through 02-07-2009",

}

Bouissou, O, Goubault, E , Putot, S, Tekkal, K & Vedrine, F 2009, HybridFluctuat: A static analyzer of numerical programs within a continuous environment. Dans Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 5643 LNCS, Springer Verlag, p. 620-626, 21st International Conference on Computer Aided Verification, CAV 2009, Grenoble, France, 26/06/09. https://doi.org/10.1007/978-3-642-02658-4_46

HybridFluctuat: A static analyzer of numerical programs within a continuous environment. / Bouissou, Olivier; Goubault, Eric ; Putot, Sylvie et al.
Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. Springer Verlag, 2009. p. 620-626 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 5643 LNCS).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - HybridFluctuat

T2 - 21st International Conference on Computer Aided Verification, CAV 2009

AU - Bouissou, Olivier

AU - Goubault, Eric

AU - Putot, Sylvie

AU - Tekkal, Karim

AU - Vedrine, Franck

PY - 2009/1/1

Y1 - 2009/1/1

N2 - A new static analyzer is described, based on the analyzer Fluctuat. Its goal is to synthetize invariants for hybrid systems, encompassing a continuous environment described by a system of possibly switched ODEs, and an ANSI C program, in interaction with it. The evolution of the continuous environment is over-approximated using a guaranteed integrator that we developped, and special assertions are added to the program that simulate the action of sensors and actuators, making the continuous environment and the program communicate. We demonstrate our approach on an industrial case study, a part of the flight control software of ASTRIUM's Automated Transfer Vehicle (ATV).

AB - A new static analyzer is described, based on the analyzer Fluctuat. Its goal is to synthetize invariants for hybrid systems, encompassing a continuous environment described by a system of possibly switched ODEs, and an ANSI C program, in interaction with it. The evolution of the continuous environment is over-approximated using a guaranteed integrator that we developped, and special assertions are added to the program that simulate the action of sensors and actuators, making the continuous environment and the program communicate. We demonstrate our approach on an industrial case study, a part of the flight control software of ASTRIUM's Automated Transfer Vehicle (ATV).

UR - https://www.scopus.com/pages/publications/70350235068

U2 - 10.1007/978-3-642-02658-4_46

DO - 10.1007/978-3-642-02658-4_46

M3 - Conference contribution

AN - SCOPUS:70350235068

SN - 3642026575

SN - 9783642026577

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 620

EP - 626

BT - Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings

PB - Springer Verlag

Y2 - 26 June 2009 through 2 July 2009

ER -

Bouissou O, Goubault E , Putot S, Tekkal K, Vedrine F. HybridFluctuat: A static analyzer of numerical programs within a continuous environment. Dans Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. Springer Verlag. 2009. p. 620-626. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-02658-4_46

HybridFluctuat: A static analyzer of numerical programs within a continuous environment

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation