Advertisement

Assembly Theories for Communication-Safe Component Systems

  • Rolf Hennicker
  • Alexander Knapp
  • Martin Wirsing
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8415)

Abstract

We propose an abstract notion of an assembly theory that formalizes rudimentary requirements for systems of interacting components. Among these are a composition operator for assemblies, a communication”=safety predicate to express the absence of communication errors, a refinement relation for assemblies, and a packing operation to encapsulate assemblies into components thus allowing hierarchical system constructions. We establish laws that must be satisfied by any concrete assembly theory in order to support compositionality of communication”=safety, of encapsulation and of refinement. Moreover, refinement must behave well w.r.t. communication”=safety and encapsulation. As a concrete instance we investigate a modal assembly theory using modal I/O”=interfaces (MIOs) for modeling observable component behaviors and MIOs with possible error states (indicating communication errors) for modeling assembly behaviors. We show that all rules of an assembly theory are satisfied by modal assemblies, in particular the compositionality requirements hold.

Keywords

Error State Composition Operator Modal Interface Modal Assembly Output Label 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Adámek, J., Plasil, F.: Component composition errors and update atomicity: Static analysis. J. Softw. Maint. 17(5), 363–377 (2005)CrossRefGoogle Scholar
  2. 2.
    ASCENS project, http://www.ascens-ist.eu
  3. 3.
    Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Proc. 4th IEEE Int. Conf. Software Engineering and Formal Methods (SEFM 2006), pp. 3–12. IEEE (2006)Google Scholar
  4. 4.
    Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175–189. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: D-Finder 2: Towards efficient correctness of incremental design. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 453–458. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Bozga, M., Jaber, M., Maris, N., Sifakis, J.: Modeling dynamic architectures using Dy-BIP. In: Gschwind, T., De Paoli, F., Gruhn, V., Book, M. (eds.) SC 2012. LNCS, vol. 7306, pp. 1–16. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  7. 7.
    Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Carmona, J., Kleijn, J.: Compatibility in a multi-component environment. Theor. Comput. Sci. 484, 1–15 (2013)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Cerná, I., Vareková, P., Zimmerova, B.: Component substitutability via equivalencies of component-interaction automata. Electr. Notes Theor. Comput. Sci. 182, 39–55 (2007)CrossRefGoogle Scholar
  10. 10.
    de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proc. 9th ACM SIGSOFT Ann. Symp. Foundations of Software Engineering (FSE 2001), pp. 109–120 (2001)Google Scholar
  11. 11.
    de Alfaro, L., Henzinger, T.A.: Interface theories for component-based design. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 148–165. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  12. 12.
    de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Broy, M., Grünbauer, J., Harel, D., Hoare, C.A.R. (eds.) Engineering Theories of Software-intensive Systems. NATO Science Series: Mathematics, Physics, and Chemistry, vol. 195, pp. 83–104. Springer (2005)Google Scholar
  13. 13.
    Gößler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Program. 55(1-3), 161–183 (2005)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Haddad, S., Hennicker, R., Møller, M.H.: Specification of asynchronous component systems with Modal I/O-Petri nets. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358. Springer (to appear, 2014)Google Scholar
  15. 15.
    Hennicker, R., Knapp, A.: Modal interface theories for communication-safe component assemblies. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 135–153. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  16. 16.
    Hüttel, H., Larsen, K.G.: The use of static constructs in a modal process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 163–180. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  17. 17.
    Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: Proc. 3rd Ann. IEEE Symp. Logic in Computer Science (LICS 1988), pp. 203–210. IEEE (1988)Google Scholar
  19. 19.
    Rausch, A., Reussner, R., Mirandola, R., Plášil, F. (eds.): The Common Component Modeling Example. LNCS, vol. 5153. Springer, Heidelberg (2008)Google Scholar
  20. 20.
    Sifakis, J.: Rigorous system design. Foundations and Trends in Electronic Design Automation 6(4), 293–362 (2013)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Rolf Hennicker
    • 1
  • Alexander Knapp
    • 2
  • Martin Wirsing
    • 1
  1. 1.Ludwig-Maximilians-Universität MünchenGermany
  2. 2.Universität AugsburgGermany

Personalised recommendations