research-article

Public Access

Probabilistic conformance for cyber-physical systems

Authors:

Borzoo Bonakdarpoor,

Miroslav PajicAuthors Info & Claims

ICCPS '21: Proceedings of the ACM/IEEE 12th International Conference on Cyber-Physical Systems

Pages 55 - 66

https://doi.org/10.1145/3450267.3450534

Published: 19 May 2021 Publication History

Abstract

In system analysis, conformance indicates that two systems simultaneously satisfy the same set of specifications of interest; thus, the results from analyzing one system automatically transfer to the other, or one system can safely replace the other in practice. In this work, we study the probabilistic conformance of cyber-physical systems (CPS). We propose a notion of (approximate) probabilistic conformance for sets of complex specifications expressed by the Signal Temporal Logic (STL). Based on a novel statistical test, we develop the first statistical verification methods for the probabilistic conformance of a wide class of CPS. Using this method, we verify the conformance of the startup time of the widely-used full and simplified model of Toyota powertrain systems, the settling time of model-predictive-control-based and neural-network-based automotive lane-keeping controllers, as well as the maximal voltage deviation of full and simplified power grid systems.

References

[1]

Houssam Abbas, Hans Mittelmann, and Georgios Fainekos. 2014. Formal Property Verification in a Conformance Testing Framework. In 12th ACM/IEEE Conf. on Formal Methods and Models for Codesign (MEMOCODE). 155--164.

Digital Library

[2]

Gul Agha and Karl Palmskog. 2018. A Survey of Statistical Model Checking. ACM Trans. Model. Comput. Simul. 28, 1 (2018), 6:1--6:39.

Digital Library

[3]

Eugene Asarin, Alexandre Donzé, Oded Maler, and Dejan Nickovic. 2011. Parametric identification of temporal properties. In International Conference on Runtime Verification. 147--160.

[4]

Steven RH Barrett, Raymond L Speth, Sebastian D Eastham, Irene C Dedoussi, Akshay Ashok, Robert Malina, and David W Keith. 2015. Impact of the Volkswagen emissions control defeat device on US public health. Environmental Research Letters 10, 11 (2015), 114005.

[5]

Gilles Barthe, Pedro R D'Argenio, Bernd Finkbeiner, and Holger Hermanns. 2016. Facets of software doping. In International Symposium on Leveraging Applications of Formal Methods. Springer, 601--608.

[6]

CPSL@Duke. 2020. Probabilistic Conformance for CPS: Case-Studies. https://gitlab.oit.duke.edu/cpsl/conformance.

[7]

Dennis Dams and Orna Grumberg. 2018. Abstraction and Abstraction Refinement. In Handbook of Model Checking. Springer International, 385--419.

[8]

Moacyr A. G. De Brito, Leonardo P. Sampaio, G. Luigi, Guilherme A. e Melo, and Carlos A. Canesin. 2011. Comparative analysis of MPPT techniques for PV applications. In 2011 International Conference on Clean Electrical Power. 99--104.

[9]

Jyotirmoy V. Deshmukh, Rupak Majumdar, and Vinayak S. Prabhu. 2017. Quantifying Conformance Using the Skorokhod Metric. Formal Methods in System Design 50, 2 (2017), 168--206.

Digital Library

[10]

Jyotirmoy V. Deshpande, Uttara Naik-Nimbalkar, and Isha Dewan. 2018. Non-parametric Statistics: Theory and Methods.

[11]

Giovanni Fasano and Alberto Franceschini. 1987. A multidimensional version of the Kolmogorov-Smirnov test. Monthly Notices of the Royal Astronomical Society 225, 1 (1987), 155--170.

[12]

Thomas D Gillespie. 1992. Fundamentals of vehicle dynamics. Vol. 400. Society of automotive engineers Warrendale, PA.

[13]

Alexander Graf-Brill and Holger Hermanns. 2019. Component-aware Input-Output Conformance. In International Conference on Formal Techniques for Distributed Objects, Components, and Systems. 111--128.

[14]

Lex Heerink and Jan Tretmans. 1996. Formal Methods in Conformance Testing: A Probabilistic Refinement. In Int. Work. on Testing of Communicating Sys. 261--276.

[15]

Thomas A Henzinger. 2000. The theory of hybrid automata. In Verification of Digital and Hybrid Systems. Springer, 265--292.

[16]

Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts. 2014. Powertrain Control Verification Benchmark. In The 17th International Conference on Hybrid Systems: Computation and Control. 253--262.

[17]

Augung A. Julius and George J. Pappas. 2009. Approximations of Stochastic Hybrid Systems. IEEE Trans. Automat. Control 54, 6 (2009), 1193--1203.

[18]

Narges Khakpour and Mohammad Reza Mousavi. 2015. Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap. In 26th International Conference on Concurrency Theory (CONCUR), Vol. 42. 18--40.

[19]

Kim G. Larsen and Axel Legay. 2016. Statistical Model Checking: Past, Present, and Future. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 3--15.

[20]

Axel Legay, Benoît Delahaye, and Saddek Bensalem. 2010. Statistical Model Checking: An Overview. In Runtime Verification. Vol. 6418. 122--135.

[21]

Stephan B. Liu and Matthias Althoff. 2018. Reachset Conformance of Forward Dynamic Models for the Formal Analysis of Robots. In IEEE/RSJ International Conf. on Intelligent Robots and Systems (IROS). 370--376.

[22]

Natalia López, Manuel Núñez, and Ismael Rodríguez. 2006. Specification, Testing and Implementation Relations for Symbolic-Probabilistic Systems. Theoretical Computer Science 353, 1-3 (2006), 228--248.

Digital Library

[23]

Rupak Majumdar, Indranil Saha, Koichi Ueda, and Hakan Yazarel. 2013. Compositional equivalence checking for models and code of control systems. In 52nd IEEE Conference on Decision and Control. 1564--1571.

[24]

Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 152--166.

[25]

MathWorks, Inc. 2019. lane-keeping Assist System,. https://www.mathworks.com/help/mpc/ug/lane-keeping-assist-system-using-model-predictive-control.htmll. Accessed: 2019-7-15.

[26]

MathWorks, Inc. 2019. Model Predictive Control Toolbox. https://www.mathworks.com/help/mpc/ug/lane-keeping-assist-system-using-model-predictive-control.html. Accessed: 2019-7-15.

[27]

MathWorks, Inc. 2019. PowerSim. https://www.mathworks.com/help/physmod/sps/index.html?s_tid=CRUX_lftnav. Accessed: 2019-7-15.

[28]

MathWorks, Inc. 2019. SimPower. https://www.mathworks.com/help/physmod/sps/examples/250-kw-grid-connected-pv-array.html. Accessed: 2019-7-15.

[29]

Yunpeng Pan, Ching-An Cheng, Kamil Saigol, Keuntaek Lee, Xinyan Yan, Evangelos Theodorou, and Byron Boots. 2017. Agile autonomous driving using end-to-end deep imitation learning. arXiv preprint arXiv:1709.07174 (2017).

[30]

John A. Peacock. 1983. Two-dimensional goodness-of-fit testing in astronomy. Monthly Notices of the Royal Astronomical Society 202, 3 (1983), 615--627.

[31]

Srinivas Pinisetty, Gerardo Schneider, and David Sands. 2018. Runtime Verification of Hyperproperties for Deterministic Programs. In Proceedings of the 6th Conference on Formal Methods in Software Engineering - FormaliSE '18. 20--29.

Digital Library

[32]

Hendrik Roehm, Jens Oehlerking, Matthias Woehrle, and Matthias Althoff. 2016. Reachset Conformance Testing of Hybrid Automata. In 19th International Conference on Hybrid Systems: Computation and Control (HSCC). 277--286.

[33]

Nima Roohi, Yu Wang, Matthew West, Geir E. Dullerud, and Mahesh Viswanathan. 2017. Statistical Verification of the Toyota Powertrain Control Verification Benchmark. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control (HSCC). 65--70.

Digital Library

[34]

Michael Ryabtsev and Ofer Strichman. 2009. Translation validation: From simulink to c. In International Conference on Computer Aided Verification. 696--701.

Digital Library

[35]

Jeremy Sproston. 2000. Decidable Model Checking of Probabilistic Hybrid Automata. In Formal Techniques in Real-Time and Fault-Tolerant Systems. 31--45.

[36]

Kishor S. Trivedi, Andrea Bobbio, and Jogesh Muppala. 2017. Reliability and Availability Engineering: Modeling, Analysis, and Applications.

[37]

A. W. van der Vaart and Jon A Wellner. 1996. Glivenko-Cantelli Theorems. In Weak Convergence and Empirical Processes. Springer, 122--126.

[38]

Yu Wang, Siddhartha Nalluri, Borzoo Bonakdarpour, and Miroslav Pajic. 2021. Statistical model checking for hyperproperties. In IEEE Computer Security Foundations Symposium (CSF). To appear.

[39]

Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir E. Dullerud. 2015. Statistical Verification of Dynamical Systems Using Set Oriented Methods. In 18th Int. Conf. on Hybrid Systems: Computation and Control (HSCC). 169--178.

[40]

Yu Wang, Mojtaba Zarei, Borzoo Bonakdarpour, and Miroslav Pajic. 2019. Statistical Verification of Hyperproperties for Cyber-Physical Systems. ACM Transactions on Embedded Computing Systems 18, 5s (2019), 1--23.

Digital Library

[41]

Mojtaba Zarei, Yu Wang, and Miroslav Pajic. 2020. Statistical verification of learning-based cyber-physical systems. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control (HSCC). 1--7.

Digital Library

[42]

Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, and Ernst Moritz Hahn. 2010. Safety Verification for Probabilistic Hybrid Systems. In Computer Aided Verification. 196--211.

Cited By

Nguyen HRakib A(2023)Formal Modelling and Verification of Probabilistic Resource Bounded AgentsJournal of Logic, Language and Information10.1007/s10849-023-09405-132:5(829-859)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1007/s10849-023-09405-1
Wang YSibai HYen MMitra SDullerud G(2022)Differentially Private Algorithms for Statistical Verification of Cyber-Physical SystemsIEEE Open Journal of Control Systems10.1109/OJCSYS.2022.32071081(294-305)Online publication date: 2022
https://doi.org/10.1109/OJCSYS.2022.3207108
Liu YMa YYang YZheng T(2021)Counterexample Generation for Probabilistic Model Checking Micro-Scale Cyber-Physical SystemsMicromachines10.3390/mi1209105912:9(1059)Online publication date: 31-Aug-2021
https://doi.org/10.3390/mi12091059

Index Terms

Probabilistic conformance for cyber-physical systems

Recommendations

Falsification of cyber-physical systems with robustness-guided black-box checking
HSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control

For exhaustive formal verification, industrial-scale cyber-physical systems (CPSs) are often too large and complex, and lightweight alternatives (e.g., monitoring and testing) have attracted the attention of both industrial practitioners and academic ...
Model Conformance for Cyber-Physical Systems: A Survey
Special Issue on Real Time Aspects in CPS and Regular Papers (Diamonds)

Model-based development is an important paradigm for developing cyber-physical systems (CPS). The underlying assumption is that the functional behavior of a model is related to the behavior of a more concretized model or the real system. A formal ...
Conformance testing for cyber-physical systems

Cyber-Physical Systems (CPS) require a high degree of reliability and robustness. Hence it is important to assert their correctness with respect to extra-functional properties, like power consumption, temperature, etc. In turn the physical quantities ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCPS '21: Proceedings of the ACM/IEEE 12th International Conference on Cyber-Physical Systems

May 2021

242 pages

ISBN:9781450383530

DOI:10.1145/3450267

General Chairs:
Martina Maggio
Lund University
,
James Weimer
University of Pennsylvania
,
Program Chairs:
Mohammad Al Faruque
University of California at Irvine
,
Meeko Oishi
University of New Mexico

Copyright © 2021 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

In-Cooperation

IEEE-CS\TCRT: TC on Real-Time Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 May 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

ICCPS '21

Sponsor:

SIGBED

ICCPS '21: ACM/IEEE 12th International Conference on Cyber-Physical Systems

May 19 - 21, 2021

Tennessee, Nashville

Acceptance Rates

Overall Acceptance Rate 25 of 91 submissions, 27%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
361
Total Downloads

Downloads (Last 12 months)99
Downloads (Last 6 weeks)19

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nguyen HRakib A(2023)Formal Modelling and Verification of Probabilistic Resource Bounded AgentsJournal of Logic, Language and Information10.1007/s10849-023-09405-132:5(829-859)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1007/s10849-023-09405-1
Wang YSibai HYen MMitra SDullerud G(2022)Differentially Private Algorithms for Statistical Verification of Cyber-Physical SystemsIEEE Open Journal of Control Systems10.1109/OJCSYS.2022.32071081(294-305)Online publication date: 2022
https://doi.org/10.1109/OJCSYS.2022.3207108
Liu YMa YYang YZheng T(2021)Counterexample Generation for Probabilistic Model Checking Micro-Scale Cyber-Physical SystemsMicromachines10.3390/mi1209105912:9(1059)Online publication date: 31-Aug-2021
https://doi.org/10.3390/mi12091059

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents