Combining Specification Techniques for Processes, Data and Time

1. J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and Wang Yi. Uppaal-a tool suite for automatic verification of real-time systems. In R. Alur, T.A. Henzinger, and E.D. Sonntag, editors, Hybrid Systems III-Verification and Control, volume 1066 of LNCS, pages 232–243. Springer, 1997.

   Google Scholar 

2. G. Booch, J. Rumbaugh, and I. Jacobson. The Unified Modeling Language User Guide. Object Technology Series. Addison Wesley, 1999.

   Google Scholar 

3. J. Davies and S. Schneider. A brief history of Timed CSP. Theoretical Computer Science, 138:243–271, 1995.

   Article  MATH  MathSciNet  Google Scholar 

4. H. Dierks, A. Fehnker, A. Mader, and F.W. Vaandrager. Operational and Logical Semantics for Polling Real-Time Systems. In A.P. Ravn and H. Rischel, editors, FTRTFT’98, volume 1486 of LNCS, pages 29–40. Springer, 1998.

   Google Scholar 

5. H. Dierks and J. Tapken. Modelling and verifying of a ‘cash point service’ using MOBY/PLC. Formal Aspects of Computing, 12:220–221, 2000.

   Article  Google Scholar 

6. H. Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata. Theoretical Computer Science, 253(1):61–93, 2001.

   Article  MATH  MathSciNet  Google Scholar 

7. C.J. Fidge, I.J. Hayes, A.P. Martin, and A.K. Wabenhorst. A set-theoretic model for real-time specification and reasoning. In J. Jeuring, editor, Mathematics of Program Construction, volume 1422 of LNCS, pages 188–206. Springer, 1998.

   Chapter  Google Scholar 

8. C. Fischer and H. Wehrheim. Model-checking CSP-OZ specifications with FDR. In K. Araki, A. Galloway, and K. Taguchi, editors, Integrated Formal Methods, pages 315–334. Springer, 1999.

   Google Scholar 

9. C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS’97), volume 2, pages 423–438. Chapman & Hall, 1997.

   Google Scholar 

10. C. Fischer. Combination and Implementation of Processes and Data: From CSP-OZ to Java. PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.

    Google Scholar 

11. Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR 2, Dec. 1995.

    Google Scholar 

12. M.R. Hansen and C. Zhou. Duration calculus: Logical foundations. Formal Aspects of Computing, 9:283–330, 1997.

    Article  MATH  Google Scholar 

13. S. Heilmann. Proof Support for Duration Calculus. PhD thesis, Dept. Inform. Technology, Tech. Univ. Denmark, June 1999. Tech. Report IT-TR: 1999-030.

    Google Scholar 

14. M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.

    Google Scholar 

15. J. He, C.A.R. Hoare, M. Fränzle, M. Müller-Olm, E.-R. Olderog, M. Schenke, M.R. Hansen, A.P. Ravn, and H. Rischel. Provably correct systems. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault Tolerant Systems, volume 863 of LNCS, pages 288–335. Springer, 1994.

    Google Scholar 

16. C.A.R. Hoare and J. He. Unifying Theories of Programming. Prentice Hall, 1997.

    Google Scholar 

17. C.A.R. Hoare. Communicating sequential processes. CACM, 21:666–677, 1978.

    MATH  Google Scholar 

18. C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

    Google Scholar 

19. Kolyang. HOL-Z — An Integrated Formal Support Environment for Z in Isabelle /HOL. PhD thesis, Univ. Bremen, 1997. Shaker Verlag, Aachen, 1999.

    Google Scholar 

20. D.G. Luenberger. Introduction to Dynamic Systems. Theory, Models & Applications. Wiley, 1979.

    Google Scholar 

21. B.P. Mahony and J.S. Dong. Blending Object-Z and Timed CSP: an introduction to TCOZ. In K. Futatsugi, R. Kemmerer, and K. Torii, editors, The 20th International Conference on Software Engineering (ICSE’98), pages 95–104. IEEE Computer Society Press, 1998.

    Google Scholar 

22. B.P. Mahony and J.S. Dong. Sensors and actuators in TCOZ. In J.M. Wing, J. Woodcock, and J. Davies, editors, FM’99 — Formal Methods, volume 1709 of LNCS, pages 1166–1185. Springer, 1999.

    Chapter  Google Scholar 

23. B. Moszkowski. A temporal logic for multi-level reasoning about hardware. IEEE Computer, 18(2):10–19, 1985.

    Google Scholar 

24. B. Moszkowski. Executing Temporal Logic Programs. Cambridge Univ. Press, 1986.

    Google Scholar 

25. R. De Nicola and M. Hennessy. Testing equivalences of processes. Theoretical Computer Science, 34:83–133, 1983.

    Article  Google Scholar 

26. E.-R. Olderog, A. P. Ravn, and J. U. Skakkebæk. Refining system requirements to program specifications. In C. Heitmeyer and D. Mandrioli, editors, Formal Methods for Real-Time Computing, pages 107–134. Wiley, 1996.

    Google Scholar 

27. A.P. Ravn, H. Rischel, and K.M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Trans. Software Engineering, 19(1):41–55, 1993.

    Article  Google Scholar 

28. A.P. Ravn. Design of embedded real-time computing systems. Technical Report ID-TR: 1995-170, Tech. Univ. Denmark, 1995. Thesis for Doctor of Technics.

    Google Scholar 

29. A.W. Roscoe. Model-checking CSP. In A.W. Roscoe, editor, A Classical Mind — Essays in Honour of C.A.R.Hoare, pages 353–378. Prentice-Hall, 1994.

    Google Scholar 

30. A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.

    Google Scholar 

31. M. Saaltink. The Z/EVES system. In J. Bowen, M. Hinchey, and D. Till, editors, ZUM’97, volume 1212 of LNCS, pages 72–88. Springer, 1997.

    Google Scholar 

32. T. Santen. A Mechanized Logical Model of Z and Object-Oriented Specification. PhD thesis, Tech. Univ. Berlin, Juli 1999. Shaker Verlag, Aachen, 2000.

    Google Scholar 

33. M. Schenke and E.-R. Olderog. Transformational design of real-time systems — Part 1: from requirements to program specifications. Acta Inform., 36:1–65, 1999.

    Article  MATH  MathSciNet  Google Scholar 

34. B. Selic and J. Rumbaugh. Using UML for modeling complex real-time systems. Technical report, ObjecTime, 1998.

    Google Scholar 

35. J.U. Skakkebaek. A Verification Assistent for a Real-Time Logic. PhD thesis, Dept. Sci., Tech. Univ. Denmark, Nov. 1994. Tech. Report ID-TR: 1994-150.

    Google Scholar 

36. G. Smith and I. Hayes. Towards real-time Object-Z. In K. Araki, A. Galloway, and K. Taguchi, editors, Integrated Formal Methods, pages 49–65. Springer, 1999.

    Google Scholar 

37. G. Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000.

    Google Scholar 

38. J.M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall International Series in Computer Science, 2nd edition, 1992.

    Google Scholar 

39. J. Woodcock and J. Davies. Using Z — Specification, Refinement, and Proof. Prentice-Hall, 1996.

    Google Scholar 

40. C. Zhou, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1991.

    Article  MATH  MathSciNet  Google Scholar 

Download references