On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems
Authors: 
Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov, Carolyn TalcottAuthors Info & Claims
Pages 96 - 113
Abstract
Cyber-Physical Systems (CPS) are used to perform complex, safety-critical missions autonomously. Examples include applications of autonomous vehicles and drones. Given the complexity of these systems, CPS must be able to adapt to possible changes during mission execution, such as regulatory updates or changes in mission objectives. This capability is informally referred to as resilience. We formalize the intuitive notion of resilience as a formal verification property using timed multiset rewriting. An important innovation in our formalization is the distinction between rules that are under the control of the CPS and those that are not. We also study the computational complexity of resilience problems. Although undecidable in general, we show that these problems are PSPACE-complete for a class of bounded systems, more precisely, balanced systems where the rules do not affect the number of facts of the configurations and where facts are of bounded size.
References
[1]
Aires Urquiza A et al. Resource and timing aspects of security protocols J. Comput. Secur. 2021 29 3 299-340
[2]
Allenby B and Fink J Toward inherently secure and resilient societies Science 2005 309 5737 1034-1036
[3]
Banescu, S., Ochoa, M., Pretschner, A.: A framework for measuring software obfuscation resilience against automated attacks. In: 2015 IEEE/ACM 1st International Workshop on Software Protection, pp. 45–51 (2015)
[4]
Barker K, Ramirez-Marquez JE, and Rocco CM Resilience-based network component importance measures Reliab. Eng. Syst. Saf. 2013 117 89-97
[5]
Bloomfield, R., et al.: Towards identifying and closing gaps in assurance of autonomous road vehicles-a collection of technical notes part 1. arXiv preprint arXiv:2003.00789 (2020)
[6]
Bruneau M et al. A framework to quantitatively assess and enhance the seismic resilience of communities Earthq. Spectra 2003 19 4 733-752
[7]
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press (1972)
[8]
Henry D and Ramirez-Marquez JE Generic metrics and quantitative approaches for system resilience as a function of time Reliab. Eng. Syst. Saf. 2012 99 114-122
[9]
Holling CS Resilience and stability of ecological systems Annu. Rev. Ecol. Syst. 1973 4 1 1-23
[10]
Hosseini S, Barker K, and Ramirez-Marquez JE A review of definitions and measures of system resilience Reliab. Eng. Syst. Saf. 2016 145 47-61
[11]
Huang, W., et al.: Formal verification of robustness and resilience of learning-enabled state estimation systems for robotics (2020)
[12]
Kanovich M, Ban Kirigin T, Nigam V, Scedrov A, and Talcott CL Time, computational complexity, and probability in the analysis of distance-bounding protocols J. Comput. Secur. 2017 25 6 585-630
[13]
Kanovich M, Ban Kirigin T, Nigam V, Scedrov A, Talcott CL, and Perovic R A rewriting framework and logic for activities subject to regulations Math. Struct. Comput. Sci. 2017 27 3 332-375
[14]
Kanovich M, Kirigin TB, Nigam V, Scedrov A, and Talcott C Dougherty D, Meseguer J, Mödersheim SA, and Rowe P On the complexity of verification of time-sensitive distributed systems Protocols, Strands, and Logic 2021 Cham Springer 251-275
[15]
Laprie, J.C.: From dependability to resilience. In: 38th IEEE/IFIP International Conference on Dependable Systems and Networks, pp. G8–G9. Citeseer (2008)
[16]
Madni, A.M., Erwin, D., Sievers, M.: Constructing models for systems resilience: challenges, concepts, and formal methods. Systems 8(1) (2020)
[17]
Madni, A.M., Sievers, M.: Combining formal and probabilistic modeling in resilient systems design. Procedia Comput. Sci. 153, 343–351 (2019). 17th Annual Conference on Systems Engineering Research (CSER)
[18]
Mason IA, Nigam V, Talcott C, and Brito A Cerone A and Roveri M A framework for analyzing adaptive autonomous aerial vehicles Software Engineering and Formal Methods 2018 Cham Springer 406-422
[19]
Mouelhi S, Laarouchi ME, Cancila D, and Chaouchi H Predictive formal analysis of resilience in cyber-physical systems IEEE Access 2019 7 33741-33758
[20]
Nigam, V., Kim, M., Mason, I., Talcott, C.: Detection and diagnosis of deviations in distributed systems of autonomous agents. Math. Struct. Comput. Sci. (2022)
[21]
Nigam V and Talcott C Bae K Automating safety proofs about cyber-physical systems using rewriting modulo SMT Rewriting Logic and its Applications (WRLA) 2022 Cham Springer 212-229
[22]
NIST: Autonomy levels for unmanned systems (ALFUS) framework. https://www.nist.gov/system/files/documents/el/isd/ks/NISTSP_1011_ver_1-1.pdf
[23]
Pregenzer, A.: Systems resilience: a new analytical framework for nuclear nonproliferation. Sandia National Laboratories, Albuquerque (2011)
[24]
Ross, R., Pillitteri, V., Graubart, R., Bodeau, D., McQuaid, R.: Developing cyber resilient systems: a systems security engineering approach. Technical report, National Institute of Standards and Technology (2019)
[25]
SAE: Recommended practice: taxonomy and definitions for terms related to driving automation systems for on-road motor vehicles. https://www.sae.org/standards/content/j3016_202104/
[26]
Savitch WJ Relationship between nondeterministic and deterministic tape classes J. Comput. Syst. Sci. 1970 4 177-192
[27]
Sharma, V.C., Haran, A., Rakamaric, Z., Gopalakrishnan, G.: Towards formal approaches to system resilience. In: 2013 IEEE 19th Pacific Rim International Symposium on Dependable Computing, pp. 41–50 (2013)
[28]
Talcott C, Arbab F, and Yadav M De Nicola R and Hennicker R Soft agents: exploring soft constraints to model robust adaptive distributed cyber-physical agent systems Software, Services, and Systems 2015 Cham Springer 273-290
[29]
Talcott C, Nigam V, Arbab F, and Kappé T Bernardo M, De Nicola R, and Hillston J Formal specification and analysis of robust adaptive distributed cyber-physical systems Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems 2016 Cham Springer 1-35
[30]
U.S. Department of Defense: Dictionary of military and associated terms. https://fas.org/irp/doddir/dod/jp1_02.pdf
[31]
Vardi M Efficiency vs. resilience: what COVID-19 teaches computing Commun. ACM 2020 63 5 9
Index Terms
- On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems
Index terms have been assigned to the content through auto-classification.
Recommendations
A Formal Framework for ASTRAL Intralevel Proof Obligations
ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Formal assessment of reliability specifications in embedded cyber-physical systems
Reliability has become an integral component of the design intent of embedded cyber-physical systems. Safety-critical embedded systems are designed with specific reliability targets, and design practices include the appropriate allocation of both ...
On the Security and Complexity of Periodic Systems
AbstractRecent years have seen a tremendous increase in the reliance of industrial systems on a variety of interconnected components ranging in complexity from simple sensors to more complex cyber-physical and Internet of Things (IoT) devices, a class of ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sep 2022
493 pages
ISBN:978-3-031-17714-9
DOI:10.1007/978-3-031-17715-6
- Editors:
- Helmut Seidl,
- Zhiming Liu,
- Corina S. Pasareanu
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2022.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 27 September 2022
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 28 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in