Skip to main content

Encoding Context-Sensitivity in Reo into Non-Context-Sensitive Semantic Models

  • Conference paper
Coordination Models and Languages (COORDINATION 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6721))

Included in the following conference series:

Abstract

Reo is a coordination language which can be used to model the interactions among a set of components or services in a compositional manner using connectors. The language concepts of Reo include synchronization, mutual exclusion, data manipulation, memory and context-dependency. Context-dependency facilitates the precise specification of a connector’s possible actions in situations where it would otherwise exhibit nondeterministic behavior. All existing formalizations of context-dependency in Reo are based on extended semantic models that provide constructs for modeling the presence and absence of I/O requests at the ports of a connector.

In this paper, we show that context-dependency in Reo can be encoded in basic semantic models, namely connector coloring with two colors and constraint automata, by introducing additional fictitious ports for Reo’s primitives. Both of these models were considered as not expressive enough to handle context-dependency up to now. We demonstrate the usefulness of our approach by incorporating context-dependency into the constraint automata based Vereofy model checker.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Arbab, F.: Reo: A channel-based coordination model for component composition. Mathematical Structures in Computer Science 14, 329–366 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  2. Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Science of Computer Programming 61(2), 75–113 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  3. Clarke, D., Costa, D., Arbab, F.: Connector colouring I: Synchronisation and context dependency. Science of Computer Programming 66(3), 205–225 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  4. Pourvatan, B., Sirjani, M., Arbab, F., Bonsangue, M.: Decomposition of constraint automata. In: Proceedings of the 7th International Workshop on Formal Aspects of Component Software (FACS 2010). LNCS. Springer, Heidelberg (to appear, 2011)

    Google Scholar 

  5. Costa, D.: Formal Models for Component Connectors. PhD thesis, Vrije Universiteit Amsterdam (2010)

    Google Scholar 

  6. Jongmans, S.S., Krause, C., Arbab, F.: Encoding context-sensitivity in Reo into non-context-sensitive semantic models. Technical Report SEN-1105, Centrum Wiskunde & Informatica (2011)

    Google Scholar 

  7. Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: Formal verification for components and connectors. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 82–101. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Arbab, F., Rutten, J.: A coinductive calculus of component connectors. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 34–55. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Bonsangue, M.M., Clarke, D., Silva, A.: Automata for context-dependent connectors. In: Field, J., Vasconcelos, V.T. (eds.) COORDINATION 2009. LNCS, vol. 5521, pp. 184–203. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. Kokash, N., Krause, C., de Vink, E.P.: Verification of context-dependent channel-based service models. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 21–40. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Kemper, S.: SAT-based verification for timed component connectors. ENTCS 255, 103–118 (2009)

    Google Scholar 

  12. Mousavi, M.R., Sirjani, M., Arbab, F.: Formal semantics and analysis of component connectors in Reo. ENTCS 154(1), 83–99 (2006)

    Google Scholar 

  13. Khosravi, R., Sirjani, M., Asoudeh, N., Sahebi, S., Iravanchi, H.: Modeling and analysis of Reo connectors using Alloy. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 169–183. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2011 IFIP International Federation for Information Processing

About this paper

Cite this paper

Jongmans, SS.T.Q., Krause, C., Arbab, F. (2011). Encoding Context-Sensitivity in Reo into Non-Context-Sensitive Semantic Models. In: De Meuter, W., Roman, GC. (eds) Coordination Models and Languages. COORDINATION 2011. Lecture Notes in Computer Science, vol 6721. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21464-6_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-21464-6_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-21463-9

  • Online ISBN: 978-3-642-21464-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics