nach oben

Acta Informatica

Erschienen in:

01.04.2015 | Original Article

Moving from interface theories to assembly theories

verfasst von: Rolf Hennicker, Alexander Knapp

Erschienen in: Acta Informatica | Ausgabe 2-3/2015

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We show how interface theories supporting pairwise component analysis can be extended in a generic way to a multi-component environment. This leads to the abstract framework of an assembly theory which captures notions of assembly refinement and communication-safety in assemblies of interacting components. An assembly theory supports also encapsulation of assemblies into interfaces and hence hierarchical constructions. We propose general rules that should be satisfied by any concrete assembly theory, like compositional construction and refinement of communication-safe assemblies. We discuss general procedures how to construct an assembly theory on top of a given interface theory such that (some of) the laws of an assembly theory are automatically guaranteed by the properties of an underlying interface theory. As a proof of concept we consider two instances of our approach. The first one starts from the (optimistic) interface theory of interface automata proposed by de Alfaro and Henzinger, and the second one from the (pessimistic) interface theory of modal I/O-interfaces. In the latter case, we propose a new notion of modal assembly refinement which has all the required properties, in particular it preserves modal communication-safety of assemblies. A small case-study illustrates how our concepts can be methodologically applied.

Vorheriger Artikel On constructibility and unconstructibility of LTS operators from other LTS operators

Nächster Artikel Refinement checking on parametric modal transition systems

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

It is assumed that the composition of compatible interfaces is defined.

Commutativity means that for all \(F, G \in {\mathcal {F}}\), if \(F, G\) are composable then \(G, F\) are composable and \(F \mathbin {\otimes }G = G \mathbin {\otimes }F\), i.e., \(F \mathbin {\otimes }G\) and \(G \mathbin {\otimes }F\) are set-theoretically equal.

Associativity means that for all \(F, G, H \in {\mathcal {F}}\), if \(F, G\) and \(H\) are pairwise composable then \((F \mathbin {\otimes }G) \mathbin {\otimes }H\) and \(F \mathbin {\otimes }(G \mathbin {\otimes }H)\) are defined and \((F \mathbin {\otimes }G) \mathbin {\otimes }H = F \mathbin {\otimes }(G \mathbin {\otimes }H)\).

In our considerations an environment for an interface \(F\) is just another interface, say \(E\), which is composable with \(F\). We do not impose any closedness assumption on \(F \mathbin {\otimes }E\), since this is not possible in the abstract framework of an interface theory. This could be done, however, in the framework of “labelled interface theories” considered in [5].

More precisely, we consider interface automata as representatives of their isomorphism classes w.r.t. bijections on states.

We refer to the different parts of modal interfaces by subscripting, such that, e.g., \(S_{M_1}\) denotes the states of the modal interface \(M_1\).

More precisely, we consider modal interfaces as representatives of their isomorphism classes w.r.t. bijections on states.

Hence for each \(A \in {\mathcal {A}}\), any non-empty sub-family of \(A\) is also in \({\mathcal {A}}\).

The modal interface \(M\) is considered as a MIO with no communication labels and the same holds for \(M_j\) in the subsequent case.

Recall that \(C_{E_j}\) are the communication labels of \(E_j\) and \((O_{E_j} {\setminus } I_{M_j})\) the output labels of \(E_j\) unshared with the input labels of \(M_j\), i.e., not used for communication between \(E_j\) and \(M_j\). The silent must-transitions of \(E_j\) are anyway subsumed in the notation \({\mathrel {{\overset{\widehat{X_j}}{\rightarrow }\!\!\!{\genfrac{}{}{0.0pt}1{}{E_j}}}}}\); see Sect. 3.2.

In order to prove the equivalence one has to check that \( pack ^{{\mathrm {mi}}}(\mathsf{CashDeskAssembly}) \mathrel {\preccurlyeq ^{\mathrm {mi}}} min ( pack ^{{\mathrm {mi}}}(\mathsf{CashDeskAssembly}))\) and vice versa. Both directions have been verified with the MIO-Workbench [6]. We believe that the interface \( min ( pack ^{{\mathrm {mi}}}(\mathsf{CashDeskAssembly}))\) is indeed minimal. Whether minimal behaviours for modal interfaces always exist and how they can be computed is an open question.

Adámek, J., Plasil, F.: Component composition errors and update atomicity: static analysis. J. Softw. Maint. 17(5), 363–377 (2005)CrossRef

Aldini, A., Bernardo, M., Corradini, F.: A Process Algebraic Approach to Software Architecture Design. Springer, Heidelberg (2010)CrossRefMATH

Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Trans. Softw. Eng. Methodol. 6(3), 213–249 (1997)CrossRef

Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Proceedings of 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM’06), pp. 3–12. (2006)

Bauer, S.S., Hennicker, R., Legay, A.: A meta-theory for component interfaces with contracts on ports. Sci. Comput. Program. 91, 70–89 (2014)CrossRef

Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO Workbench. In: Esparza, J., Majumdar, R. (eds.) Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’10), volume 6015 of Lecture Notes in Computer Science, pp. 175–189. Springer, Heidelberg (2010)

Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Rev. Lect. 6th Int. Symp. Formal Methods for Components and Objects (FMCO’07), volume 5382 of Lecture Notes in Computer Science, pp. 200–225. Springer, Heidelberg (2008)

Bernardo, M., Ciancarini, P., Donatiello, L.: Architecting families of software systems with process algebras. ACM Trans. Softw. Eng. Methodol. 11(4), 386–426 (2002)CrossRef

Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)CrossRefMATHMathSciNet

10.

Bujtor, F., Vogler, W.: Error-pruning in interface automata. In: Geffert, V., Preneel, B., Rovan, B., Stuller, J., Tjoa, A.M. (eds.) Proceedings of 40th International Conference in Current Trends in Theory and Practice of Computer Science (SOFSEM’14), volume 8327 of Lecture Notes in Computer Science, pp. 162–173. Springer, Heidelberg (2014)

11.

Carmona, J., Cortadella, J.: Input/output compatibility of reactive systems. In: Aagaard, M., O’Leary, J.W. (eds.) Proceedings of 4th International Conference Formal Methods in Computer-Aided Design (FMCAD’02), volume 2517 of Lecture Notes in Computer Science, pp. 360–377. Springer, Heidelberg (2002)

12.

Carmona, J., Kleijn, J.: Compatibility in a multi-component environment. Theor. Comput. Sci. 484, 1–15 (2013)CrossRefMATHMathSciNet

13.

Cerná, I., Vareková, P., Zimmerova, B.: Component substitutability via equivalences of component-interaction automata. In: Proceedings of 3rd Int. Wsh. Formal Aspects of Component Systems (FACS’06), volume 182 of Electr. Notes Theor. Comput. Sci., pp. 39–55. Elsevier, (2007)

14.

de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of 9th ACM SIGSOFT Annual Symposium of Foundations of Software Engineering (FSE’01), pp. 109–120. ACM, (2001)

15.

de Alfaro, L., Henzinger, T.A.: Interface theories for component-based design. In: Henzinger, T.A., Kirsch, C.M. (eds). Proceedings of 1st Int. Wsh. Embedded Software (EMSOFT’01), vol 2211 Lecture Notes in Computer Science. Springer, pp. 148–165. (2001)

16.

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, Volume 195 of NATO Science Series: Mathematics, Physics, and Chemistry, pp. 83–104. Springer, Heidelberg (2005)CrossRef

17.

Gößler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Program. 55(1–3), 161–183 (2005)CrossRefMATH

18.

Haddad, S., Hennicker, R., Møller, M.H.: Specification of asynchronous component systems with Modal I/O-petri nets. In: Proceedings of 8th Int. Symp. Trustworthy Global Computing (TGC’13), vol 8358 of Lect. Notes Comp. Sci. Springer, 2014

19.

Hennicker, R., Janisch, S., Knapp, A.: On the observable behaviour of composite components. In: Canal, C., Pasareanu, C. (eds.) Proceedings of 5th Int. Wsh. Formal Aspects of Component Systems (FACS’08), vol. 260 of Electr. Notes Theor. Comput. Sci, pp. 125–153. Elsevier, Amsterdam (2010)

20.

Hennicker, R., Knapp, A.: Modal interface theories for communication-safe component assemblies. In: Cerone, A., Pihlajasaari, P. (eds.) Proceedings of 8th Int. Coll. Theoretical Aspects of Computing (ICTAC’11), vol. 6916 of Lecture Notes in Computer Science, pp. 135–153. Springer, Heidelberg (2011)

21.

Hennicker, R., Knapp, A., Wirsing, M.: Assembly theories for communication-safe component systems. In: Bensalem, S., Lakhneck, Y., Legay, A. (eds.) Proceedings of ETAPS Wsh. from Programs to Systems (FPS’14). In Honor of Joseph Sifakis., vol. 8415 of Lecture Notes in Computer Science, pp. 145–160. Springer, Heidelberg (2014)

22.

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) Proceedings of 35th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL’08), pp. 273–284. ACM, New York (2008)

23.

Hüttel, H., Larsen, K.G.: The use of static constructs in a modal process logic. In: Meyer, A.R., Taitslin, M.A. (eds), Proceedings of Symp. Logical Foundations of Computer Science (Logic at Botik ’89), vol. 363 of Lecture Notes in Computer Science, pp. 163–180. (1989)

24.

Larsen, K.G., Nyman, U., Wasowski, A.: Modal I/O automata for interface and product line theories. In: Nicola, R.D. (ed.) Proceedings of 16th Europ. Symp. Programming (ESOP’07), vol 4421 of Lecture Notes in Computer Science, pp. 64–79. Springer, Heidelberg (2007)

25.

Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of 3rd Ann. IEEE Symp. Logic in Computer Science (LICS’88), pp. 203–210. IEEE, (1988)

26.

Liu, Z., Parnas, D.L., Trancón y Widemann, B.: Documenting and verifying systems assembled from components. Frontiers Comp. Sci. China 4(2), 151–161 (2010)CrossRefMATH

27.

Lüttgen, G., Vogler, W.: Modal interface automata. Logical Meth. Comp. Sci. 9(3) (2013). doi:10.2168/LMCS-9(3:4)2013

28.

Lüttgen, G., Vogler, W.: Richer interface automata with optimistic and pessimistic compatibility. In: Schneider, S., Treharne, H. (eds). Proceedings of 13th Int. Wsh. Automated Verification of Critical Systems (AVOCS’13), vol 66 of Electr. Comm. EASST, (2013)

29.

Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundam. Inform. 108(1–2), 119–149 (2011)MATHMathSciNet

30.

Rausch, A., Reussner, R., Mirandola, R., Plášil, F. (eds.): The Common Component Modeling Example: Comparing Software Component Models, volume 5153 of Lect. Notes Comp. Sci. Springer, Heidelberg (2008)

31.

Tripakis, S., Lickly, B., Henzinger, T.A., Lee, E.A.: A theory of synchronous relational interfaces. ACM Trans. Program. Lang. Syst. 33(4), 14 (2011)

Titel: Moving from interface theories to assembly theories
verfasst von: Rolf Hennicker
Alexander Knapp
Publikationsdatum: 01.04.2015
Verlag: Springer Berlin Heidelberg
Erschienen in: Acta Informatica / Ausgabe 2-3/2015
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI: https://doi.org/10.1007/s00236-015-0220-7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2-3/2015

On constructibility and unconstructibility of LTS operators from other LTS operators

Modal algebra and Petri nets

Refinement checking on parametric modal transition systems

Observable liveness of Petri nets

CCS: It’s not fair!

State space axioms for T-systems

Premium Partner