[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Threaded behavior protocols

  • Original Article
  • Published:
Formal Aspects of Computing

Abstract

Component-based development is a well-established methodology of software development. Nevertheless, some of the benefits that the component based development offers are often neglected. One of them is modeling and subsequent analysis of component behavior, which can help establish correctness guarantees, such as absence of composition errors and safety of component updates. We believe that application of component behavior modeling in practice is limited due to huge differences between the behavior modeling languages (e.g., process algebras) and the common implementation languages (e.g., Java). As a result, many concepts of the implementation languages are either very different or completely missing in the behavior modeling languages. As an example, even though behavior modeling languages are practical for modeling and analysis of various message-based protocols, they are not well suited for modeling current component applications, where thread-based parallelism, lock-based synchronization, and nested method calls are the essential building blocks. With this in mind, we propose a new behavior modeling language for software components, Threaded Behavior Protocols (TBP). At the model level, TBP provides developers with the concepts known from the implementation languages and essential to most component applications. In addition, the theoretical framework of TBP provides a notion of correctness based on absence of communication errors and a refinement relation to verify correctness of hierarchical components. The main asset of TBP formalism is that it links together the notion of threads as used in imperative object oriented languages and the notion of refinement. For instance, this allows reasoning about hierarchical components composed of primitive components implemented in Java without the need of bridging abstractions and simplifications enforced by the modeling languages.

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
£29.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 includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Aldini A, Bernardo M, Corradini F (2010) A process algebraic approach to software architecture design. Springer, Berlin

    Book  MATH  Google Scholar 

  2. Adamek J, Bures T, Jezek P, Kofron J, Mencl V, Parizek P, Plasil F (2006) Component reliability extensions for fractal component model. http://kraken.cs.cas.cz/ft/public/public_index.phtml

  3. de Alfaro L, Henzinger TA (2001) Interface automata. SIGSOFT Softw Eng Notes 26(5): 109–120

    Article  Google Scholar 

  4. de Alfaro L, Henzinger TA (2001) Interface theories for component-based design. In: EMSOFT ’01: Proceedings of the first international workshop on embedded software. London UK, Springer, Berlin, pp 148–165

  5. Allen RJ (1997) A formal approach to software architecture. PhD thesis, CMU

  6. Adamek J, Plasil F (2003) Behavior protocols capturing errors and updates. In: Proceedings of the 2nd international workshop on unanticipated software evolution

  7. Adamek J, Plasil F (2004) Component composition errors and update atomicity: Static analysis. J Softw Maint Evol Res Pract 17(5): 102

    Google Scholar 

  8. Basu A, Bozga M, Sifakis J (2006) Modeling heterogeneous real-time components in bip. In: Proceedings of the fourth IEEE international conference on software engineering and formal methods, Washington, DC, USA. IEEE Computer Society, pp 3–12

  9. Bureš T, Děcký M, Hnětynka P, Kofroň J, Parízek P, Plášil F, Poch T, Šerý O, Tůma P (2008) CoCoME in SOFA. In: The common component modeling example: comparing software component models. Springer, Berlin, pp 388–417

  10. Badger—Verification of component behavior specification. http://d3s.mff.cuni.cz/~sery/badger

  11. Booch G, Rumbaugh J, Jacobson I (2005) Unified modeling language user guide, 2nd edn. Addison-Wesley Object Technology Series. Addison-Wesley Professional

  12. Modelling Contest: Common Component Modelling Example. http://agrausch.informatik.uni-kl.de/CoCoME

  13. Clarke EM, Sharygina N, Sinha N (2005) Program compatibility approaches. In: Boer FS, Bonsangue MM, Graf S, Roever WP (eds) Lecture notes in computer science, vol 4111. Springer, Berlin, pp 243–258

    Google Scholar 

  14. Černá I, Vařeková P, Zimmerova B (2007) Component substitutability via equivalencies of component-interaction automata. In: Proceedings of the workshop on formal aspects of component software (FACS’06). ENTCS, vol 182. Elsevier Science Publishers, pp 39–55, June 2007

  15. Fournet C, Hoare CAR, Rajamani SK, Rehof J (2004) Stuck-free conformance. In: Alur R, Peled D (eds) Proceedings of 16th international conference on computer aided verification (CAV 2004), Boston, MA, USA, July 13–17, 2004 Lecture notes in computer science, vol 3114. Springer, Berlin, pp 242–254

    Google Scholar 

  16. Fournet C, Hoare T, Rajamani SK, Rehof J (2004) Stuck-free conformance theory for ccs. Technical report, Microsoft Research, July 2004

  17. Grimes R, Grimes R Dr (1997) Professional Dcom programming. Wrox Press Ltd., Birmingham

    Google Scholar 

  18. Hoare CAR (1985) Communicating sequential processes. Prentice Hall International (UK) Ltd

  19. Havelund K, Pressburger T (2000) Model checking JAVA programs using JAVA pathfinder. Int J Softw Tools Technol Transf 2(4): 366–381

    Article  MATH  Google Scholar 

  20. Kofron J (2007) Checking software component behavior using behavior protocols and spin. In: Proceedings of applied computing 2007, Seoul, Korea, pp 1513–1517

  21. Larsen KG, Nyman U, Wasowski A (2007) Modal I/O automata for interface and product line theories. In: De Nicola R (eds) ESOP. Lecture notes in computer science, vol 4421. Springer, Berlin, pp 64–79

    Google Scholar 

  22. Leavens, GT, Sitaraman, M (eds) (2000) Foundations of component-based systems. Cambridge University Press, New York

    MATH  Google Scholar 

  23. Magee J, Dulay N, Eisenbach S, Kramer J (1995) Specifying distributed software architectures. In: Fifth European software engineering conference, ESEC ’95, Barcelona

  24. Milner R (1995) Communication and concurrency. Prentice Hall International (UK) Ltd., Hertfordshire

    Google Scholar 

  25. Matena V, Stearns B, Demichiel L (2003) Applying enterprise JavaBeans: component-based development for the J2EE platform. Pearson Education

  26. van Ommering R, van der Linden F, Kramer J, Magee J (2000) The Koala component model for consumer electronics software. Computer 33(3): 78–85

    Article  Google Scholar 

  27. OMG Group (2006) CORBA component model specification. Technical report, OMG Group

  28. Poch T (2010) Towards thread aware component behavior specifications. PhD thesis, Charles University, Prague

  29. Plasil F, Visnovsky S (2002) Behavior protocols for software components. IEEE Trans Softw Eng 28(9)

  30. Roscoe AW (1998) The theory and practice of concurrency. Prentice Hall

  31. Rausch A, Reussner R, Mirandola R, Plasil F (eds) (2008) The common component modeling example: comparing software component models. In: Lecture notes in computer science, vol 5153. Springer, Berlin

Download references

Author information

Authors and Affiliations

  1. Faculty of Mathematics and Physics, Charles University Prague, Malostranské náměstí 25, 118 00, Prague 1, Czech Republic

    Tomáš Poch, Ondřej Šerý, František Plášil & Jan Kofroň

Authors
  1. Tomáš Poch
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ondřej Šerý
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. František Plášil
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jan Kofroň
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jan Kofroň.

Additional information

by M. Broy

This work was partially supported by the Grant Agency of the Czech Republic project P202/11/0312 and by the grant SVV-2011-263312.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Poch, T., Šerý, O., Plášil, F. et al. Threaded behavior protocols. Form Asp Comp 25, 543–572 (2013). https://doi.org/10.1007/s00165-011-0194-3

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-011-0194-3

Keywords

Search

Navigation