research-article

Reachset Conformance Testing of Hybrid Automata

Authors:

Jens Oehlerking,

Matthias Woehrle,

Matthias AlthoffAuthors Info & Claims

HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

Pages 277 - 286

https://doi.org/10.1145/2883817.2883828

Published: 11 April 2016 Publication History

Abstract

Industrial-sized hybrid systems are typically not amenable to formal verification techniques. For this reason, a common approach is to formally verify abstractions of (parts of) the original system. However, we need to show that this abstraction conforms to the actual system implementation including its physical dynamics. In particular, verified properties of the abstract system need to transfer to the implementation. To this end, we introduce a formal conformance relation, called reachset conformance, which guarantees transference of safety properties, while being a weaker relation than the existing trace inclusion conformance. Based on this formal relation, we present a conformance testing method which allows us to tune the trade-off between accuracy and computational load. Additionally, we present a test selection algorithm that uses a coverage measure to reduce the number of test cases for conformance testing. We experimentally show the benefits of our novel techniques based on an example from autonomous driving.

References

[1]

H. Abbas, H. D. Mittelmann, and G. E. Fainekos. Formal property verification in a conformance testing framework. In ACM/IEEE MEMOCODE, pages 155--164, 2014.

Digital Library

[2]

R. W. Allen, H. T. Szostak, D. H. Klyde, T. J. Rosenthal, and K. J. Owens. Vehicle dynamic stability and rollover. Technical report, U.S. Department of Transportation, Final Report DOT HS 807--956, 1992.

[3]

M. Althoff. An introduction to CORA 2015. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems, pages 120--151, 2015.

[4]

M. Althoff and J. M. Dolan. Reachability computation of low-order models for the safety verification of high-order road vehicle models. In American Control Conference, pages 3559--3566. IEEE, 2012.

[5]

M. Althoff, O. Stursberg, and M. Buss. Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes. Nonlinear Analysis: Hybrid Systems, 4(2):233--249, 2010.

[6]

M. S. Branicky, M. M. Curtiss, J. Levine, and S. B. Morgan. RRTs for nonlinear, discrete, and hybrid planning and control. In Decision and Control, volume 1, pages 657--663. IEEE, 2003.

[7]

T. Dang. Model-based testing of hybrid systems. In Model-Based Testing for Embedded Systems, chapter 14, pages 383--424. CRC Press, Inc., 2011.

[8]

P. S. Duggirala, S. Mitra, M. Viswanathan, and M. Potok. C2E2: A verification tool for Stateflow models. In Tools and Algorithms for the Construction and Analysis of Systems, pages 68--82. 2015.

Digital Library

[9]

G. Frehse, C. L. Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. SpaceEx: Scalable verification of hybrid systems. In Computer Aided Verification, pages 379--395, 2011.

[10]

A. Girard. Reachability of uncertain linear systems using zonotopes. In Hybrid Systems: Computation and Control, pages 291--305. 2005.

Digital Library

[11]

A. Girard and C. L. Guernic. Zonotope/hyperplane intersection for hybrid systems reachability analysis. In Hybrid Systems: Computation and Control, pages 215--228. 2008.

Digital Library

[12]

A. Girard, C. L. Guernic, and O. Maler. Efficient computation of reachable sets of linear time-invariant systems with inputs. In Hybrid Systems: Computation and Control, pages 257--271. 2006.

Digital Library

[13]

Á. González. Measurement of areas on a sphere using fibonacci and latitude-longitude lattices. Mathematical Geosciences, 42(1):49--64, 2010.

[14]

L. J. Guibas, A. Nguyen, and L. Zhang. Zonotopes as bounding volumes. In Proc. of the ACM-SIAM Symposium on Discrete Algorithms, pages 803--812, 2003.

Digital Library

[15]

A. Kanade, R. Alur, F. Ivancic, S. Ramesh, S. Sankaranarayanan, and K. C. Shashidhar. Generating and analyzing symbolic traces of Simulink/Stateflow models. In Computer Aided Verification, pages 430--445, 2009.

Digital Library

[16]

N. Khakpour and M. R. Mousavi. Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap. In Int. Conf. on Concurrency Theory, volume 42 of LIPIcs, pages 18--40, 2015.

[17]

C. Le Guernic, A. Girard, C. L. Guernic, and A. Girard. Reachability analysis of hybrid systems using support functions. In Computer Aided Verification, pages 540--554, 2009.

Digital Library

[18]

I. M. Mitchell. Comparing forward and backward reachability as tools for safety analysis. In Hybrid Systems: Computation and Control, pages 428--443. 2007.

[19]

S. Mitra. Proving abstractions of dynamical systems through numerical simulations. In Proc. of the Symposium and Bootcamp on the Science of Security, page 12, 2014.

Digital Library

[20]

J. Schmaltz and J. Tretmans. On conformance testing for timed systems. In Formal Modeling and Analysis of Timed Systems, pages 250--264. 2008.

Digital Library

[21]

P. Tabuada. Verification and Control of Hybrid Systems - A Symbolic Approach. Springer, 2009.

Digital Library

[22]

G. J. Tretmans. A formal approach to conformance testing. PhD thesis, Universiteit Twente, 1992.

[23]

M. P. W. J. van Osch. Automated model-based testing of hybrid systems. PhD thesis, Eindhoven University of Technology, 2009.

Cited By

Kulmburg ABrkan IAlthoff M(2024)Search-based and Stochastic Solutions to the Zonotope and Ellipsotope Containment Problems2024 European Control Conference (ECC)10.23919/ECC64448.2024.10590884(1057-1064)Online publication date: 25-Jun-2024
https://doi.org/10.23919/ECC64448.2024.10590884
Roehm HRausch AAlthoff M(2022)Reachset Conformance and Automatic Model Adaptation for Hybrid SystemsMathematics10.3390/math1019356710:19(3567)Online publication date: 29-Sep-2022
https://doi.org/10.3390/math10193567
Giusti ALiu SAlthoff M(2022)Interval-Arithmetic-Based Robust Control of Fully Actuated Mechanical SystemsIEEE Transactions on Control Systems Technology10.1109/TCST.2021.311848830:4(1525-1537)Online publication date: Jul-2022
https://doi.org/10.1109/TCST.2021.3118488
Show More Cited By

Index Terms

Reachset Conformance Testing of Hybrid Automata

Recommendations

Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics
SCOPES '19: Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems

Disributed control systems often exhibit aperiodic sampling behavior due to varying communication delays and execution times. In such cases traditional analysis methods fall short because the functional and temporal behaviors need to be analyzed ...
Multiple conformance to hybrid automata for checking smart house temperature change
DS-RT '18: Proceedings of the 22nd International Symposium on Distributed Simulation and Real Time Applications

Conformance testing is a formal approach for checking the validity of an implemented system against its specification. This paper adopts it to comprehensively check the conformance of smart house temperature with its requirements. However, besides its ...
Approximated Reachability on Hybrid Automata: Falsification meets Certification

Undecidability of the reachability problem is ubiquitous in the context of hybrid automata. Being mostly based on either bounded reachability or on the notion of simulation preorder, current techniques for the approximated reachability analysis force to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

April 2016

324 pages

ISBN:9781450339551

DOI:10.1145/2883817

Program Chairs:
Alessandro Abate
University of Oxford, UK
,
Georgios Fainekos
Arizona State University, USA

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

European Commission

Conference

HSCC'16

Sponsor:

SIGBED

HSCC'16: 19th International Conference on Hybrid Systems: Computation and Control

April 12 - 14, 2016

Vienna, Austria

Acceptance Rates

HSCC '16 Paper Acceptance Rate 28 of 65 submissions, 43%;

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
295
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)6

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kulmburg ABrkan IAlthoff M(2024)Search-based and Stochastic Solutions to the Zonotope and Ellipsotope Containment Problems2024 European Control Conference (ECC)10.23919/ECC64448.2024.10590884(1057-1064)Online publication date: 25-Jun-2024
https://doi.org/10.23919/ECC64448.2024.10590884
Roehm HRausch AAlthoff M(2022)Reachset Conformance and Automatic Model Adaptation for Hybrid SystemsMathematics10.3390/math1019356710:19(3567)Online publication date: 29-Sep-2022
https://doi.org/10.3390/math10193567
Giusti ALiu SAlthoff M(2022)Interval-Arithmetic-Based Robust Control of Fully Actuated Mechanical SystemsIEEE Transactions on Control Systems Technology10.1109/TCST.2021.311848830:4(1525-1537)Online publication date: Jul-2022
https://doi.org/10.1109/TCST.2021.3118488
Kochdumper NBak S(2022)Conformant Synthesis for Koopman Operator Linearized Control Systems2022 IEEE 61st Conference on Decision and Control (CDC)10.1109/CDC51059.2022.9992324(7327-7332)Online publication date: 6-Dec-2022
https://doi.org/10.1109/CDC51059.2022.9992324
Althoff MFrehse GGirard A(2021)Set Propagation Techniques for Reachability AnalysisAnnual Review of Control, Robotics, and Autonomous Systems10.1146/annurev-control-071420-0819414:1(369-395)Online publication date: 3-May-2021
https://doi.org/10.1146/annurev-control-071420-081941
Althoff MMaierhofer SPek C(2021)Provably-Correct and Comfortable Adaptive Cruise ControlIEEE Transactions on Intelligent Vehicles10.1109/TIV.2020.29919536:1(159-174)Online publication date: Mar-2021
https://doi.org/10.1109/TIV.2020.2991953
Schneider PButz MHeinzemann COehlerking JWoehrle M(2021)Towards threat metric evaluation in complex urban scenarios2021 IEEE International Intelligent Transportation Systems Conference (ITSC)10.1109/ITSC48978.2021.9564790(1192-1198)Online publication date: 19-Sep-2021
https://doi.org/10.1109/ITSC48978.2021.9564790
Althoff MRath J(2021)Comparison of guaranteed state estimators for linear time-invariant systemsAutomatica10.1016/j.automatica.2021.109662130(109662)Online publication date: Aug-2021
https://doi.org/10.1016/j.automatica.2021.109662
Althoff M(2020)Reachability Analysis of Large Linear Systems With Uncertain Inputs in the Krylov SubspaceIEEE Transactions on Automatic Control10.1109/TAC.2019.290643265:2(477-492)Online publication date: Feb-2020
https://doi.org/10.1109/TAC.2019.2906432
Tarraf AHedrich LKochdumper NRechmal-Lesse MOlbrich M(2020)Equivalence Checking Methods for Analog Circuits Using Continuous Reachable Sets2020 IEEE Computer Society Annual Symposium on VLSI (ISVLSI)10.1109/ISVLSI49217.2020.00012(7-12)Online publication date: Jul-2020
https://doi.org/10.1109/ISVLSI49217.2020.00012
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents