Hostname: page-component-cd9895bd7-hc48f Total loading time: 0 Render date: 2024-12-22T20:10:49.341Z Has data issue: false hasContentIssue false
  • English
  • Français

Detection and diagnosis of deviations in distributed systems of autonomous agents

Published online by Cambridge University Press:  06 September 2022

Vivek Nigam Open the ORCID record for Vivek Nigam [Opens in a new window] ,
Minyoung Kim ,
Ian Mason  and
Carolyn Talcott
Vivek Nigam*
Affiliation:
Federal University of Paraíba, João Pessoa, Brazil
Minyoung Kim
Affiliation:
SRI International, Menlo Park, CA 94025, USA
Ian Mason
Affiliation:
SRI International, Menlo Park, CA 94025, USA
Carolyn Talcott
Affiliation:
SRI International, Menlo Park, CA 94025, USA
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Given the complexity of cyber-physical systems (CPS), such as swarms of drones, often deviations, from a planned mission or protocol, occur which may in some cases lead to harm and losses. To increase the robustness of such systems, it is necessary to detect when deviations happen and diagnose the cause(s) for a deviation. We build on our previous work on soft agents, a formal framework based on using rewriting logic for specifying and reasoning about distributed CPS, to develop methods for diagnosis of CPS at design time. We accomplish this by (1) extending the soft agents framework with Fault Models; (2) proposing a protocol specification language and the definition of protocol deviations; and (3) development of workflows/algorithms for detection and diagnosis of protocol deviations. Our approach is partially inspired by existing work using counterfactual reasoning for fault ascription. We demonstrate our machinery with a collection of experiments.

Keywords

Counterfactual ReasoningSoft AgentsRewriting LogicCyber-Physical Systems
Type
Special Issue: LSFA’19 and LSFA’20
Information
Mathematical Structures in Computer Science , Volume 32 , Special Issue 9: LSFA 2019 and 2020 , October 2022 , pp. 1254 - 1282
Check for updates
Copyright
© The Author(s), 2022. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Alur, R., Courcoubetis, C., Henzinger, T. A. and Ho, P. (1992). Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R. L., Nerode, A., Ravn, A. P., and Rischel, H. (eds.) Hybrid Systems, Lecture Notes in Computer Science, vol. 736, Springer, 209–229.CrossRefGoogle Scholar
Basin, D., Cremers, C., Dreier, J. and Sasse, R. (2017). Symbolically analyzing security protocols using tamarin. ACM SIGLOG News 4 (4) 19–30.CrossRefGoogle Scholar
Basin, D., Cremers, C. and Meier, S. (2012). Provably repairing the ISO/IEC 9798 Standard for entity authentication. In: POST, LNCS, vol. 7215, Springer-Verlag Berlin Heidelberg, 129–148.Google Scholar
Bistarelli, S., Montanari, U. and Rossi, F. (1997). Semiring-based constraint satisfaction and optimization. Journal of the ACM 44 (2) 201–236.CrossRefGoogle Scholar
Choi, J. S., McCarthy, T., Kim, M. and Stehr, M.-O. (2013). Adaptive wireless networks as an example of declarative fractionated systems. In: Mobile and Ubiquitous Systems: Computing, Networking, and Services. MobiQuitous 2013, Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol. 131, Springer.Google Scholar
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J. and Talcott, C. (2007). All About Maude: A High-Performance Logical Framework , LNCS, vol. 4350, Springer.Google Scholar
Dantas, Y. G., Nigam, V. and Talcott, C. L. (2020). A formal security assessment framework for cooperative adaptive cruise control. In: IEEE Vehicular Networking Conference, VNC 2020, New York, NY, USA, December 16–18, 2020, IEEE, 1–8.CrossRefGoogle Scholar
Debouk, R., Lafortune, S. and Teneketzis, D. (2000). Coordinated decentralized protocols for failure diagnosis of discrete event systems. Discrete Event Dynamic Systems 10 (1–2) 33–86.CrossRefGoogle Scholar
Frehse, G. and Althoff, M. (eds.) (2021). 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), EPiC Series in Computing, EPIC.Google Scholar
Gössler, G. and Astefanoaei, L. (2014). Blaming in component-based real-time systems. In: Proceedings of the Embedded Software (EMSOFT), 7:1–7:10.Google Scholar
Gössler, G. and Stefani, J. (2016). Fault ascription in concurrent systems. In: Proceedings of the 2nd Symposium on Trustworthy Global Computing (TGC), LNCS, vol. 9533, Springer, 79–94.CrossRefGoogle Scholar
Gössler, G. and Stefani, J.-B. (2020). Causality analysis and fault ascription in component-based systems. Theoretical Computer Science 837 158–180.CrossRefGoogle Scholar
Halpern, J. and Pearl, J. (2005). Causes and explanations: A structural-model approach. Part I: Causes. British Journal for the Philosophy of Science 56 (4) 843–887.Google Scholar
Kamali, M., Dennis, L. A., McAree, O., Fisher, M. and Veres, S. M. (2017). Formal verification of autonomous vehicle platooning. Science of Computer Programming 148 88–106.CrossRefGoogle Scholar
Kanovich, M. I., Kirigin, T. B., Nigam, V., Scedrov, A., Talcott, C. L. and Perovic, R. (2017). A rewriting framework and logic for activities subject to regulations. Mathematical Structures in Computer Science 27 (3) 332–375.CrossRefGoogle Scholar
Kappé, T., Lion, B., Arbab, F. and Talcott, C. (2019). Soft component automata: Composition, compilation, logic, and verification. Science of Computer Programming 183 102300.CrossRefGoogle Scholar
Kim, M., Mason, I. and Talcott, C. 2019. Softagents diagnosis. Accessed: 2021-06-21.Google Scholar
Laurent, J., Yang, J. and Fontana, W. (2018). Counterfactual resimulation for causal analysis of rule-based models. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), 1182–1890.CrossRefGoogle Scholar
Lee, J., Kim, S., Bae, K. and Ölveczky, P. C. (2021). HYBRID SYNCHAADL: Modeling and formal analysis of virtually synchronous CPSs in AADL. In: Silva, A. and Leino, K. R. M. (eds.) Computer Aided Verification, Lecture Notes in Computer Science, vol. 12759, Cham, Springer.CrossRefGoogle Scholar
Mason, I. A., Nigam, V., Talcott, C. and Brito, A. (2017). A framework for analyzing adaptive autonomous aerial vehicles. In: 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems.Google Scholar
Maude-Team (2021). The Maude System. Accessed: 2021-06-21.Google Scholar
Meseguer, J. (1992). Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96 (1) 73–155.CrossRefGoogle Scholar
Meseguer, J. (2012). Twenty years of rewriting logic. The Journal of Logic and Algebraic Programming 81 (7–8) 721–781.CrossRefGoogle Scholar
Mitra, S. (2021). Verifying Cyber-Physical Systems, Cambridge, MA, MIT Press.Google Scholar
Moradi, F., Asadollah, S. A., Sedaghatbaf, A., Causevic, A., Sirjani, M. and Talcott, C. L. 2020. An actor-based approach for security analysis of cyber-physical systems. In: Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Vienna, Austria, September 2–3, 2020, Proceedings, 130–147.Google Scholar
Nigam, V. and Talcott, C. (2022). Automating safety proofs about cyber-physical systems using rewriting modulo SMT. In: Bae, K. (ed.) 14th International Workshop on Rewriting Logic and its Applications, 164–181.CrossRefGoogle Scholar
Pearl, J. (2000). Causality: Models, Reasoning, and Inference, New York, NY, Cambridge University Press.Google Scholar
Pnueli, A. (1977). The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October–1 November 1977, IEEE Computer Society, 46–57.CrossRefGoogle Scholar
Schmidt, B., Meier, S., Cremers, C. and Basin, D. (2012). Automated analysis of diffie-hellman protocols and advanced security properties. In: IEEE 25th Computer Security Foundations Symposium, 78–94.CrossRefGoogle Scholar
Sha, L., Al-Nayeem, A., Sun, M., Meseguer, J. and Ölveczky, P. C. (2009). PALS: Physically asynchronous logically synchronous systems. In: The IEEE Real-Time Systems Symposium.Google Scholar
Talcott, C., Arbab, F. and Yadav, M. (2015). Soft agents: Exploring soft constraints to model robust adaptive distributed cyber-physical agent systems. In: Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, LNCS, vol. 8950, Springer.Google Scholar
Talcott, C., Nigam, V., Arbab, F. and Kappe, T. (2016). Formal specification and analysis of robust adaptive distributed cyber-physical systems. In: SFM 2016: Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems, LNCS, vol. 9700, Springer, 1–35.CrossRefGoogle Scholar
Urquiza, A. A., Alturki, M. A., Kirigin, T. B., Kanovich, M. I., Nigam, V., Scedrov, A. and Talcott, C. L. (2021). Resource and timing aspects of security protocols. Journal of Computer Security 29 (3) 299–340.Google Scholar