SpaceEx: Scalable verification of hybrid systems

Goran Frehse; Colas Le Guernic; Alexandre Donzé; Scott Cotton; Rajarshi Ray; Olivier Lebeltel; Rodolfo Ripado; Antoine Girard; Thao Dang; Oded Maler

doi:10.1007/978-3-642-22110-1_30

SpaceEx: Scalable verification of hybrid systems

Goran Frehse
, Colas Le Guernic
, Alexandre Donzé
, Scott Cotton
, Rajarshi Ray
, Olivier Lebeltel
, Rodolfo Ripado
, Antoine Girard
, Thao Dang
, Oded Maler

Verimag
New York University
LTHE (UMR 5564 CNRS/IRD/Université de Grenoble)

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é

We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an over-approximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.

langue originale	Anglais
titre	Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings
Editeur	Springer Verlag
Pages	379-395
Nombre de pages	17
ISBN (imprimé)	9783642221095
Les DOIs	https://doi.org/10.1007/978-3-642-22110-1_30
état	Publié - 1 janv. 2011
Modification externe	Oui

Série de publications

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

Accès au document

10.1007/978-3-642-22110-1_30

Contient cette citation

Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., & Maler, O. (2011). SpaceEx: Scalable verification of hybrid systems. Dans Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings (p. 379-395). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 6806 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-22110-1_30

@inproceedings{020f7ad126e44c3da6b2e94638102c63,

title = "SpaceEx: Scalable verification of hybrid systems",

abstract = "We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an over-approximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.",

author = "Goran Frehse and \{Le Guernic\}, Colas and Alexandre Donz{\'e} and Scott Cotton and Rajarshi Ray and Olivier Lebeltel and Rodolfo Ripado and Antoine Girard and Thao Dang and Oded Maler",

year = "2011",

month = jan,

day = "1",

doi = "10.1007/978-3-642-22110-1\_30",

language = "English",

isbn = "9783642221095",

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

publisher = "Springer Verlag",

pages = "379--395",

booktitle = "Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings",

}

Frehse, G, Le Guernic, C, Donzé, A, Cotton, S, Ray, R, Lebeltel, O, Ripado, R, Girard, A, Dang, T & Maler, O 2011, SpaceEx: Scalable verification of hybrid systems. Dans Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 6806 LNCS, Springer Verlag, p. 379-395. https://doi.org/10.1007/978-3-642-22110-1_30

SpaceEx: Scalable verification of hybrid systems. / Frehse, Goran; Le Guernic, Colas; Donzé, Alexandre et al.
Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Springer Verlag, 2011. p. 379-395 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 6806 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 - SpaceEx

T2 - Scalable verification of hybrid systems

AU - Frehse, Goran

AU - Le Guernic, Colas

AU - Donzé, Alexandre

AU - Cotton, Scott

AU - Ray, Rajarshi

AU - Lebeltel, Olivier

AU - Ripado, Rodolfo

AU - Girard, Antoine

AU - Dang, Thao

AU - Maler, Oded

PY - 2011/1/1

Y1 - 2011/1/1

N2 - We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an over-approximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.

AB - We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an over-approximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.

U2 - 10.1007/978-3-642-22110-1_30

DO - 10.1007/978-3-642-22110-1_30

M3 - Conference contribution

AN - SCOPUS:79960348872

SN - 9783642221095

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

SP - 379

EP - 395

BT - Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings

PB - Springer Verlag

ER -

Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O et al. SpaceEx: Scalable verification of hybrid systems. Dans Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Springer Verlag. 2011. p. 379-395. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-22110-1_30

SpaceEx: Scalable verification of hybrid systems

Résumé

Série de publications

Accès au document

Empreinte digitale

Contient cette citation