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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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).

Original language	English
Title of host publication	Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings
Pages	620-626
Number of pages	7
DOIs	https://doi.org/10.1007/978-3-642-02658-4_46
Publication status	Published - 27 Oct 2009
Externally published	Yes
Event	21st International Conference on Computer Aided Verification, CAV 2009 - Grenoble, France Duration: 26 Jun 2009 → 2 Jul 2009

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5643 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Conference on Computer Aided Verification, CAV 2009
Country/Territory	France
City	Grenoble
Period	26/06/09 → 2/07/09

Access to Document

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

Cite this

Bouissou, O., Goubault, E., Putot, S., Tekkal, K., & Vedrine, F. (2009). HybridFluctuat: A static analyzer of numerical programs within a continuous environment. In Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings (pp. 620-626). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5643 LNCS). 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. 2009. pp. 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 = oct,

day = "27",

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)",

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. in 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, pp. 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. 2009. p. 620-626 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5643 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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/10/27

Y1 - 2009/10/27

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).

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

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. In Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. 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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this