Abstract
Reduction and abstraction techniques have been proposed to address the state space explosion problem in verification. In this paper, we present reduction and abstraction techniques for component-based systems modeled in BIP (Behavior, Interaction and Priority). Given a BIP system consisting of several atomic components, we select two atomic components amenable for reduction and compute their product. The resulting product component typically contains constants and branching bisimilar states. We use constant propagation to reduce the resulting component. Then we use a branching bisimulation abstraction to compute an abstraction of the product component. The presented method is fully implemented and scales to large designs not possible to verify with existing techniques.
Mohamad Noureddine – The presented work was partially realised while this author was at EPFL for a summer internship. The authors are listed alphabetically.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
All sets are finite.
- 2.
Here and below, we omit the index on \(\xrightarrow {}\), since it is always clear from the context.
References
Aziz, A., Singhal, V., Swamy, G., Brayton, R.K.: Minimizing interacting finite state machines: a compositional approach to language to containment. In: ICCD, pp. 255–261 (1994)
Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the bip framework. IEEE Softw. 28(3), 41–48 (2011)
Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-Finder: a tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 614–619. Springer, Heidelberg (2009)
Bliudze, S., Sifakis, J.: A notion of glue expressiveness for component-based systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 508–522. Springer, Heidelberg (2008)
Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. Electron. Notes Theor. Comput. Sci. 89(1), 99–113 (2003). PDMC 2003, Parallel and Distributed Model Checking (Satellite Workshop of CAV 2003)
Bloom, B.: Ready simulation, bisimulation, and the semantics of CCS-like languages. Ph.D. thesis, Massachusetts Institute of Technology (1989)
Chaudron, M., Eskenazi, E., Fioukov, A., Hammer, D.: A framework for formal component-based software architecting. In: OOPSLA, pp. 73–80 (2001)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Crouzen, P., Hermanns, H.: Aggregation ordering for massively compositional models. In: 2010 10th International Conference on Application of Concurrency to System Design (ACSD), pp. 171–180. IEEE (2010)
Crouzen, P., Lang, F.: Smart reduction. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 111–126. Springer, Heidelberg (2011)
Emerson, E.A., Wahl, T.: Efficient reduction techniques for systems with many components. Electr. Notes Theor. Comput. Sci. 130, 379–399 (2005)
Garavel, H., Sifakis, J.: Compilation and verification of lotos specifications. PSTV 10, 359–376 (1990)
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)
Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: CAV, pp. 186–196 (1990)
Groote, J.F., Ponse, A.: The syntax and semantics of \(\mu \)CRL. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds.) Algebra of Communicating Processes, pp. 26–62. Springer, London (1995)
Kildall, G.A.: A unified approach to global program optimization. In: POPL 1973, pp. 194–206. ACM, New York (1973)
Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846–862. Springer, Heidelberg (2013)
Lang, F.: Exp.Open 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 70–88. Springer, Heidelberg (2005)
Tai, K.C., Koppol, P.V.: Hierarchy-based incremental analysis of communication protocols. In: Proceedings of the 1993 International Conference on Network Protocols, 1993, pp. 318–325. IEEE (1993)
Wegman, M.N., Zadeck, F.K.: Constant propagation with conditional branches. ACM Trans. Program. Lang. Syst. 13(2), 181–210 (1991)
Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref – a symbolic bisimulation tool box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 477–492. Springer, Heidelberg (2006)
Zaraket, F.A., Baumgartner, J., Aziz, A.: Scalable compositional minimization via static analysis. In: ICCAD, pp. 1060–1067 (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Noureddine, M., Jaber, M., Bliudze, S., Zaraket, F.A. (2015). Reduction and Abstraction Techniques for BIP. In: Lanese, I., Madelaine, E. (eds) Formal Aspects of Component Software. FACS 2014. Lecture Notes in Computer Science(), vol 8997. Springer, Cham. https://doi.org/10.1007/978-3-319-15317-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-15317-9_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15316-2
Online ISBN: 978-3-319-15317-9
eBook Packages: Computer ScienceComputer Science (R0)