Traverdi — Transformation and verification of distributed systems

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