Document Open Access Logo

On an Invariance Problem for Parameterized Concurrent Systems

Authors Marius Bozga, Lucas Bueri, Radu Iosif

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.24.pdf
  • Filesize: 0.82 MB
  • 16 pages

Document Identifiers

Author Details

Marius Bozga
  • Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France
Lucas Bueri
  • Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France
Radu Iosif
  • Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France

Cite AsGet BibTex

Marius Bozga, Lucas Bueri, and Radu Iosif. On an Invariance Problem for Parameterized Concurrent Systems. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.24

Abstract

We consider concurrent systems consisting of replicated finite-state processes that synchronize via joint interactions in a network with user-defined topology. The system is specified using a resource logic with a multiplicative connective and inductively defined predicates, reminiscent of Separation Logic [John C. Reynolds, 2002]. The problem we consider is if a given formula in this logic defines an invariant, namely whether any model of the formula, following an arbitrary firing sequence of interactions, is transformed into another model of the same formula. This property, called havoc invariance, is quintessential in proving the correctness of reconfiguration programs that change the structure of the network at runtime. We show that the havoc invariance problem is many-one reducible to the entailment problem ϕ ⊧ ψ, asking if any model of ϕ is also a model of ψ. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • parameterized verification
  • invariant checking
  • resource logics
  • reconfigurable systems
  • tree automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Emma Ahrens, Marius Bozga, Radu Iosif, and Joost-Pieter Katoen. Local reasoning about parameterized reconfigurable distributed systems. CoRR, abs/2107.05253, 2021. URL: http://arxiv.org/abs/2107.05253.
  2. Yehoshua Bar-Hillel, Micha Perles, and Eli Shamir. On formal properties of simple phrase structure grammars. Sprachtypologie und Universalienforschung, 14:143-172, 1961. Google Scholar
  3. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. Google Scholar
  4. Marius Bozga, Lucas Bueri, and Radu Iosif. Decision problems in a logic for reasoning about reconfigurable distributed systems. In International Joint Conference on Automated Reasoning, to appear, 2022. URL: http://arxiv.org/abs/2202.09637.
  5. Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis, and Christoph Welzel. Structural invariants for the verification of systems with parameterized architectures. In Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, volume 12078 of LNCS, pages 228-246. Springer, 2020. Google Scholar
  6. Marius Bozga and Radu Iosif. Specification and safety verification of parametric hierarchical distributed systems. In Formal Aspects of Component Software - 17th International Conference, FACS 2021, Virtual Event, October 28-29, 2021, Proceedings, volume 13077 of Lecture Notes in Computer Science, pages 95-114. Springer, 2021. Google Scholar
  7. Antonio Bucchiarone and Juan P. Galeotti. Dynamic software architectures verification using dynalloy. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 10, 2008. Google Scholar
  8. Cristiano Calcagno, Peter W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 366-378. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.30.
  9. Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, and James Worrell. Tractable reasoning in a fragment of separation logic. In CONCUR, volume 6901 of Lecture Notes in Computer Science, pages 235-249. Springer, 2011. Google Scholar
  10. Julien Dormoy, Olga Kouchnarenko, and Arnaud Lanoix. Using temporal logic for dynamic reconfigurations of components. In Luís Soares Barbosa and Markus Lumpe, editors, Formal Aspects of Component Software - 7th International Workshop, FACS 2010, volume 6921 of Lecture Notes in Computer Science, pages 200-217. Springer, 2010. Google Scholar
  11. Antoine El-Hokayem, Marius Bozga, and Joseph Sifakis. A temporal configuration logic for dynamic reconfigurable systems. In Chih-Cheng Hung, Jiman Hong, Alessio Bechini, and Eunjee Song, editors, SAC '21: The 36th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, Republic of Korea, March 22-26, 2021, pages 1419-1428. ACM, 2021. URL: https://doi.org/10.1145/3412841.3442017.
  12. Klaus-Tycho Foerster and Stefan Schmid. Survey of reconfigurable data center networks: Enablers, algorithms, complexity. SIGACT News, 50(2):62-79, 2019. Google Scholar
  13. Dan Hirsch, Paolo Inverardi, and Ugo Montanari. Graph grammars and constraint solving for software architecture styles. In Proceedings of the Third International Workshop on Software Architecture, ISAW '98, pages 69-72, New York, NY, USA, 1998. Association for Computing Machinery. URL: https://doi.org/10.1145/288408.288426.
  14. Yonit Kesten, Amir Pnueli, Elad Shahar, and Lenore D. Zuck. Network invariants in action. In CONCUR 2002 - Concurrency Theory, 13th International Conference, volume 2421 of LNCS, pages 101-115. Springer, 2002. Google Scholar
  15. Arnaud Lanoix, Julien Dormoy, and Olga Kouchnarenko. Combining proof and model-checking to validate reconfigurable architectures. Electron. Notes Theor. Comput. Sci., 279(2):43-57, 2011. Google Scholar
  16. Daniel Le Metayer. Describing software architecture styles using graph grammars. IEEE Transactions on Software Engineering, 24(7):521-533, 1998. URL: https://doi.org/10.1109/32.708567.
  17. David Lesens, Nicolas Halbwachs, and Pascal Raymond. Automatic verification of parameterized linear networks of processes. In The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 346-357. ACM Press, 1997. Google Scholar
  18. Mohammad Noormohammadpour and Cauligi S. Raghavendra. Datacenter traffic control: Understanding techniques and tradeoffs. IEEE Commun. Surv. Tutorials, 20(2):1492-1525, 2018. Google Scholar
  19. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  20. Ze'ev Shtadler and Orna Grumberg. Network grammars, communication behaviors and automatic verification. In Joseph Sifakis, editor, Automatic Verification Methods for Finite State Systems, International Workshop, volume 407 of LNCS, pages 151-165. Springer, 1989. Google Scholar
  21. Pierre Wolper and Vinciane Lovinfosse. Verifying properties of large sets of processes with network invariants. In Automatic Verification Methods for Finite State Systems, International Workshop, volume 407 of LNCS, pages 68-80. Springer, 1989. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact