Parameterized Systems in BIP: Design and 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.
Rigorous system design
BIP
verification
parameterized model checking
30:1-30:16
Regular Paper
Igor
Konnov
Igor Konnov
Tomer
Kotek
Tomer Kotek
Qiang
Wang
Qiang Wang
Helmut
Veith
Helmut Veith
Simon
Bliudze
Simon Bliudze
Joseph Sifakis
Joseph Sifakis
10.4230/LIPIcs.CONCUR.2016.30
P. A. Abdulla, K. Cerans, B. Jonsson, and Y. Tsay. General decidability theorems for infinite-state systems. In LICS, 1996.
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.
B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith. Parameterized model checking of rendezvous systems. In CONCUR. Springer, 2014.
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.
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.
S. Bliudze and J. Sifakis. The algebra of connectors - structuring interaction in BIP. In EMSOFT, 2007.
S. Bliudze and J. Sifakis. Causal semantics for the algebra of connectors. FMSD, 2010.
S. Bliudze and J. Sifakis. Synthesizing glue operators from glue constraints for the construction of component-based systems. In Software Composition, 2011.
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.
M. Bozga, M. Jaber, N. Maris, and J. Sifakis. Modeling dynamic architectures using Dy-BIP. In Software Composition. Springer, 2012.
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.
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
E. Clarke, M. Talupur, T. Touili, and H. Veith. Verification by network decomposition. In CONCUR, 2004.
L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008.
E. A. Emerson and V. Kahlon. Model checking guarded protocols. In LICS, 2003.
E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In POPL, 1995.
J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. LICS, 1999.
S. M. German and A. P. Sistla. Reasoning about systems with many processes. J. ACM, 1992.
O. Grumberg and H. Veith. 25 years of model checking: history, achievements, perspectives. Springer, 2008.
J. Y Halpern. Presburger arithmetic with unary predicates is π₁¹ complete. J. of Symb. Logic, 1991.
A. Mavridou, E. Baranov, S. Bliudze, and J. Sifakis. Configuration logics: Modelling architecture styles. In FACS, 2015.
Q.Wang and S. Bliudze. Verification of component-based systems via predicate abstraction and simultaneous set reduction. In TGC, 2015.
S. Schmitz and P. Schnoebelen. The power of well-structured systems. In CONCUR, 2013.
J. Sifakis. Rigorous system design. Foundations and Trends in Electr. Design Automation, 2013.
J. Sifakis. System design automation: Challenges and limitations. Proc. of the IEEE, 2015.
I. Suzuki. Proving properties of a ring of finite-state machines. Inf. Process. Lett., 1988.
W. Thomas. Languages, automata, and logic. Springer, 1997.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode