Skip to main content
SpringerLink
Log in

Composing Constraint Automata, State-by-State

  • Conference paper
  • First Online:
Formal Aspects of Component Software (FACS 2015)

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

Included in the following conference series:

Abstract

The grand composition of n automata may have a number of states/transitions exponential in n. When it does, it seems not unreasonable for the computation of that grand composition to require exponentially many resources (time, space, or both). Conversely, if the grand composition of n automata has a number of states/transitions only linear in n, we may reasonably expect the computation of that grand composition to also require only linearly many resources.

Recently and problematically, we saw cases of linearly-sized grand compositions whose computation required exponentially many resources. We encountered these cases in the context of Reo (a graphical language for coordinating components in component-based software), constraint automata (a general formalism for modeling systems’ behavior), and our compiler for Reo based on constraint automata. Combined with earlier research on constraint automata verification, these ingredients facilitate a correctness-by-construction approach to component-based software engineering—one of the hallmarks in Sifakis’ “rigorous system design”. To achieve that ambitious goal, however, we need to solve the previously stated problem. In this paper we present such a solution.

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

Access this chapter

Log in via an institution
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 EPUB and 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

Notes

  1. 1.

    We recollected the data shown in Fig. 4 specifically for this paper, but we made our initial observations based on our previous data [11].

References

  1. Arbab, F.: Reo: a channel-based coordination model for component composition. MSCS 14(3), 329–366 (2004)

    MATH  MathSciNet  Google Scholar 

  2. Arbab, F.: Puff, the magic protocol. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 169–206. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  3. Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: A uniform framework for modeling and verifying components and connectors. In: Field, J., Vasconcelos, V.T. (eds.) COORDINATION 2009. LNCS, vol. 5521, pp. 247–267. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Baier, C., Blechmann, T., Klein, J., Klüppelholz, S., Leister, W.: Design and verification of systems with exogenous coordination using Vereofy. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol. 6416, pp. 97–111. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  6. Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995, pp. 3–18 (1995)

    Google Scholar 

  7. Ghassemi, F., Tasharofi, S., Sirjani, M.: Automated mapping of Reo circuits to constraint automata. In: FSEN 2005, ENTCS, vol. 159, pp. 99–115 (2006)

    Google Scholar 

  8. Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages, and Computation (2001)

    Google Scholar 

  9. Jongmans, S.S., Arbab, F.: Overview of thirty semantic formalisms for Reo. Sci. Ann. Comput. Sci. 22(1), 201–251 (2012)

    MathSciNet  Google Scholar 

  10. Jongmans, S.S., Arbab, F.: Toward sequentializing overparallelized protocol code. In: ICE 2014, EPTCS, vol. 166, pp. 38–44 (2014)

    Google Scholar 

  11. Jongmans, S.S., Arbab, F.: Can high throughput atone for high latency in compiler-generated protocol code? In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 238–258. Springer, Heidelberg (2015)

    Google Scholar 

  12. Jongmans, S.S., Kappé, T., Arbab, F.: Composing constraint automata, state-by-state (Technical report). Technical report FM-1506, CWI (2015)

    Google Scholar 

  13. Klein, J., Klüppelholz, S., Stam, A., Baier, C.: Hierarchical modeling and formal verification. An industrial case study using Reo and Vereofy. In: Salaün, G., Schätz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 228–243. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Pourvatan, B., Rouhy, N.: An alternative algorithm for constraint automata product. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 412–422. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Proença, J.: Synchronous coordination of distributed components. Ph.D. thesis, Leiden University (2011)

    Google Scholar 

  16. Sifakis, J.: Rigorous system design. In: PODC 2014, p. 292 (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Open University of the Netherlands, Heerlen, The Netherlands

    Sung-Shik T. Q. Jongmans

  2. Institute for Computing and Information Sciences, Radboud University Nijmegen, Nijmegen, The Netherlands

    Sung-Shik T. Q. Jongmans

  3. Centrum Wiskunde and Informatica, Amsterdam, The Netherlands

    Sung-Shik T. Q. Jongmans & Farhad Arbab

  4. Leiden Institute of Advanced Computer Science, Leiden University, Leiden, The Netherlands

    Tobias Kappé & Farhad Arbab

Authors
  1. Sung-Shik T. Q. Jongmans
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tobias Kappé
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Farhad Arbab
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sung-Shik T. Q. Jongmans .

Editor information

Editors and Affiliations

  1. Universidade Federal Fluminense, Niterói, Brazil

    Christiano Braga

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Jongmans, SS.T.Q., Kappé, T., Arbab, F. (2016). Composing Constraint Automata, State-by-State. In: Braga, C., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2015. Lecture Notes in Computer Science(), vol 9539. Springer, Cham. https://doi.org/10.1007/978-3-319-28934-2_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-28934-2_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-28933-5

  • Online ISBN: 978-3-319-28934-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation