Abstract
Automata-based interface and protocol specifications provide an elegant framework to capture and automatically verify the interactive behavior of component-based software systems. Unfortunately, the underlying formalisms suffer from combinatorial state explosion when constructing new specifications for composite components or systems and may therefore render the application of these techniques impractical for real-world applications. In this paper, we explore the bisimulation technique as a means for a mechanical state space reduction of component-based systems. In particular, we apply both strong and weak bisimulation to Component Interaction Automata in order to obtain a minimal automata that can serve as a behavioral equivalent abstraction for a given component specification and illustrate that the proposed approach can significantly reduce the complexity of an interface specification after composition.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arbab, F.: Reo: A Channel-based Coordination Model for Component Composition. Mathematical Structures in Computer Science 14(3), 329–366 (2004)
Baeten, J.C.M., Bergstra, J.A.: Real time process algebra. Formal Aspects of Computing 3(2), 142–188 (1991)
Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 119–130. Springer, Heidelberg (1997)
Blom, S., Orzan, S.: Distributed state space minimization. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 280–291 (2005)
Brim, L., Černá, I., Vařeková, P., Zimmerova, B.: Component-Interaction Automata as a Verification-Oriented Component-Based System Specification. SIGSOFT Software Engineering Notes 31(2), 1–8 (2006)
Broy, M.: A core theory of interfaces and architecture and its impact on object orientation. In: Reussner, R.H., Stafford, J.A., Szyperski, C.A. (eds.) Architecting Systems with Trustworthy Components. LNCS, vol. 3938, pp. 26–47. Springer, Heidelberg (2006)
Černá, I., Vařeková, P., Zimmerova, B.: Component Substitutability via Equivalencies of Component-Interaction Automata. Electronic Notes in Theoretical Computer Science 182, 39–55 (2007)
Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Jurdzinski, M., Mang, F.Y.C.: Interface compatibility checking for software modules. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 428–441. Springer, Heidelberg (2002)
Cheung, S.C., Kramer, J.: Checking safety properties using compositional reachability analysis. ACM Transactions on Software Engineering and Methodology 8(1), 49–78 (1999)
de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable interfaces. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 81–105. Springer, Heidelberg (2005)
de Alfaro, L., Henzinger, T.A.: Interface Automata. In: Gruhn, V., Tjoa, A.M. (eds.) Proceedings ESEC/FSE 2001, Vienna, Austria, September 2001, pp. 109–120. ACM Press, New York (2001)
de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Timed Interfaces. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 108–122. Springer, Heidelberg (2002)
de Alfaro, L., Stoelinga, M.: Interfaces: A game-theoretic framework for reasoning about component-based systems. Electronic Notes in Theoretical Computer Science 97, 3–23 (2004)
DeNicola, R., Vaandrager, F.: Three logics for branching bisimulation. Journal of the ACM 42(2), 458–487 (1995)
Fernandez, J.-C.: An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming 13(2–3), 219–236 (1990)
Fisler, K., Vardi, M.Y.: Bisimulation minimization and symbolic model checking. Formal Methods in System Design 21(1), 39–78 (2002)
Habib, M., Paul, C., Viennot, L.: Partition refinement techniques: An interesting algorithmic tool kit. International Journal of Foundations of Computer Science 10(2), 147–170 (1999)
Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
Inverardi, P., Wolf, A.L., Yankelevich, D.: Static checking of system behaviors using derived component assumptions. ACM Transactions on Software Engineering Methodology 9(3), 239–272 (2000)
Kang, I., Lee, I., Kim, Y.-S.: An efficient state space generation for the analysis of real-time systems. IEEE Transactions on Software Engineering 26(5), 453–477 (2000)
Lee, E.A., Xiong, Y.: System-Level Types for Component-Based Design. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 237–253. Springer, Heidelberg (2001)
Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, Vancouver, British Columbia, Canada, August 1987, pp. 137–151 (1987)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Nierstrasz, O.: Regular Types for Active Objects. In: Proceedings OOPSLA 1993, September 1993. ACM SIGPLAN Notices, vol. 28, pp. 1–15 (1993)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing 16(6), 973–989 (1987)
Park, D.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Plasil, F., Visnovsky, S.: Behavior protocols for software components. IEEE Transactions on Software Engineering 28(11), 1056–1076 (2002)
PLT Scheme v372 (2008), http://www.plt-scheme.org
Stirling, C.: Modal and temporal logics for processes. In: Moller, F., Birtwistle, G.M. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 149–237. Springer, Heidelberg (1996)
Szyperski, C.: Component Software: Beyond Object-Oriented Programming, 2nd edn. Addison-Wesley / ACM Press (2002)
ter Beek, M.H., Ellis, C.A., Kleijn, J., Rozenberg, G.: Synchronizations in team automata for groupware systems. Computer Supported Cooperative Work 12(1), 21–69 (2003)
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996)
Yellin, D.M., Strom, R.E.: Protocol specifications and component adaptors. ACM Transactions on Programming Languages and Systems 19(2), 292–333 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lumpe, M., Grunske, L., Schneider, JG. (2008). State Space Reduction Techniques for Component Interfaces. In: Chaudron, M.R.V., Szyperski, C., Reussner, R. (eds) Component-Based Software Engineering. CBSE 2008. Lecture Notes in Computer Science, vol 5282. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87891-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-87891-9_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87890-2
Online ISBN: 978-3-540-87891-9
eBook Packages: Computer ScienceComputer Science (R0)