×

Introducing extra operations in refinement. (English) Zbl 1342.68204


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

LOTOS; Z
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Abrial J-R (2010) Modelling in Event-B. CUP, Cambridge · doi:10.1017/CBO9781139195881
[2] Aceto L (1992) Action refinement in process algebras. CUP, Cambridge · Zbl 0762.68003
[3] Abrial J-R, Cansell D, Méry D (2005) Refinement and reachability in Event-B. In: Treharne H, King S, Henson MC, Schneider SA (eds) ZB. LNCS, vol 3455, pp 222-241. Springer · Zbl 1118.68535
[4] Back RJR (1993) Refinement of parallel and reactive programs. In: Broy M (ed) Program design calculi, pp 73-92
[5] Bolognesi T, Brinksma E (1988) Introduction to the ISO specification language LOTOS. Comput Netw ISDN 14(1): 25-59 · doi:10.1016/0169-7552(87)90085-7
[6] Bolton C, Davies J (2006) A singleton failures semantics for communicating sequential processes. Form Asp Comp 18: 181-210 · Zbl 1110.68067 · doi:10.1007/s00165-005-0081-x
[7] Boiten EA, Derrick J (2009) Modelling divergence in relational concurrent refinement. In: Leuschel M, Wehrheim H (eds) IFM 2009. LNCS, vol 5423, pp 183-199. Springer · Zbl 1211.68265
[8] Boiten EA, Derrick J (2010) Incompleteness of relational simulations in the blocking paradigm. Sci Comput Program 75(12): 1262-1269 · Zbl 1209.68306 · doi:10.1016/j.scico.2010.07.003
[9] Boiten EA, Derrick J, Schellhorn G (2009) Relational concurrent refinement II: internal operations and outputs. Form Asp Comp 21(1-2): 65-102 · Zbl 1165.68412 · doi:10.1007/s00165-007-0066-z
[10] Boiten EA (2011) Perspicuity and granularity in refinement. In: Derrick J, Boiten EA, Reeves S (eds) Refinement workshop 2011. EPTCS, vol 55, pp 155-165 · Zbl 1367.68194
[11] Banach R, Schellhorn G (2010) Atomic actions, and their refinements to isolated protocols. Form Asp Comp 22(1): 33-61 · Zbl 1183.68362 · doi:10.1007/s00165-009-0103-1
[12] Butler M (1997) An approach to the design of distributed systems with B AMN. In: Bowen JP, Hinchey MG, Till D (eds) ZUM’97: the Z formal specification notation. LNCS, vol 1212, pp 223-241. Springer
[13] Butler M (2009) Decomposition structures for Event-B. In: Leuschel M, Wehrheim H (eds) IFM. LNCS, vol 5423, pp 20-38. Springer
[14] Derrick J, Boiten EA (1999) Non-atomic refinement in Z. In: Wing JM, Woodcock JCP, Davies J (eds) FM’99 World congress on formal methods in the development of computing systems. LNCS, vol 1708, pp 1477-1496. Springer · Zbl 1209.68306
[15] Derrick J, Boiten EA (2001) Refinement in Z and object-Z. Springer, Berlin · Zbl 0982.68086 · doi:10.1007/978-1-4471-0257-1
[16] Derrick J, Boiten EA, Bowman H, Steen MWA (1998) Specifying and refining internal operations in Z. Form Asp Comp 10: 125-159 · Zbl 0912.68133 · doi:10.1007/s001650050007
[17] De Roever WP, Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. CUP, Cambridge · Zbl 0955.68076 · doi:10.1017/CBO9780511663079
[18] Derrick J, Wehrheim H (2003) Using coupled simulations in non-atomic refinement. In: Bert D, Bowen JP, King S, Waldén M (eds) ZB 2003. LNCS, vol 2651, pp 127-147. Springer · Zbl 1028.68541
[19] Hesselink WH (2005) Eternity variables to prove simulation of specifications. ACM T Comput Log 6(1): 175-201 · Zbl 1367.68194 · doi:10.1145/1042038.1042044
[20] Hoare CAR, Jifeng H (1998) Unifying theories of programming. Prentice Hall, New Jersey
[21] Jifeng H, Hoare CAR, Sanders JW (1986) Data refinement refined. In: Robinet B, Wilhelm R (eds) Proceedings of the ESOP 86. LNCS, vol 213, pp 187-196. Springer
[22] Hoare CAR (1985) Communicating sequential processes. Prentice Hall, New Jersey · Zbl 0637.68007
[23] Lamport L (1994) The temporal logic of actions. ACM T Prog Lang Sys 16(3): 872-923 · doi:10.1145/177492.177726
[24] Morgan CC (1994) Programming from Specifications. International series in Computer Science, 2nd edn. Prentice Hall, New Jersey
[25] Reeves S, Streader D (2008) Data refinement and singleton failures refinement are not equivalent. Form Asp Comp 20(3): 295-301 · Zbl 1149.68057 · doi:10.1007/s00165-008-0076-5
[26] Schellhorn G (2005) ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor Comput Sci 336(2-3): 403-436 · Zbl 1080.68058 · doi:10.1016/j.tcs.2004.11.013
[27] 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, pp 3-99. North-Holland · Zbl 1035.68073
[28] Wirth N (1971) Program development by stepwise refinement. Commun ACM 14: 221-227 · Zbl 0214.43005 · doi:10.1145/362575.362577
[29] Woodcock JCP, Davies J (1996) Using Z: specification, refinement, and proof. Prentice Hall, New Jersey · Zbl 0855.68060
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.