References

2

R.J.R. Back. Refinement calculus, part II: Parallel and reactive programs. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems - Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 67-93. Springer-Verlag, 1990.

3

D. Bjørner. Trusted computing systems. In Proc. 14th International Conference on Software Engineering (ICSE), Melbourne, Australia. North-Holland, May 1992.

4

D. Bjørner et al. A ProCoS project description: ESPRIT BRA 3104. Bulletin of the EATCS, 39:60-73, 1989.

5

D. Bjørner, H. Langmaack, and C.A.R. Hoare. ProCoS I final deliverable. ProCoS Technical Report [ID/DTH DB 13/1], Department of Computer Science, Technical University of Denmark, DK-2800 Lyngby, Denmark, January 1993.

6

J. Bohn. Interaktive synthese kommunizierender systeme mit LAMBDA. Bericht, Carl-von-Ossietzky-Universität Oldenburg, Germany, February 1993.

7

J.P. Bowen. From programs to object code using logic and logic programming. In R. Giegerich and S.L. Graham, editors, Code Generation - Concepts, Tools, Techniques, Workshops in Computing, pages 173-192. Springer-Verlag, 1992. Proc. International Workshop on Code Generation, Dagstuhl, Germany, 20-24 May 1991.

8

J.P. Bowen, editor. Towards Verified Systems. Real-Time Safety Critical Systems Series. Elsevier, 1994. In press.

9

J.P. Bowen, B. Buth, He Jifeng, M. Müller-Olm, E.-R. Olderog, and A.P. Ravn. Provably correct systems: Tutorial material, Formal Methods Europe 93. ProCoS Technical Report [ID/DTH APR 20/1], Department of Computer Science, Technical University of Denmark, DK-2800 Lyngby, Denmark, March 1993.

10

J.P. Bowen, M. Fränzle, E.-R. Olderog, and A.P. Ravn. Developing correct systems. In Proc. 5th Euromicro Workshop on Real-Time Systems, Oulu, Finland. IEEE Computer Society Press, pages 176-187, 1993.

11

B. Buth, K.-H. Buth, M. Fränzle, B. von Karger, Y. Lakhneche, H. Langmaack, and M. Müller-Olm. Provably correct compiler development and implementation. In Compiler Construction '92, Proc. 4th International Conference (CC'92), Paderborn, Germany, volume 641 of Lecture Notes in Computer Science, pages 141-155. Springer-Verlag, October 1992.

12

K.-H. Buth. Simulation of transition systems with term rewriting systems. Bericht 9212, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, Germany, 1992.

13

K.-H. Buth. Using SOS definitions in term rewriting proofs. In Ursula Martin and Jeannette Wing, editors, Proc. First International Workshop on Larch, Workshops in Computing. Springer-Verlag, 1992. Full version available as Bericht 9214, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, Germany.

14

K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.

15

M. Engel et al. A formal approach to computer systems requirements documentation. In Hybrid Systems, Lecture Notes in Computer Science 736. Springer-Verlag, pages 452-474, 1993.

16

M. Fränzle. Proposal for a programming language core for ProCoS II. ProCoS Technical Report [Kiel MF 11/2], Christian-Albrechts-Universität Kiel, Germany, March 1993.

17

D.I. Good and W.D. Young. Mathematical methods for digital system development. In S. Prehn and W.J. Toetenel, editors, VDM'91, Formal Software Development Methods, Volume 2: Tutorials, volume 552 of Lecture Notes in Computer Science, pages 406-430. Springer-Verlag, 1991.

18

M.R. Hansen and E.-R. Olderog. Constructing circuits from decidable Duration Calculus. Bericht, Carl-von-Ossietzky-Universität Oldenburg, Germany, April 1993.

19

M.R. Hansen and Zhou Chaochen. Semantics and completeness of Duration Calculus. In W-P. de Roever, editor, Proc. REX'91, Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

20

He Jifeng and J.P. Bowen. Time interval semantics and implementation of a real-time programming language. In Proc. 4th Euromicro Workshop on Real-Time Systems, pages 110-115. IEEE Press, 1992.

21

He Jifeng, I. Page, and J.P. Bowen. Towards a provably correct hardware implementation of Occam. In G.J. Milne and L. Pierre, editors, Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science 683. Springer-Verlag, pages 214-225, 1993.

22

C.A.R. Hoare. Refinement algebra proves correctness of compiling specifications. In C.C. Morgan and J.C.P. Woodcock, editors, 3rd Refinement Workshop, Workshops in Computing, pages 33-48. Springer-Verlag, 1991.

23

C.A.R. Hoare and He Jifeng. Refinement algebra proves correctness of a compiler. In M. Broy, editor, Programming and Mathematical Method: International Summer School directed by F.L. Bauer, M. Broy, E.W. Dijkstra, C.A.R. Hoare, volume 88 of NATO ASI Series F: Computer and Systems Sciences, pages 245-269. Springer-Verlag, 1992.

24

C.A.R. Hoare, He Jifeng, J.P. Bowen, and P.K. Pandya. An algebraic approach to verifiable compiling specification and prototyping of the ProCoS level 0 programming language. In CEC DG XIII, editor, ESPRIT'90 Conference Proceedings, Brussels, pages 804-818, 1990.

25

C.A.R. Hoare, He Jifeng, and A.C.A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30:701-739, 1993.

26

L. Lamport. The temporal logic of actions. Technical Report 79, Digital Systems Research Center, 130 Lytton Avenue, Palo Alto, California 94301, USA, 25 December 1991.

27

Z. Liu, A.P. Ravn, E.V. Sørensen, and Zhou Chaochen. A probabilistic Duration Calculus. In Proc. 2nd Int. Workshop on Responsive Computing Systems, Tokyo, Japan. KDD R&D Laboratories, October 1992.

28

J.S. Moore et al. Special issue on system verification. Journal of Automated Reasoning, 5(4):409-530, December 1989.

29

S.M. Brien and J.E. Nicholls. Z base standard. Technical Report PRG-107, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford OX1 3QD, UK, 30 November 1992. Accepted for ISO standardization under ISO/IEC JTC1/SC22.

30

E-R. Olderog. Towards a design calculus for communicating programs. In J.C.M. Baeten and J.F. Groote, editors, Proc. CONCUR'91, volume 527 of Lecture Notes in Computer Science, pages 61-72. Springer-Verlag, 1991.

31

E-R. Olderog. Interfaces between languages for communicating systems. In W. Kuich, editor, Automata, Languages and Programming: Proc. 19th International Colloquium (ICALP), Wien, Austria, July 1992, volume 623 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

32

E.-R. Olderog and S. Rössig. A case study in transformational design of concurrent systems. In M.-C. Gaudel and J.-P. Jouannaud, editors, Proc. TAPSOFT'93, volume 668 of Lecture Notes in Computer Science, pages 90-104. Springer-Verlag, 1993.

33

I. Page and W. Luk. Compiling Occam into field-programmable gate arrays. In W. Moore and W. Luk, editors, FPGAs, Oxford Workshop on Field Programmable Logic and Applications, pages 271-283, 15 Harcourt Way, Abingdon OX14 1NV, UK, 1991. Abingdon EE&CSBooks.

34

A.P. Ravn and H. Rischel. Requirements capture for embedded real-time systems. In Proc. IMACS-IFAC Symposium on Modelling and Control of Technological Systems (MCTS'91), volume 2, pages 147-152, 1991.

35

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

36

S. Rössig and M. Schenke. Towards a design calculus for communicating programs. In S. Prehn and W.J. Toetenel, editors, VDM'91 Formal Software Development Methods, volume 551 of Lecture Notes in Computer Science, pages 148-163. Springer-Verlag, 1991.

37

M. Schenke. A timed specification language for concurrent reactive systems. ProCoS Technical Report [OLD MS 6], Carl-von-Ossietzky-Universität Oldenburg, Germany, March 1993.

38

J.U. Skakkebæk, A.P. Ravn, H. Rischel, and Zhou Chaochen. Specification of embedded real-time systems. In Proc. 4th Euromicro Workshop on Real-Time Systems, pages 116-121. IEEE Press, 1992.

39

E.V. Sørensen, J. Nordahl, and N.H. Hansen. From CSP models to Markov models. IEEE Transactions on Software Engineering, to appear.

40

Zhou ChaoChen, M.R. Hansen, A.P. Ravn, and H. Rischel. Duration specifications for shared processors. In J. Vytopil, editor, Proc. Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science, pages 21-32. Springer-Verlag, 1991.

41

Zhou Chaochen, M.R. Hansen, and P. Sestoft. Decidability and undecidability results for Duration Calculus. In STACS '93: 10th Symposium on Theoretical Aspects of Computer Science, Würzburg, Germany, February 1993, Lecture Notes in Computer Science. Springer-Verlag, 1993.

42

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

43

Zhou Chaochen, A.P. Ravn, and M.R. Hansen. An extended Duration Calculus for hybrid systems. In Hybrid Systems, Lecture Notes in Computer Science 736. Springer-Verlag, pages 36-59, 1993.