Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Expressiveness of component-based frameworks: a study of the expressiveness of BIP

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

A Correction to this article was published on 16 September 2019

This article has been updated

Abstract

We extend our previous algebraic formalisation of the notion of component-based framework in order to formally define two forms—strong and weak—of the notion of full expressiveness and study their properties. Our earlier result shows that the BIP (Behaviour–Interaction–Priority) framework does not possess the strong full expressiveness with respect to the sub-class of GSOS rules used for the definition of its semantics. In this paper, we refine this comparison detailing the expressiveness of classical BIP, Offer BIP and a number of variations obtained either by relaxing the constraints in the definition of priority models or by introducing positive premises into the rule formats used to define the operational semantics of composition operators. The obtained results are organised into an expressiveness hierarchy.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10

Similar content being viewed by others

Change history

  • 16 September 2019

    The Original Article has been funded.

Notes

  1. Two component-based frameworks with distinct semantic domains can be compared by mapping to a common behaviour type and taking an appropriate equivalence relation consistent with those of the frameworks. However, this essentially boils down to a substitution of the semantic domains, i.e. considering a different pair of frameworks.

  2. The notion of uniform flattening is stronger than that of flattening introduced in [3] in that it requires the operator \(o_3\) to be the same, independently of the choice of \(C_1,\dots ,C_n\).

  3. As opposed to a (non-strict) partial order, which is a reflexive, antisymmetric and transitive relation, a strict partial order is an irreflexive and transitive (hence also antisymmetric) one.

  4. To simplify the notation we use the juxtaposition \(\gamma = \{p, q, r, qr\}\) instead of the set notation \(\gamma = \bigl \{\{p\}, \{q\}, \{r\}, \{q, r\} \bigr \}\) for interactions. Similarly, we directly write \(\pi = \{q\prec r\}\) instead of \(\pi = \{(q, r)\}\).

  5. We denote by \(r \cdot s\) the set of two singleton interactions r and s, as opposed to rs, which denotes one interaction consisting of the two ports.

  6. As in Note 1, we omit the indices on \({\uparrow }{}\), whenever they are clear from the context.

  7. We have only introduced the term “AcBSOS” in the present paper. In [3], we speak of composition operators defined by sets of SOS rules.

  8. The rule \(S_a\) might be removed from the operator o as redundant, however this would imply the existence of another rule with the same conclusion and whereof premises would also be satisfied in the state q.

References

  1. Attie, P., Baranov, E., Bliudze, S., Jaber, M., Sifakis, J.: A general framework for architecture composability. In: Giannakopoulou, D., Salaün, G. (eds.) 12th International Conference on Software Engineering and Formal Methods (SEFM 2014), no. 8702 in LNCS, pp. 128–143. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10431-7_10

    Chapter  Google Scholar 

  2. Attie, P., Baranov, E., Bliudze, S., Jaber, M., Sifakis, J.: A general framework for architecture composability. Form. Asp. Comput. 18(2), 207–231 (2016). https://doi.org/10.1007/s00165-015-0349-8. (Open access)

    Article  MathSciNet  MATH  Google Scholar 

  3. Baranov, E., Bliudze, S.: Offer semantics: achieving compositionality, flattening and full expressiveness for the glue operators in BIP. Sci. Comput. Program. 109, 2–35 (2015). https://doi.org/10.1016/j.scico.2015.05.011. (Selected Papers of the 6th Interaction and Concurrency Experience (ICE 2013))

    Article  Google Scholar 

  4. Baranov, E., Bliudze, S.: A note on the expressiveness of BIP. In: Proceedings of the Combined 23rd International Workshop on Expressiveness in Concurrency and 13th Workshop on Structural Operational Semantics, EXPRESS/SOS 2016, EPTCS, vol. 222, pp. 1–14 (2016). https://doi.org/10.4204/EPTCS.222.1

  5. Basten, T.: Branching bisimilarity is an equivalence indeed!. Inf. Process. Lett. 58(3), 141–147 (1996)

    Article  MathSciNet  Google Scholar 

  6. Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011). https://doi.org/10.1109/MS.2011.27

    Article  Google Scholar 

  7. Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM06), pp. 3–12 (2006). https://doi.org/10.1109/SEFM.2006.27. Invited talk

  8. Bliudze, S., Mavridou, A., Szymanek, R., Zolotukhina, A.: Exogenous coordination of concurrent software components with JavaBIP. Softw. Pract. Exp. 47(11), 1801–1836 (2017). https://doi.org/10.1002/spe.2495

    Article  Google Scholar 

  9. Bliudze, S., Sifakis, J.: The algebra of connectors—structuring interaction in BIP. In: Proceedings of the EMSOFT’07, pp. 11–20. ACM SigBED (2007). https://doi.org/10.1145/1289927.1289935

  10. 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, Cham (2008). https://doi.org/10.1007/978-3-540-85361-9_39

    Chapter  Google Scholar 

  11. Bliudze, S., Sifakis, J.: Causal semantics for the algebra of connectors. Form. Methods Syst. Des. 36(2), 167–194 (2010). https://doi.org/10.1007/s10703-010-0091-z

    Article  MATH  Google Scholar 

  12. Bliudze, S., Sifakis, J.: Synthesizing glue operators from glue constraints for the construction of component-based systems. In: Apel, S., Jackson, E. (eds.) 10th International Conference on Software Composition, LNCS, vol. 6708, pp. 51–67. Springer, Cham (2011). https://doi.org/10.1007/978-3-642-22045-6_4

    Chapter  Google Scholar 

  13. Bliudze, S., Sifakis, J., Bozga, M.D., Jaber, M.: Architecture internalisation in BIP. In: Proceedings of the 17th International ACM Sigsoft Symposium on Component-Based Software Engineering, CBSE’14, pp. 169–178. ACM, New York, NY, USA (2014). https://doi.org/10.1145/2602458.2602477

  14. Bloom, B.: Ready simulation, bisimulation, and the semantics of CCS-like languages. Ph.D. thesis, Massachusetts Institute of Technology (1989)

  15. Boulanger, J.L., et al.: SCADE: Language and Applications, 1st edn. Wiley-IEEE Press, New York (2015)

    Google Scholar 

  16. Bruni, R., Lanese, I., Montanari, U.: A basic algebra of stateless connectors. Theor. Comput. Sci. 366(1), 98–120 (2006). https://doi.org/10.1016/j.tcs.2006.07.005

    Article  MathSciNet  MATH  Google Scholar 

  17. Bruni, R., Melgratti, H., Montanari, U.: Connector algebras, petri nets, and bip. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) Perspectives of Systems Informatics, Lecture Notes in Computer Science, vol. 7162, pp. 19–38. Springer Berlin Heidelberg, Berlin (2012). https://doi.org/10.1007/978-3-642-29709-0_2

    Chapter  Google Scholar 

  18. Dezani-Ciancaglini, M., de’Liguoro, U.: Sessions and session types: an overview. In: Laneve, C., Su, J. (eds.) Web Services and Formal Methods: 6th International Workshop, WS-FM 2009, no. 6194 in Lecture Notes in Computer Science, pp. 1–28. Springer Berlin Heidelberg, Berlin (2010). https://doi.org/10.1007/978-3-642-14458-5_1

    Chapter  Google Scholar 

  19. Dokter, K., Jongmans, S.T.Q., Arbab, F., Bliudze, S.: Relating BIP and reo. In: Knight, S., Lanese, I., Lluch-Lafuente, A., Vieira, H.T. (eds.) Proceedings 8th Interaction and Concurrency Experience, ICE 2015, Grenoble, France, 4-5th June 2015., EPTCS, vol. 189, pp. 3–20 (2015). https://doi.org/10.4204/EPTCS.189.3

  20. Eker, J., Janneck, J., Lee, E., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity: the Ptolemy approach. Proc. IEEE 91(1), 127–144 (2003). https://doi.org/10.1109/JPROC.2002.805829

    Article  Google Scholar 

  21. Felleisen, M.: On the expressive power of programming languages. In: 3rd European Symposium on Programming (ESOP’90), LNCS, vol. 432, pp. 134–151. Springer (1990). https://doi.org/10.1007/3-540-52592-0_60

  22. Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031–1053 (2010). https://doi.org/10.1016/j.ic.2010.05.002

    Article  MathSciNet  MATH  Google Scholar 

  23. Gößler, G., Sifakis, J.: Priority systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and Objects, Second International Symposium, FMCO 2003, Leiden, The Netherlands, November 4–7, 2003, Revised Lectures, Lecture Notes in Computer Science, vol. 3188, pp. 314–329. Springer, Cham (2003). https://doi.org/10.1007/978-3-540-30101-1_15

    Chapter  Google Scholar 

  24. Gössler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Program. 55(1–3), 161–183 (2005). https://doi.org/10.1016/j.scico.2004.05.014. (Formal Methods for Components and Objects: Pragmatic aspects and applications)

    Article  MathSciNet  MATH  Google Scholar 

  25. Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) Programming Languages and Systems, LNCS, vol. 1381, pp. 122–138. Springer Berlin Heidelberg, Berlin (1998). https://doi.org/10.1007/BFb0053567

    Chapter  Google Scholar 

  26. Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deniélou, P.M., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H.T., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1–3:36 (2016). https://doi.org/10.1145/2873052

    Article  Google Scholar 

  27. Mavridou, A., Stachtiari, E., Bliudze, S., Ivanov, A., Katsaros, P., Sifakis, J.: Architecture-based design: A satellite on-board software case study. In: 13th International Conference on Formal Aspects of Component Software (FACS 2016), Lecture Notes in Computer Science, vol. 10231, pp. 260–279 (2016). https://doi.org/10.1007/978-3-319-57666-4_16

  28. Milner, R.: Communication and Concurrency. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River (1989)

    Google Scholar 

  29. Mousavi, M., Phillips, I., Reniers, M.A., Ulidowski, I.: Semantics and expressiveness of ordered SOS. Inf. Comput. 207, 85–119 (2009). https://doi.org/10.1016/j.ic.2007.11.008

    Article  MathSciNet  MATH  Google Scholar 

  30. Mousavi, M., Reniers, M.A., Groote, J.F.: SOS formats and meta-theory: 20 years after. Theor. Comput. Sci. 373(3), 238–272 (2007). https://doi.org/10.1016/j.tcs.2006.12.019

    Article  MathSciNet  MATH  Google Scholar 

  31. Park, D.M.R.: Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science, pp. 167–183 (1981). https://doi.org/10.1007/BFb0017309

  32. Plotkin, G.D.: A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, University of Aarhus (1981). http://citeseer.ist.psu.edu/plotkin81structural.html

  33. Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3–80 (2000). https://doi.org/10.1016/S0304-3975(00)00056-6

    Article  MathSciNet  MATH  Google Scholar 

  34. Sifakis, J.: A framework for component-based construction. In: 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM05), pp. 293–300 (2005). https://doi.org/10.1109/SEFM.2005.3. Keynote talk

  35. Sobocinski, P.: A non-interleaving process calculus for multi-party synchronisation. In: Bonchi, F., Grohmann, D., Spoletini, P., Tuosto, E. (eds.) ICE, EPTCS, vol. 12, pp. 87–98 (2009). https://doi.org/10.4204/EPTCS.12.6

  36. Stachtiari, E., Mavridou, A., Katsaros, P., Bliudze, S., Sifakis, J.: Early validation of system requirements and design through correctness-by-construction. J. Syst. Softw. 145, 52–78 (2018). https://doi.org/10.1016/j.jss.2018.07.053

    Article  Google Scholar 

  37. van Glabbeek, R.J.: Musings on encodings and expressiveness. In: Luttik, B., Reniers, M.A. (eds.) Proceedings Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, EXPRESS/SOS 2012, Newcastle upon Tyne, UK, September 3, 2012., EPTCS, vol. 89, pp. 81–98 (2012). https://doi.org/10.4204/EPTCS.89.7

Download references

Author information

Authors and Affiliations

  1. Université catholique de Louvain, Place de l’Université 1, 1348, Ottignies-Louvain-la-Neuve, Belgium

    Eduard Baranov

  2. INRIA Lille – Nord Europe, 40 avenue Halley, 59650, Villeneuve d’Ascq, France

    Simon Bliudze

Authors
  1. Eduard Baranov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Simon Bliudze
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Simon Bliudze.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Baranov, E., Bliudze, S. Expressiveness of component-based frameworks: a study of the expressiveness of BIP. Acta Informatica 57, 761–800 (2020). https://doi.org/10.1007/s00236-019-00337-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-019-00337-7

Search

Navigation