Skip to main content
SpringerLink
Log in
Book cover

KORSO: Methods, Languages, and Tools for the Construction of Correct Software pp 317–338Cite as

Traverdi — Transformation and verification of distributed systems

  • Tools
  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1009))

Abstract

Korso at Oldenburg was concerned with distributed systems. Both synthesis of systems from specifications (correctness by construction) and verification of systems (correctness proofs) are part of the approach. The emphasis was on developing prototype tools to support such activities. But also questions of theoretical nature concerning specification formalisms and verification techniques have been tackled.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.K. Annot and R.A.H. van Twist. A novel deadlock free and starvation free packet switching communication processor. In J.W. de Bakker, A.J. Nijman, and P.C. Treleaven, editors, Parallel Architectures and Languages Europe, LNCS 258. Springer, 1987.

    Google Scholar 

  2. R. Baumann. Implementierung eines Kommunkationsalgorithmus und Verifikation des Programms mit modelcheckbasierten Techniken. Master thesis, CvO University Oldenburg, 1994.

    Google Scholar 

  3. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In 5th IEEE Symp. on Logic in Comp. Sc., pages 428–439, 1990.

    Google Scholar 

  4. D. Bjørner et al. A ProCoS project description — ESPRIT BRA 3104. EATCS Bulletin, 39:60–73, 1989.

    Google Scholar 

  5. J. Bohn. Formalizing the transformational design of communicating systems in the theorem prover lambda. Technical report, CvO University Oldenburg, 1993. Presented at HOA'93, Amsterdam.

    Google Scholar 

  6. R.J.R. Back and J. von Wright. Refinement concepts formalized in higher order logic. Formal Aspects of Computing, 2:247–272, 1990.

    Article  Google Scholar 

  7. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. In 10th ACM Symp. on Principles of Programming Languages, pages 117–126, 1983. Also appeared in ACM Transact. on Prog. Lang. and Systems 8:244–263, 1986.

    Google Scholar 

  8. F. Cornelius, H. Hußmann, and M. Löwe. The KORSO Case Study for Software Engineering with Formal Methods: A Medical Information System. In this volume.

    Google Scholar 

  9. R.L. Constable et. al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs, New Jersey, 1986.

    Google Scholar 

  10. W. Damm, H. Hungar, P. Kelb, and R. Schlör. Using graphical specification languages and symbolic model checking in the verification of a production cell. In C. Lewerentz and T. Lindner, editors, Formal development of reactive systems — Case study prodution cell, LNCS 891, pages 131–149. Springer, 1995.

    Google Scholar 

  11. H.D. Ehrich. KORSO reference languages. Concepts and application domains. In this volume.

    Google Scholar 

  12. E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of theoretical computer science. Elsevier, 1990.

    Google Scholar 

  13. M. Fourman and E. Mayger. Integration of formal methods with system design. In Proc. VLSI'91, Edingburgh, 1991.

    Google Scholar 

  14. T. Fuchß, W. Reif, G. Schellhorn, and K. Stenzel. Three selected Case Studies in Verification. In this volume.

    Google Scholar 

  15. M.J.C. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. LNCS 78. Springer, 1979.

    Google Scholar 

  16. M.J.C. Gordon. HOL: A proof generating system for Higher-Order Logic. In G. Birtwistle and P. A. Subramanyam, editors, VLSI Specification, Verification and Synthesis, pages 73–128. Kluwer, 1988.

    Google Scholar 

  17. H. Hungar and G. Rünger. Verification of a communication network — A case study in the use of temporal logic. Technical report, CvO University Oldenburg/University of the Saarland, 1995.

    Google Scholar 

  18. H. Hungar. Combining model checking and theorem proving to verify parallel processes. In C. Courcoubetis, editor, 5th Int. Conf. on Computer Aided Verification, LNCS 697, pages 154–165. Springer, 1993.

    Google Scholar 

  19. NMOS Ltd. OCCAM 2 Reference Manual. Prentice Hall, 1988.

    Google Scholar 

  20. B. Josko. Verifying the correctness of AADL modules using model checking. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise refinement of distributed systems. Models, formalisms, correctness, LNCS 430, pages 386–00. Springer, 1990.

    Google Scholar 

  21. B. Josko. Modular specification and verification of reactive systems. Habilitation Thesis, CvO University Oldenburg, 1993.

    Google Scholar 

  22. V. Jansen, A. Potthoff, W. Thomas, and U. Wermuth. A short guide to the amore system. Technical Report 90-02, RWTH Aachen, Gernamy, 1990.

    Google Scholar 

  23. S. Kleuker. Case study: Stepwise development of a communication processor using trace logic. In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors, Semantics of Specification Languages, Utrecht 1993, pages 252–269. Springer, 1994.

    Google Scholar 

  24. F. Kröger. Temporal logic of programs. EATCS Monograph. Springer, 1987.

    Google Scholar 

  25. C. Lewerentz and T. Lindner, editors. Formal development of reactive systems — Case study production cell. LNCS 891. Springer, 1995.

    Google Scholar 

  26. T. Nipkow and L. C. Paulson. ISABELLE tutorial and user's manual. Technical Report 189, Univ. Cambridge Comp. Lab., 1990.

    Google Scholar 

  27. E.-R. Olderog. Towards a Design Calculus for Communicating Programs. In J.C.M. Baeten and J.F. Groote, editors, 2nd Int. Workshop on Concurrency Theory, LNCS 527, pages 61–77. Springer, 1991. Invited paper.

    Google Scholar 

  28. E.-R. Olderog, S. Rössig, J. Sander, and M. Schenke. ProCoS at Oldenburg: The Interface between Specification Language and OCCAM-like Programming Language. Technical Report 3/92, CvO University Oldenburg, 1992.

    Google Scholar 

  29. L.C. Paulson. Logic and computation, interactive proof with Cambridge LCF. Cambridge Tracts in Theoretical Computer Science 2. Cambridge University Press, 1987.

    Google Scholar 

  30. S. Rössig. A Transformational Approach to the Design of Communicating Systems. PhD thesis, Univ. Oldenburg, 1994. Tech. report 4-94, Fachbereich Informatik, Univ. Oldenburg.

    Google Scholar 

  31. M. Schulte. Spezifikation und Verifikation von kommunizierenden Objekten in einem vermeilten System. Master thesis, CvO University Oldenburg, 1994.

    Google Scholar 

  32. P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In 13th ACM Symp. on Principles of Programming Languages, pages 184–193, 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Universität Oldenburg, Germany

    J. Bohn & H. Hungar

Authors
  1. J. Bohn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. H. Hungar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Manfred Broy Stefan Jähnichen

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Bohn, J., Hungar, H. (1995). Traverdi — Transformation and verification of distributed systems. In: Broy, M., Jähnichen, S. (eds) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Lecture Notes in Computer Science, vol 1009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015470

Download citation

  • DOI: https://doi.org/10.1007/BFb0015470

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60589-8

  • Online ISBN: 978-3-540-47802-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation