zbMATH — the first resource for mathematics

Parameterized systems in BIP: design and model checking. (English) Zbl 1392.68254
Desharnais, Josée (ed.) et al., 27th international conference on concurrency theory, CONCUR 2016, Québec City, Canada, August 23–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-017-0). LIPIcs – Leibniz International Proceedings in Informatics 59, Article 30, 16 p. (2016).
Summary: BIP is a component-based framework for system design built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP without priority 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. On the other hand, 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.
For the entire collection see [Zbl 1351.68014].

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX Cite
Full Text: DOI