2026-07-22T11:26:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6167 2024-03-06T10:38:30Z ddc:004 open_access

Parameterized Systems in BIP: Design and Model Checking Konnov, Igor Kotek, Tomer Wang, Qiang Veith, Helmut Bliudze, Simon Joseph Sifakis Rigorous system design BIP verification parameterized model checking 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Igor Konnov and Tomer Kotek and Qiang Wang and Helmut Veith and Simon Bliudze and Joseph Sifakis 2016 Is Part Of LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2016.30 urn:nbn:de:0030-drops-61670 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.30 eng https://creativecommons.org/licenses/by/3.0/legalcode