Document Open Access Logo

Parameterized Systems in BIP: Design and Model Checking

Authors Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.30.pdf
  • Filesize: 0.66 MB
  • 16 pages

Document Identifiers

Author Details

Igor Konnov
Tomer Kotek
Qiang Wang
Helmut Veith
Simon Bliudze
Joseph Sifakis

Cite As Get BibTex

Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, and Joseph Sifakis. Parameterized Systems in BIP: Design and Model Checking. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.30

Abstract

BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to systems parameterized in the number of components. We show that FOIL captures classical parameterized architectures such as token-passing rings, cliques of identical components communicating with rendezvous or broadcast, and client-server systems.

Although the BIP framework includes efficient verification tools for statically-defined systems, none are available for parameterized systems with an unbounded number of components. The parameterized model checking literature contains a wealth of techniques for systems of classical architectures. However, application of these results requires a deep understanding of parameterized model checking techniques and their underlying mathematical models. To overcome these difficulties, we introduce a framework that automatically identifies parameterized model checking techniques applicable to a BIP design. To our knowledge, it is the first framework that allows one to apply prominent parameterized model checking results in a systematic way.

Subject Classification

Keywords
  • Rigorous system design
  • BIP
  • verification
  • parameterized model checking

Metrics

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

References

  1. P. A. Abdulla, K. Cerans, B. Jonsson, and Y. Tsay. General decidability theorems for infinite-state systems. In LICS, 1996. Google Scholar
  2. P. A. Abdulla, G. Delzanno, N. B. Henda, and A. Rezine. Monotonic abstraction: on efficient verification of parameterized systems. Int. J. Found. Comput. Sci., 2009. Google Scholar
  3. B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith. Parameterized model checking of rendezvous systems. In CONCUR. Springer, 2014. Google Scholar
  4. A. Basu, S. Bensalem, M. Bozga, J. Combaz, M. Jaber, T. Nguyen, and J. Sifakis. Rigorous component-based system design using the BIP framework. Software, IEEE, 2011. Google Scholar
  5. S. Bliudze, A. Cimatti, M. Jaber, S. Mover, M. Roveri, W. Saab, and Q. Wang. Formal verification of infinite-state BIP models. In ATVA, 2015. Google Scholar
  6. S. Bliudze and J. Sifakis. The algebra of connectors - structuring interaction in BIP. In EMSOFT, 2007. Google Scholar
  7. S. Bliudze and J. Sifakis. Causal semantics for the algebra of connectors. FMSD, 2010. Google Scholar
  8. S. Bliudze and J. Sifakis. Synthesizing glue operators from glue constraints for the construction of component-based systems. In Software Composition, 2011. Google Scholar
  9. R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, and J. Widder. Decidability of parameterized verification. Synthesis Lectures on Distributed Computing Theory, 2015. Google Scholar
  10. M. Bozga, M. Jaber, N. Maris, and J. Sifakis. Modeling dynamic architectures using Dy-BIP. In Software Composition. Springer, 2012. Google Scholar
  11. R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta. The nuXmv symbolic model checker. In CAV, 2014. Google Scholar
  12. E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999. Google Scholar
  13. E. Clarke, M. Talupur, T. Touili, and H. Veith. Verification by network decomposition. In CONCUR, 2004. Google Scholar
  14. L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008. Google Scholar
  15. E. A. Emerson and V. Kahlon. Model checking guarded protocols. In LICS, 2003. Google Scholar
  16. E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In POPL, 1995. Google Scholar
  17. J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. LICS, 1999. Google Scholar
  18. S. M. German and A. P. Sistla. Reasoning about systems with many processes. J. ACM, 1992. Google Scholar
  19. O. Grumberg and H. Veith. 25 years of model checking: history, achievements, perspectives. Springer, 2008. Google Scholar
  20. J. Y Halpern. Presburger arithmetic with unary predicates is π₁¹ complete. J. of Symb. Logic, 1991. Google Scholar
  21. A. Mavridou, E. Baranov, S. Bliudze, and J. Sifakis. Configuration logics: Modelling architecture styles. In FACS, 2015. Google Scholar
  22. Q.Wang and S. Bliudze. Verification of component-based systems via predicate abstraction and simultaneous set reduction. In TGC, 2015. Google Scholar
  23. S. Schmitz and P. Schnoebelen. The power of well-structured systems. In CONCUR, 2013. Google Scholar
  24. J. Sifakis. Rigorous system design. Foundations and Trends in Electr. Design Automation, 2013. Google Scholar
  25. J. Sifakis. System design automation: Challenges and limitations. Proc. of the IEEE, 2015. Google Scholar
  26. I. Suzuki. Proving properties of a ring of finite-state machines. Inf. Process. Lett., 1988. Google Scholar
  27. W. Thomas. Languages, automata, and logic. Springer, 1997. 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 About DROPS Imprint Privacy Contact