Relational concurrent refinement. II: Internal operations and outputs. (English) Zbl 1165.68412
Keywords:
data refinement; Z; simulations, process algebraic semantics; failures-divergences refinement; deadlock; internal operations; outputs; mechanisation; KIVReferences:
| [1] | Abrial J-R (1996) The B-Book: assigning programs to meanings. Cambridge University Press, Cambridge · Zbl 0915.68015 |
| [2] | Boiten EA, de Roever W-P (2003) Getting to the bottom of relational refinement: relations and correctness, partial and total. In: Berghammer R, Möller B (eds) 7th International seminar on relational methods in computer science (RelMiCS 7). University of Kiel, pp 82–88 |
| [3] | Bolton C, Davies J, Woodcock JCP (1999) On the refinement and simulation of data types and processes. In: Araki K, Galloway A, Taguchi K (eds) International conference on integrated formal methods 1999 (IFM’99). Springer, Berlin, pp 273–292 · Zbl 0963.68126 |
| [4] | Berghammer R, Zierer H (1986) Relation algebraic semantics of deterministic and non-deterministic programs. Theor Comp Sci 43:123–147 · Zbl 0596.68019 · doi:10.1016/0304-3975(86)90172-6 |
| [5] | Brookes SD, Hoare CAR, Roscoe AW (1984) A theory of communicating sequential processes. J ACM 31(3):560–599 · Zbl 0628.68025 · doi:10.1145/828.833 |
| [6] | Bolognesi T, Brinksma E (1988) Introduction to the ISO Specification Language LOTOS. Comput Networks ISDN 14(1):25–59 · doi:10.1016/0169-7552(87)90085-7 |
| [7] | Boiten EA, Derrick J (2002) Unifying concurrent and relational refinement. In: Derrick J, Boiten EA, Woodcock JCP, von Wright J (eds) Refine 2002, ENTCS 70:94–131 · Zbl 1270.68078 |
| [8] | Bolton C, Davies J (2002) Refinement in Object-Z and CSP. In: Butler M, Petre L, Sere K (eds) Integrated formal methods (IFM 2002), Lecture notes in computer science, vol 2335. Springer, Berlin, pp 225–244 · Zbl 1057.68639 |
| [9] | Bolton C, Davies J (2006) A singleton failures semantics for communicating sequential processes. Form Asp Comput 18:181–210 · Zbl 1110.68067 · doi:10.1007/s00165-005-0081-x |
| [10] | Bowman H, Gomez R (2005) Concurrency theory: calculi and automata for modelling untimed and timed concurrent systems. Springer, New York · Zbl 1140.68046 |
| [11] | Bolton C (2002) On the refinement of state-based and event-based models. Ph.D. thesis, University of Oxford |
| [12] | Bolton C, Lowe G (2003) A hierarchy of failures-based models. In: Corradini F, Nestmann U (eds) Proceedings of express 2003: 10th international workshop on expressiveness in concurrency. Elsevier Science, Amsterdam · Zbl 1271.68129 |
| [13] | Bolton C, Lowe G (2005) A hierarchy of failures-based models: theory and application. Theor Comp Sci 330(3):407–438 · Zbl 1078.68104 · doi:10.1016/j.tcs.2004.10.004 |
| [14] | Brookes SD, Roscoe AW (1985) An improved failures model for communicating processes. In: Brookes SD, Roscoe AW, Winskel G (eds) Seminar on concurrency, Lecture notes in computer science, vol 197. Springer, Berlin, pp 281–305 · Zbl 0565.68023 |
| [15] | Cooper D, Stepney S, Woodcock J (2002) Derivation of Z refinement proof rules: forwards and backwards rules incorporating input/output refinement. Technical Report YCS-2002-347, University of York. URL: http://www-users.cs.york.ac.uk/\(\sim\)susan/bib/ss/z/zrules.htm |
| [16] | Derrick J, Boiten EA, Bowman H, Steen MWAS (1998) Specifying and refining internal operations in Z. Form Asp Comput 10:125–159 · Zbl 0912.68133 · doi:10.1007/s001650050007 |
| [17] | Derrick J, Boiten EA (2001) Refinement in Z and object-Z: foundations and advanced applications, FACIT series. Springer, London · Zbl 0982.68086 |
| [18] | Derrick J, Boiten EA (2003) Relational concurrent refinement. Form Asp Comput 15(1):182–214 · Zbl 1093.68061 · doi:10.1007/s00165-003-0007-4 |
| [19] | Derrick J, Boiten EA (2006) Relational concurrent refinement with internal operations. In: Aichernig B, Boiten EA, Derrick J, Groves L (eds) BCS-FACS Refinement Workshop, ENTCS 187:35–53 |
| [20] | Deutsch M, Henson MC (2006) An analysis of refinement in an abortive paradigm. Form Asp Comput 18(3):329–363 · Zbl 1105.68070 · doi:10.1007/s00165-006-0006-3 |
| [21] | Doornbos H (1994) A relational model of programs without the restriction to Egli-Milner constructs. In: Olderog E-R (ed) PROCOMET ’94, IFIP, pp 357–376 |
| [22] | De Roever W-P, Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. Cambridge University Press, Cambridge · Zbl 0955.68076 |
| [23] | Dunne S, Conroy S (2005) Process refinement in B. In: Treharne H, King S, Henson MC, Schneider S (eds) ZB 2005: formal specification and development in Z and B, 4th international conference of B and Z users, Lecture notes in computer science, vol 3455. Springer, Berlin, pp 45–64 · Zbl 1118.68543 |
| [24] | Fischer C (1997) CSP-OZ–A combination of CSP and Object-Z. In: Bowman H, Derrick J (eds) Second IFIP international conference on formal methods for open object-based distributed systems. Chapman & Hall, London, pp 423–438 |
| [25] | He J (1989) Process refinement. In: McDermid J (ed) The theory and practice of refinement. Butterworths, London · Zbl 0696.68099 |
| [26] | Hennessy M, Ingólfsdóttir A (1993) A theory of communicating processes with value passing. Inf Comput 107(2):202–236 · Zbl 0794.68098 · doi:10.1006/inco.1993.1067 |
| [27] | He J, Hoare CAR, Sanders JW (1986) Data refinement refined. In Robinet B, Wilhelm R (eds) Proc. ESOP’86. Lecture notes in computer science, vol 213. Springer, Berlin, pp 187–196 |
| [28] | Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs · Zbl 0637.68007 |
| [29] | Hoare CAR, He J (1998) Unifying theories of programming. Prentice-Hall, Englewood Cliffs |
| [30] | Josephs MB (1988) A state-based approach to communicating processes. Distrib Comput 3:9–18 · Zbl 0659.68046 · doi:10.1007/BF01788563 |
| [31] | Leduc G (1991) On the role of implementation relations in the design of distributed systems using LOTOS. Ph.D. thesis, University of Liège |
| [32] | Miarka R, Boiten EA, Derrick J (2000) Guards, preconditions and refinement in Z. In: Bowen JP, Dunne S, Galloway A, King S (eds) ZB2000: Formal specification and development in Z and B. Lecture notes in computer science, vol 1878. Springer, Berlin, pp 286–303 |
| [33] | Milner R (1989) Communication and concurrency. Prentice-Hall, Englewood Cliffs · Zbl 0683.68008 |
| [34] | Reeves S, Streader D (2006) State- and event-based refinement. Technical report, Department of Computer Science, University of Waikato · Zbl 1096.68109 |
| [35] | Roscoe AW (1998) The theory and practice of concurrency. Prentice-Hall, Englewood Cliffs |
| [36] | Reif W, Schellhorn G, Stenzel K, Balser M (1998) Structured specifications and interactive proofs with KIV. In: Bibel W, Schmitt P (eds) Automated deduction–a basis for applications, vol II: systems and implementation techniques, Chap. 1: Interactive Theorem Proving. Kluwer, Dordrecht, pp 13–39 · Zbl 0970.68149 |
| [37] | Schellhorn G (2005) ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor Comp Sci 336(2–3):403–435 · Zbl 1080.68058 · doi:10.1016/j.tcs.2004.11.013 |
| [38] | Schellhorn G (2006) Web presentation of the KIV proofs of ’Relational Concurrent Refinement Part II: Internal Operations and Output’. URL: http://www.informatik.uni-augsburg.de/swt/projects/Refinement/Web/CSPRef |
| [39] | Schneider S, Treharne H (2004) CSP theorems for communicating B machines. Form Asp Comput 17(4):390–422 · Zbl 1103.68599 · doi:10.1007/s00165-005-0076-7 |
| [40] | Schellhorn G, Grandy H, Haneberg D, Reif W (2006) The Mondex challenge: machine checked proofs for an electronic purse. In: Misra J, Nipkow T, Sekerinski E (eds) Formal methods 2006, Proceedings. Lecture notes in computer science, vol 4085. Springer, Berlin, pp 16–31 |
| [41] | Smith G, Derrick J (2002) Abstract specification in Object-Z and CSP. In: George C, Miao H (eds) Formal methods and software engineering. Lecture notes in computer science, vol 2495. Springer, Berlin, pp 108–119 · Zbl 1015.68600 |
| [42] | Spivey JM (1992) The Z notation: a reference manual, 2nd edn. Prentice-Hall, Englewood Cliffs |
| [43] | Valmari A, Tienari M (1995) Compositional failure-based semantics models for basic LOTOS. Form Asp Comput 7(4):440–468 · Zbl 0838.68076 · doi:10.1007/BF01211218 |
| [44] | van Glabbeek, RJ (2001) The linear time–branching time spectrum I. The semantics of concrete sequential processes. In: Bergstra JA, Ponse A, Smolka SA (eds) Handbook of process algebra. North-Holland, Amsterdam pp 3–99 · Zbl 1035.68073 |
| [45] | Woodcock JCP, Davies J (1996) Using Z: specification, refinement, and proof. Prentice-Hall, Englewood Cliffs · Zbl 0855.68060 |
| [46] | Woodcock JCP, Morgan CC (1990) Refinement of state-based concurrent systems. In: Bjørner D, Hoare CAR, Langmaack H (eds) VDM’90: VDM and Z!–formal methods in software development, Lecture notes in computer science, vol 428. Springer, Berlin |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
