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

A UNITY-Based Framework Towards Component Based Systems

  • Conference paper
  • First Online:
Principles of Distributed Systems (OPODIS 2004)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3544))

Included in the following conference series:

  • 698 Accesses

Abstract

Compositionality provides the foundation of software modularity, re-usability and separate verification of software components. One of the known difficulties, when separately verifying components, is producing compositional proofs for progress properties of distributed systems. This paper offers a UNITY-based framework to model distributed applications which are built with a component based approach. The framework enables components to be abstractly specified in terms of contracts. Temporal properties are expressed and proven in the UNITY style. Compositional reasoning about components’ properties, including progress, is supported. The semantical model is simple and intuitive.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems 15(1), 73–132 (1993)

    Article  Google Scholar 

  2. Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)

    Article  Google Scholar 

  3. Back, R.J.R., Von Wright, J.: Refinement calculus, part I: Sequential non-deterministic programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 42–66. Springer, Heidelberg (1990)

    Google Scholar 

  4. Broy, M.: Multi-view modelling of software sytems. In: H.D. Van and Z. Liu, editors, Proceedings of the Workshop on Formal Aspects of Component Software (FACS), Also as UNU/IIST Report no. 284 (2003), available on-line at http://www.iist.unu.edu/newrh/III/1/page.html

  5. Chandy, K., Charpentier, M.: An experiment in program composition and proof. Formal Methods in System Design 20(1), 7–21 (2002)

    Article  Google Scholar 

  6. Chandy, K.M., Misra, J.: Parallel Program Design – A Foundation. Addison-Wesley Publishing Company, Inc., Reading (1988)

    MATH  Google Scholar 

  7. Chandy, K.M., Sanders, B.A.: Reasoning about program composition. Technical Report 96-035, University of Florida (1996)

    Google Scholar 

  8. Chandy, K.M., Sanders, B.A.: Reasoning about program composition. Draft, Presently available via (2000), http://www.cise.ufl.edu/~sanders/pubs

  9. Charpentier, M., Chandy, K.: Theorems about composition. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 167–186. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Collette, P.: Composition of assumption-commitment specifications in a UNITY style. Science of Computer Programming 23, 107–125 (1994)

    Article  MathSciNet  Google Scholar 

  11. Collette, P., Knapp, E.: Logical foundations for compositional verification and development of concurrent programs in UNITY. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 353–367. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  12. Jifeng, H., Zhiming, L., Xiaoshan, L.: A contract-oriented approach to CBP. In: H.D. Van and Z. Liu, editors, Proceedings of the Workshop on Formal Aspects of Component Software (FACS), Also as UNU/IIST Report no. 284 (2003), available on-line at http://www.iist.unu.edu/newrh/III/1/page.html

  13. Kim, S.-K., Carrington, D.: A formal mapping between UML models and object-Z specifications. In: P. Bowen, J., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, p. 2. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  14. Misra, J.: A Discipline of Multiprogramming. Springer, Heidelberg (2001)

    Book  Google Scholar 

  15. Prasetya, I.S.W.B.: Mechanically Supported Design of Self-stabilizing Algorithms. PhD thesis, Inst. of Information and Comp. Science, Utrecht Univ. (1995), Download http://www.cs.uu.nl/library/docs/theses.html

  16. Prasetya, I.S.W.B.: Error in the UNITY substitution rule for subscripted operators. Formal Aspects of Computing 6, 466–470 (1994)

    Article  Google Scholar 

  17. Prasetya, I.S.W.B., Vos, T.E.J., Azurat, A., Swierstra, S.D.: A unity-based framework towards component based systems. Technical Report UU-CS-2003-043, Inst. of Information and Comp. Science, Utrecht Univ. (2003), Download www.cs.uu.nl/staff/wishnu.html

  18. Sanders, B.A.: Eliminating the substitution axiom from UNITY logic. Formal Aspects of Computing 3(2), 189–205 (1991)

    Article  Google Scholar 

  19. Shankar, N.: Lazy compositional verification. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 541–564. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  20. Szyperski, C.: Component Software, Beyond Object-Oriented Programming. Addison-Wesley, Reading (1998)

    Google Scholar 

  21. Udink, R.T.: Program Refinement in UNITY-like Environments. PhD thesis, Inst. of Information and Computer Sci., Utrecht University (1995), Downloadable from http://www.cs.uu.nl

  22. Vos, T.E.J.: UNITY in Diversity: A Stratified Approach to the Verification of Distributed Algorithms. PhD thesis, Inst. of Information and Computer Sci., Utrecht University (2000), Download http://www.cs.uu.nl

  23. Vos, T.E.J., Swierstra, S.D., Prasetya, I.S.W.B.: Yet another program refinement relation. In: International Workshop on Refinement of Critical Systems: Methods, Tools and Experience (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Informatica Instituut, Universiteit Utrecht, Japan

    I. S. W. B. Prasetya, A. Azurat & S. D. Swierstra

  2. Instituto Tecnológico de Informática, Universidad Politécnica de Valencia, Japan

    T. E. J. Vos

Authors
  1. I. S. W. B. Prasetya
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. T. E. J. Vos
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. A. Azurat
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. S. D. Swierstra
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Japan Science Technology and Agency, CREST, Japan

    Teruo Higashino

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Prasetya, I.S.W.B., Vos, T.E.J., Azurat, A., Swierstra, S.D. (2005). A UNITY-Based Framework Towards Component Based Systems. In: Higashino, T. (eds) Principles of Distributed Systems. OPODIS 2004. Lecture Notes in Computer Science, vol 3544. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11516798_4

Download citation

  • DOI: https://doi.org/10.1007/11516798_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-27324-0

  • Online ISBN: 978-3-540-31584-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation