Bibliography

Bibliography]Bibliography

1

M. Abadi and L. Lamport.
The existence of refinement mappings.
Theoretical Computer Science, 2(82):253-284, 1991.

2

J.-R. Abrial.
The B-Book: Assigning Programs to Meanings.
CUP, 1996.

3

J.-R. Abrial and L. Mussat.
Specification and design of a transmission protocol by successive refinements using B.
In M. Broy and B. Schieder (Eds), Mathematical Methods in Program Development, volume 158 of NATO ASI Series F: Computer and Systems Sciences, pp 129-200. Springer, 1997.

4

L. Aceto.
Action Refinement in Process Algebras.
CUP, London, 1992.

5

M. Ainsworth, A. H. Cruickshank, P. J. L. Wallis, and L. J. Groves.
Viewpoint specification and Z.
Information and Software Technology, 36(1):43-51, February 1994.

6

A. J. Alencar and J. A. Goguen.
OOZE: An object oriented Z environment.
In P. America (Ed), ECOOP '91 - Object-Oriented Programming, LNCS 512, pp 180-199. Springer-Verlag, 1991.

7

P. America.
A Parallel Object-Oriented Language with Inheritance and Subtyping.
In Proceedings of the OOPSLA/ECOOP '90 Conference on Object-Oriented Programming Systems, Languages and Applications, pp 161-168, October 1990.
Published as ACM SIGPLAN Notices, volume 25, number 10.

8

K. Araki, A. Galloway, and K. Taguchi (Eds).
International Conference on Integrated Formal Methods 1999 (IFM'99).
Springer, York, July 1999.

9

R. D. Arthan.
On free type definitions in Z.
In J. E. Nicholls (Ed), Sixth Annual Z User Workshop, pp 40-58, York, December 1991. Springer-Verlag.

10

R. J. R. Back.
A method for refining atomicity in parallel algorithms.
In PARLE'89 Parallel Architectures and Languages Europe, number 366 in Lecture Notes in Computer Science, pp 199-216, Eindhoven, Netherlands, June 1989. Springer-Verlag.

11

R. J. R. Back.
Atomicity refinement in a refinement calculus framework.
Reports on computer science and mathematics 142, Abo Akademi, 1993.

12

R. J. R. Back and R. Kurki-Suonio.
Distributed cooperation with action systems.
ACM Transactions on Programming Languages and Systems, 10(4):513-554, October 1988.

13

R. J. R. Back and R. Kurki-Suonio.
Decentralization of process nets with centralized control.
Distributed Computing, 3(2):73-87, 1989.

14

R. J. R. Back and J. von Wright.
Trace refinement of action systems.
In B. Jonsson and J. Parrow (Eds), CONCUR'94: Concurrency Theory, number 836 in Lecture Notes in Computer Science, pp 367-384, Uppsala, Sweden, August 1994. Springer-Verlag.

15

R. Barden, S. Stepney, and D. Cooper.
Z in Practice.
BCS Practitioner Series. Prentice Hall, 1994.

16

S. Behnia and H. Waeselynck.
Test criteria definition for B models.
In FM'99 [206], pp 509-529.

17

E. Bertino and G. Guerrini.
Viewpoints in object database systems.
In Viewpoints'96 [83], pp 289-293.

18

J. C. Bicarregui (Ed).
Proof in VDM: Case Studies.
FACIT. Springer, 1998.

19

E. A. Boiten, H. Bowman, J. Derrick, and M. W. A. Steen.
Issues in multiparadigm viewpoint specification.
In Viewpoints'96 [83], pp 162-166.

20

E. A. Boiten and J. Derrick.
Grey box data refinement.
In IRW/FMP'98 [104], pp 45-59.

21

E. A. Boiten and J. Derrick.
IO-refinement in Z.
In A. Evans, D. J. Duke, and T. Clark (Eds), 3rd BCS-FACS Northern Formal Methods Workshop. Springer-Verlag, September 1998.
http://www.ewic.org.uk/.

22

E. A. Boiten and J. Derrick.
Liberating data refinement.
In R. C. Backhouse and J. N. Oliveira (Eds), Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pp 144-166. Springer-Verlag, 2000.

23

E. A. Boiten, J. Derrick, H. Bowman, and M. W. A. Steen.
Constructive consistency checking for partial specification in Z.
Science of Computer Programming, 35(1):29-75, September 1999.

24

T. Bolognesi and E. Brinksma.
Introduction to the ISO Specification Language LOTOS.
Computer Networks and ISDN Systems, 14(1):25-59, 1988.

25

C. Bolton, J. Davies, and J. C. P. Woodcock.
On the refinement and simulation of data types and processes.
In IFM'99 [8], pp 273-292.

26

M. Bonsangue, J. Kok, and K. Sere.
An approach to object-orientation in action systems.
In J. Jeuring (Ed), Mathematics of Program Construction (MPC'98), volume 1422 of Lecture Notes in Computer Science, pp 68-95. Springer-Verlag, June 1998.

27

M. Bonsangue, J. Kok, and K. Sere.
Developing object-based distributed systems.
In FMOODS'99 [49], pp 19-34.

28

A. Borgida, J. Mylopoulos, and R. Reiter.
And nothing else changes: The frame problem in procedure specifications.
In Proc. 15th International Conference on Software Engineering, pp 303-314, Baltimore, Maryland, May 1993. IEEE Computer Society Press.

29

L. Bottaci and J. Jones.
Formal Specification using Z: A modelling approach.
International Thomson Publishing, 1995.

30

J. P. Bowen.
Formal Specification and Documentation using Z: A Case Study Approach.
International Thomson Computer Press, 1996.

31

J. P. Bowen, S. Dunne, A. Galloway, and S. King (Eds).
ZB2000: Formal Specification and Development in Z and B, volume 1878 of Lecture Notes in Computer Science.
Springer-Verlag, September 2000.

32

J. P. Bowen, A. Fett, and M. G. Hinchey (Eds).
ZUM'98: The Z Formal Specification Notation, volume 1493 of Lecture Notes in Computer Science.
Springer-Verlag, September 1998.

33

J. P. Bowen and J. A. Hall (Eds).
ZUM'94, Z User Workshop.
Workshops in Computing. Springer-Verlag, Cambridge, United Kingdom, June 1994.

34

J. P. Bowen and M. G. Hinchey (Eds).
ZUM'95: The Z Formal Specification Notation, volume 967 of Lecture Notes in Computer Science.
Springer-Verlag, Limerick, September 1995.

35

J. P. Bowen, M. G. Hinchey, and D. Till (Eds).
ZUM'97: The Z Formal Specification Notation, volume 1212 of Lecture Notes in Computer Science.
Springer-Verlag, April 1997.

36

J. P. Bowen and J. E. Nicholls (Eds).
Seventh Annual Z User Workshop.
Springer-Verlag, London, December 1992.

37

H. Bowman, E. A. Boiten, J. Derrick, and M. W. A. Steen.
Viewpoint consistency in ODP, a general interpretation.
In E. Najm and J. B. Stefani (Eds), First IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems, pp 189-204, Paris, March 1996. Chapman & Hall.

38

W. Brauer, R. Gold, and W. Vogler.
A survey of behaviour and equivalence preserving refinements of Petri nets.
In G. Rozenberg (Ed), Advances in Petri Nets, LNCS 483, pp 1-46. Springer-Verlag, 1991.

39

E. Brinksma.
A theory for the derivation of tests.
In S. Aggarwal and K. Sabnani (Eds), Protocol Specification, Testing and Verification, VIII, pp 63-74, Atlantic City, USA, June 1988. North-Holland.

40

E. Brinksma, G. Scollo, and C. Steenbergen.
Process specification, their implementation and their tests.
In B. Sarikaya and G. v. Bochmann (Eds), Protocol Specification, Testing and Verification, VI, pp 349-360, Montreal, Canada, June 1986. North-Holland.

41

G. Bruns and S. Anderson.
The formalization of a communications protocol.
Technical report, LFCS/Adelard SCCS, April 1992.

42

M. Büchi and E. Sekerinski.
Refining concurrent objects.
TUCS Technical Report 298, Abo Akademi, 1999.

43

M. Butler.
An approach to the design of distributed systems with B AMN.
In ZUM'97 [35], pp 223-241.

44

M. Butler.
csp2B: A practical approach to combining CSP and B.
In FM'99 [206], pp 490-508.

45

M. Butler.
Distributed electronic mail system.
In E. Sekerinski and K. Sere (Eds), Program Development by Refinement - Case Studies Using the B Method, FACIT. Springer, 1999.

46

S. Butler.
Behaviour in Object-Based Systems: A Formal Approach.
PhD thesis, University of Queensland, 1998.

47

E. Canver and F. W. von Henke.
Formal development of object-based systems in a temporal logic setting.
In FMOODS'99 [49], pp 419-436.

48

D. Carrington and P. Stocks.
A tale of two paradigms: Formal methods and software testing.
In ZUM'98 [32], pp 51-68.

49

P. Ciancarini, A. Fantechi, and R. Gorrieri (Eds).
Formal Methods for Open Object-based Distributed Systems.
Kluwer, February 1999.

50

T. Clement.
Comparing approaches to data reification.
In FME'94 [163], pp 118-133.

51

E. F. Codd.
Extending the database relational model to capture more meaning.
ACM Transactions on Database Systems, 4(4), December 1979.

52

E. Cohen and L. Lamport.
Reduction in TLA.
In CONCUR'98, volume 1466 of Lecture Notes in Computer Science, pp 317-331. Springer-Verlag, 1998.

53

E. Cusack.
Inheritance in object oriented Z.
In P. America (Ed), ECOOP '91 - Object-Oriented Programming, LNCS 512, pp 167-179. Springer-Verlag, 1991.

54

E. Cusack and G. H. B. Rafsanjani.
ZEST.
In S. Stepney, R. Barden, and D. Cooper (Eds), Object Orientation in Z, Workshops in Computing, pp 113-126. Springer-Verlag, 1992.

55

E. Cusack and C. Wezeman.
Deriving tests for objects specified in Z.
In ZUM'92 [36], pp 180-195.

56

J. W. de Bakker, W.-P. de Roever, and G. Rozenberg (Eds).
REX Workshop on Stepwise Refinement of Distributed Systems, Nijmegen, 1989, volume 430 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

57

J. W. de Bakker and E. P. de Vink.
Bisimulation semantics for concurrency with atomicity and action refinement.
Fundamenta Informaticae, 20:3-34, 1994.

58

M. de Groot and K. Robinson.
Correctness in refinement developments.
In IRW/FMP'98 [104], pp 117-132.

59

R. de Nicola and M. Hennessy.
Testing equivalences for processes.
Theoretical Computer Science, 34(3):83-133, 1984.

60

W.-P. de Roever and K. Engelhardt.
Data Refinement: Model-Oriented Proof Methods and their Comparison.
CUP, 1998.

61

J. Derrick.
A single complete refinement rule for Z.
Logic and Computation, 10(5):663-675, 2000.

62

J. Derrick and E. A. Boiten.
Testing refinements by refining tests.
In ZUM'98 [32], pp 265-283.

63

J. Derrick and E. A. Boiten.
Calculating upward and downward simulations of state-based specifications.
Information and Software Technology, 41:917-923, July 1999.

64

J. Derrick and E. A. Boiten.
Non-atomic refinement in Z.
In FM'99 [206], pp 1477-1496.

65

J. Derrick and E. A. Boiten.
Testing refinements of state-based formal specifications.
Software Testing, Verification & Reliability, 9:27-50, 1999.

66

J. Derrick and E. A. Boiten.
Refinement of state-based systems with internal operations.
Technical report, Computing Laboratory, University of Kent, Canterbury, 2000.

67

J. Derrick, E. A. Boiten, H. Bowman, and M. W. A. Steen.
Supporting ODP - translating LOTOS to Z.
In E. Najm and J.-B. Stefani (Eds), First IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems, pp 399-406, Paris, March 1996. Chapman & Hall.

68

J. Derrick, E. A. Boiten, H. Bowman, and M. W. A. Steen.
Weak refinement in Z.
In ZUM'97 [35], pp 369-388.

69

J. Derrick, E. A. Boiten, H. Bowman, and M. W. A. Steen.
Specifying and Refining Internal Operations in Z.
Formal Aspects of Computing, 10:125-159, December 1998.

70

J. Derrick and G. Smith.
Structural refinement in Object-Z/CSP.
In W. Grieskamp, T. Santen, and B. Stoddart (Eds), International Conference on Integrated Formal Methods 2000 (IFM'00), volume 1945 of Lecture Notes in Computer Science, pp 194-213. Springer, November 2000.

71

J. Dick and A. Faivre.
Automating the generation and sequencing of test cases from model-based specifications.
In J. C. P. Woodcock and P. G. Larsen (Eds), FME'93: Industrial-Strength Formal Methods, pp 268-284. Formal Methods Europe, Springer-Verlag, April 1993.
Lecture Notes in Computer Science 670.

72

E. W. Dijkstra.
A Discipline of Programming.
Prentice-Hall, Englewood Cliffs, N.J., 1976.

73

D. J. Duke and R. Duke.
Towards a semantics for Object-Z.
In D. Bjorner, C. A. R. Hoare, and H. Langmaack (Eds), VDM'90: VDM and Z! - Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pp 244-261, Kiel, FRG, April 1990. Springer-Verlag.

74

D. J. Duke and M. D. Harrison.
Event model of human-system interaction.
Software Engineering Journal, 10(1):3-12, January 1995.

75

D. J. Duke and M. D. Harrison.
Mapping user requirements to implementations.
Software Engineering Journal, 10(1):13-20, January 1995.

76

R. Duke, C. Bailes, and G. Smith.
A blocking model for reactive objects.
Formal Aspects of Computing, 8(3):347-368, 1996.

77

R. Duke, P. King, G. A. Rose, and G. Smith.
The Object-Z specification language version 1.
Technical Report 91-1, Software Verification Research Centre, Department of Computer Science, University of Queensland, May 1991.

78

R. Duke and G. A. Rose.
Formal Object-Oriented Specification Using Object-Z.
Cornerstones of Computing. Macmillan, 2000.

79

R. Duke, G. A. Rose, and G. Smith.
Object-Z: A specification language advocated for the description of standards.
Computer Standards and Interfaces, 17:511-533, September 1995.

80

M. Elvang-Goransson and R. E. Fields.
An extended VDM refinement relation.
In FME'94 [163], pp 175-189.

81

A. S. Evans.
An improved recipe for specifying reactive systems in Z.
In ZUM'97 [35], pp 275-294.

82

A. Finkelstein, J. Kramer, B. Nuseibeh, L. Finkelstein, and M. Goedicke.
Viewpoints: A framework for integrating multiple perspectives in system development.
International Journal on Software Engineering and Knowledge Engineering, Special Issue on Trends and Research Directions in Software Engineering Environments, 2(1):31-58, March 1992.

83

A. Finkelstein and G. Spanoudakis (Eds).
SIGSOFT '96 International Workshop on Multiple Perspectives in Software Development (Viewpoints '96).
ACM, 1996.

84

C. Fischer.
CSP-OZ - A combination of CSP and Object-Z.
In H. Bowman and J. Derrick (Eds), Second IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems, pp 423-438. Chapman & Hall, July 1997.

85

C. Fischer.
How to combine Z with a process algebra.
In ZUM'98 [32], pp 5-23.

86

C. Fischer.
Combination and Implementation of Processes and Data: From CSP-OZ to Java.
PhD thesis, University of Oldenburg, January 2000.

87

C. Fischer and G. Smith.
Combining CSP and Object-Z: Finite or infinite trace semantics.
In T. Higashino and A. Togashi (Eds), FORTE/PSTV'97, pp 503-518, Osaka, Japan, November 1997. Chapman & Hall.

88

C. Fischer and H. Wehrheim.
Model checking CSP-OZ specifications with FDR.
In IFM'99 [8], pp 315-334.

89

C. Fischer and H. Wehrheim.
Behavioural subtyping relations for object-oriented formalisms.
In T. Rus (Ed), Algebraic Methodology and Software Technology, volume 1816 of Lecture Notes in Computer Science, pp 469-483. Springer-Verlag, 2000.

90

J. Fitzgerald, C. B. Jones, and P. Lucas (Eds).
FME'97: Industrial Application and Strengthened Foundations of Formal Methods, volume 1313 of Lecture Notes in Computer Science.
Springer-Verlag, September 1997.

91

Formal Systems (Europe) Ltd.
Failures-Divergences Refinement: FDR 2, October 1997.
FDR2 User Manual.

92

M. Frappier, A. Mili, and J. Desharnais.
Defining and detecting feature interactions.
In R. S. Bird and L. Meertens (Eds), IFIP TC2 WG 2.1 International Workshop on Algorithmic Languages and Calculi, pp 212-239. Chapman & Hall, 1997.

93

A. Galloway and W. Stoddart.
An operational semantics for ZCCS.
In ICFEM'97 [119], pp 272-282.

94

P. H. B. Gardiner and C. C. Morgan.
A single complete rule for data refinement.
Formal Aspects of Computing, 5:367-382, 1993.

95

M.-C. Gaudel and J. C. P. Woodcock (Eds).
FME'96: Industrial Benefit of Formal Methods, Third International Symposium of Formal Methods Europe, volume 1051 of Lecture Notes in Computer Science.
Springer-Verlag, March 1996.

96

R. Gerth.
Foundations of compositional program refinement.
In REX'89 [56], pp 777-807.

97

S. J. Goldsack, K. Lano, and E. H. Dürr.
Annealing and data decomposition in VDM$^{++}$.
ACM SIGPLAN Notices, 31(4):32-38, April 1996.

98

R. Gorrieri.
Refinement, Atomicity and Transactions for Process Description Languages.
PhD thesis, University of Pisa, Pisa, 1991.

99

A. Griffiths.
A Formal Semantics to Support Modular Reasoning in Object-Z.
PhD thesis, University of Queensland, 1997.

100

A. Griffiths.
Modular reasoning in Object-Z.
In Asia-Pacific Software Engineering Conference and International Computer Science Conference. IEEE Computer Society Press, 1997.

101

K. Grimm.
Industrial requirements for the efficient development of reliable embedded systems.
In ZUM'98 [32], pp 1-4.

102

M. Grochtmann and K. Grimm.
Classification trees for partition testing.
Software Testing, Verification and Reliability, 3:63-82, 1993.

103

L. Groves.
Adapting program derivations using program conjunction.
In IRW/FMP'98 [104], pp 145-164.

104

J. Grundy, M. Schwenke, and T. Vickers (Eds).
International Refinement Workshop & Formal Methods Pacific '98.
Discrete Mathematics and Theoretical Computer Science. Springer-Verlag, Canberra, September 1998.

105

J. A. Hall.
Using Z as a specification calculus for object-oriented systems.
In D. Bjorner, C. A. R. Hoare, and H. Langmaack (Eds), VDM '90 VDM and Z - Formal Methods in Software Development, LNCS 428, pp 290-318, Kiel, FRG, April 1990. Springer-Verlag.

106

J. A. Hall.
Specifying and interpreting class hierarchies in Z.
In ZUM'94 [33], pp 120-138.

107

I. J. Hayes (Ed).
Specification Case Studies.
International Series in Computer Science. Prentice Hall, 1987.
2nd ed., 1993.

108

I. J. Hayes.
VDM and Z: A comparative case study.
Formal Aspects of Computing, 4(1):76-99, 1992.

109

I. J. Hayes and J. W. Sanders.
Specification by interface separation.
Formal Aspects of Computing, 7(4):430-439, 1995.

110

He Jifeng and C. A. R. Hoare.
Prespecification and data refinement.
In Data Refinement in a Categorical Setting, Technical Monograph, number PRG-90. Oxford University Computing Laboratory, November 1990.

111

He Jifeng, C. A. R. Hoare, and J. W. Sanders.
Data refinement refined.
In B. Robinet and R. Wilhelm (Eds), Proc. ESOP'86, volume 213 of Lecture Notes in Computer Science, pp 187-196. Springer-Verlag, 1986.

112

L. Heerink and J. Tretmans.
Refusal testing for classes of transition systems with inputs and outputs.
In T. Mizuno, N. Shiratori, T. Higashino, and A. Togashi (Eds), FORTE/PSTV XVII'97. Chapman and Hall, November 1997.

113

S. Helke and T. Santen.
Mechanized analysis of behavioral conformance in the Eiffel base libraries.
In Formal Methods Europe, 2001.
To appear.

114

M. C. Henson.
The standard logic of Z is inconsistent.
Formal Aspects of Computing, 10(3):243-247, 1998.

115

M. C. Henson and S. Reeves.
Revising Z: Part I - Logic and semantics.
Formal Aspects of Computing, 11(4):359-380, 1999.

116

M. C. Henson and S. Reeves.
Revising Z: Part II - Logical development.
Formal Aspects of Computing, 11(4):381-401, 1999.

117

R. M. Hierons.
Testing from a Z specification.
Software Testing, Verification and Reliability, 7(1):19-33, March 1997.

118

M. G. Hinchey and J. P. Bowen.
Applications of Formal Methods.
International Series in Computer Science. Prentice Hall, 1995.

119

M. G. Hinchey and Shaoying Liu (Eds).
First International Conference on Formal Engineering Methods (ICFEM'97), Hiroshima, Japan, November 1997. IEEE Computer Society Press.

120

C. A. R. Hoare.
Proof of correctness of data representations.
Acta Informatica, 1:271-281, 1972.

121

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

122

C. A. R. Hoare, He Jifeng, and J. W. Sanders.
Prespecification in data refinement.
Information Processing Letters, 25(2):71-76, May 1987.

123

H.-M. Hörcher.
Improving software tests using Z specifications.
In ZUM'95 [34], pp 152-166.

124

ISO/IEC.
Z notation: Final committee draft.
International Standard CD 13568.2, International Standards Organization, 1999.

125

D. Jackson.
Structuring Z specifications with views.
ACM Transactions on Software Engineering and Methodology, 4(4):365-389, October 1995.

126

J. Jacky.
The Way of Z: Practical Programming with Formal Methods.
Cambridge University Press, 1997.

127

J. Jacky, J. Unger, M. Patrick, R. Reid, and R. Risler.
Experience with Z developing a control program for a radiation therapy machine.
In ZUM'97 [35], pp 317-328.

128

H. M. Järvinen and R. Kurki-Suonio.
DisCo specification language: Marriage of actions and objects.
In 11th International Conference on Distributed Computing Systems, pp 142-151, Washington, D.C., USA, May 1991. IEEE Computer Society Press.

129

He Jifeng.
Process refinement.
In J. McDermid (Ed), The Theory and Practice of Refinement. Butterworths, 1989.

130

C. B. Jones.
Software Development: A Rigorous Approach.
Prentice Hall, 1980.

131

C. B. Jones.
Systematic Software Development using VDM.
Prentice Hall, 1989.

132

C. B. Jones and R. C. F. Shaw (Eds).
Case studies in Systematic Software Development.
Prentice Hall, 1990.

133

M. B. Josephs.
The data refinement calculator for Z specifications.
Information Processing Letters, 27:29-33, February 1988.

134

M. B. Josephs.
A state-based approach to communicating processes.
Distributed Computing, 3:9-18, 1988.

135

M. B. Josephs.
Specifying reactive systems in Z.
Technical Report PRG-19, Programming Research Group, Oxford University Computing Laboratory, 1991.

136

S. King.
`The standard logic for Z': A clarification.
Formal Aspects of Computing, 11(4):472-473, 1999.

137

S. King, J. Hammond, R. Chapman, and A. Prior.
The value of verification: Positive experience of industrial proof.
In FM'99 [206], pp 1527-1545.

138

G. J. Klinker.
An environment for telecollaborative data exploration.
In Proceedings Visualization '93 - sponsored by the IEEE Computer Society, pp 110-117, 1993.

139

L. Lamport.
The temporal logic of actions.
ACM Transactions on Programming Languages and Systems, 16(3):872-923, May 1994.

140

L. Lamport and F. B. Schneider.
Pretending atomicity.
Technical Report 44, Compaq Systems Research Center, May 1989.

141

K. Lano.
The B Language and Method.
FACIT. Springer, 1996.

142

K. Lano.
Specifying reactive systems in B AMN.
In ZUM'97 [35], pp 242-274.

143

K. Lano and K. Androutsopoulos.
Reactive system refinement of distributed systems in B.
In IFM'99 [8], pp 415-434.

144

K. Lano and S. Goldsack.
Refinement of distributed object systems.
In E. Najm and J.-B. Stefani (Eds), First IFIP International Workshop on Formal Methods for Open Object-Based Distributed Systems, pp 99-114, Paris, March 1996. Chapman & Hall.

145

K. Lano and H. Haughton (Eds).
Object Oriented Specification Case Studies.
Prentice Hall, 1994.

146

G. Leduc.
On the Role of Implementation Relations in the Design of Distributed Systems using LOTOS.
PhD thesis, University of Liège, Liège, Belgium, June 1991.

147

R. J. Lipton.
Reduction: A method of proving properties of parallel programs.
Communications of the ACM, 18(12):717-721, December 1975.

148

B. Liskov and J. M. Wing.
A behavioural notion of subtyping.
ACM Transactions on Programming Languages and Systems, 16(6):1811-1841, 1994.

149

B. Liskov and J. M. Wing.
Specifications and their use in defining subtypes.
In ZUM'95 [34], pp 245-263.

150

P. J. Lupton.
Promoting forward simulation.
In ZUM'90 [164], pp 27-49.

151

N. A. Lynch.
Multivalued possibility mappings.
In REX'89 [56], pp 519-543.

152

N. A. Lynch and F. Vaandrager.
Forward and backward simulations for timing-based systems.
In J. W. de Bakker, W.-P. de Roever, C. Huizing, and G. Rozenberg (Eds), Real-Time: Theory in Practice (REX Workshop, Mook, The Netherlands, June 1991), LNCS 600, pp 397-446. Springer-Verlag, 1992.

153

B. P. Mahony.
The least conjunctive refinement and promotion in the refinement calculus.
Formal Aspects of Computing, 11(1):75-105, 1999.

154

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 (Eds), 20th International Conference on Software Engineering (ICSE'98). IEEE Press, 1998.

155

B. P. Mahony and J. S. Dong.
Timed communicating Object-Z.
IEEE Transactions on Software Engineering, 26(2):150-177, February 2000.

156

S. L. Meira and A. L. C. Cavalcanti.
Modular object oriented Z specifications.
In ZUM'90 [164], pp 173-192.

157

M. Merritt.
Completeness theorems for automata.
In REX'89 [56], pp 544-560.

158

R. Miarka, E. A. Boiten, and J. Derrick.
Guards, preconditions and refinement in Z.
In ZB 2000 [31], pp 286-303.

159

A. Mikhajlova and E. Sekerinski.
Class refinement and interface refinement in object-oriented programs.
In FME'97 [90], pp 82-101.

160

R. Milner.
Communication and Concurrency.
Prentice-Hall, 1989.

161

C. C. Morgan.
Programming from Specifications.
Prentice Hall International Series in Computer Science, 2nd edition, 1994.

162

L. Murray, D. Carrington, I. MacColl, J. McDonald, and P. Strooper.
Formal derivation of finite state machines for class testing.
In ZUM'98 [32], pp 42-59.

163

M. Naftalin, T. Denvir, and M. Bertran (Eds).
FME'94: Industrial Benefit of Formal Methods, Second International Symposium of Formal Methods Europe, volume 873 of Lecture Notes in Computer Science, Berlin, 1994. Springer-Verlag.

164

J. E. Nicholls (Ed).
Z User Workshop, Oxford 1990, Workshops in Computing. Springer-Verlag, 1990.

165

T. Nipkow.
Formal verification of data type refinement -- Theory and practice.
In REX'89 [56], pp 561-591.

166

B. Potter, J. Sinclair, and D. Till.
An Introduction to Formal Specification and Z.
International Series in Computer Science. Prentice Hall, 1991.
2nd ed., 1996.

167

Monty Python.
The Meaning of Life.
1983.

168

G. H. B. Rafsanjani.
ZEST - Z Extended with Structuring: A users's guide.
Technical report, BT, June 1994.

169

B. Ratcliff.
Introducing Specification using Z: A Practical Case Study Approach.
McGraw-Hill, 1994.

170

J. C. Roberts.
On encouraging multiple views for visualization.
In Information Visualization IV'98, London, July 1998. IEEE Computer Society.

171

A. W. Roscoe, J. C. P. Woodcock, and L. Wulf.
Non-interference through determinism.
Journal of Computer Security, 4(1):27-54, 1996.

172

A.W. Roscoe.
The Theory and Practice of Concurrency.
International Series in Computer Science. Prentice Hall, 1998.

173

S. Schneider.
Concurrent and Real-Time Systems: The CSP Approach.
Wiley, 2000.

174

G. T. Scullard.
Test case selection using VDM.
In VDM '88 VDM - The Way Ahead, pp 178-186, September 1988.

175

E. Sekerinski and K. Sere (Eds).
Program Development by Refinement - Case Studies Using the B Method.
FACIT. Springer, 1999.

176

K. Sere and M. Walden.
Data refinement of remote procedures.
In International Symposium on Theoretical Aspects of Computer Software (TACS'97), number 1281 in Lecture Notes in Computer Science, pp 267-294. Springer-Verlag, 1997.

177

H. Singh, M. Conrad, and S. Sadeghipour.
Test case design based on Z and the classification-tree method.
In ICFEM'97 [119], pp 81-90.

178

G. Smith.
Extending W for Object-Z.
In ZUM'95 [34], pp 276-295.

179

G. Smith.
A fully abstract semantics of classes for Object-Z.
Formal Aspects of Computing, 7(3):289-313, 1995.

180

G. Smith.
A semantic integration of Object-Z and CSP for the specification of concurrent systems.
In FME'97 [90], pp 62-81.

181

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

182

G. Smith and J. Derrick.
Refinement and verification of concurrent systems specified in Object-Z and CSP.
In ICFEM'97 [119], pp 293-302.

183

G. Smith and J. Derrick.
Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP.
Formal Methods in System Design, 2001.
To appear.

184

G. Smith and I. J. Hayes.
Towards real-time Object-Z.
In IFM'99 [8], pp 49-65.

185

J. F. Sogaard-Andersen, N. A. Lynch, and B. W. Lampson.
Correctness of communication protocols - A case study.
Technical report, Laboratory for Computer Science, MIT, November 1993.

186

J. M. Spivey.
Understanding Z: A Specification Language and its Formal Semantics.
Cambridge University Press, 1988.

187

J. M. Spivey.
The Z Notation: A Reference Manual.
International Series in Computer Science. Prentice Hall, 1989.

188

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

189

S. Stepney.
Testing as Abstraction.
In ZUM'95 [34], pp 137-151.

190

S. Stepney, R. Barden, and D. Cooper (Eds).
Object Orientation in Z.
Workshops in Computing. Springer-Verlag, 1992.

191

S. Stepney, R. Barden, and D. Cooper.
A survey of object orientation in Z.
Software Engineering Journal, 7(2):150-160, 1992.

192

S. Stepney and D. Cooper.
Formal methods for industrial products.
In ZB 2000 [31], pp 374-393.

193

S. Stepney, D. Cooper, and J. C. P. Woodcock.
More powerful data refinement in Z.
In ZUM'98 [32], pp 284-307.

194

P. Stocks.
Applying Formal Methods to Software Testing.
PhD thesis, Department of Computer Science, University of Queensland, St. Lucia 4072, Australia, 1993.

195

D. W. J. Stringer-Calvert, S. Stepney, and I. Wand.
Using PVS to prove a Z refinement: A case study.
In FME'97 [90], pp 573-588.

196

B. Strulo, 1995.
Email communication.

197

B. Strulo.
How firing conditions help inheritance.
In ZUM'95 [34], pp 264-275.

198

B. Sufrin and J. He.
Specification, refinement, and analysis of interactive processes.
In M. D. Harrison and H. W. Thimbleby (Eds), Formal Methods in Human Computer Interaction, pp 153-200. Cambridge University Press, 1990.

199

K. Taguchi and K. Araki.
The state-based CCS semantics for concurrent Z specification.
In ICFEM'97 [119], pp 283-292.

200

I. Toyn.
Innovations in standard Z notation.
In ZUM'98 [32], pp 193-213.

201

H. Treharne and S. Schneider.
Using a process algebra to control B operations.
In IFM'99 [8], pp 437-456.

202

L. van Aertryck, M. Benveniste, and D. Le Metayer.
Casting: A formally based software test generation method.
In ICFEM'97 [119], pp 101-110.

203

R. J. van Glabbeek.
Comparative Concurrency Semantics and Refinement of Actions.
PhD thesis, Vrije Universiteit, Amsterdam, 1990.

204

H. Wehrheim.
Behavioural subtyping and property preservation.
In S. F. Smith and C. L. Talcott (Eds), Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000), pp 213-231. Kluwer, September 2000.

205

C. Wezeman and A. J. Judge.
Z for managed objects.
In ZUM'94 [33], pp 108-119.

206

J. M. Wing, J. C. P. Woodcock, and J. Davies (Eds).
FM'99 World Congress on Formal Methods in the Development of Computing Systems, volume 1708 of Lecture Notes in Computer Science, Berlin, 1999. Springer-Verlag.

207

J. C. P. Woodcock.
Mathematics as a management tool: Proof rules for promotion.
In CSR Sixth Annual Conference on Large Software Systems. Elsevier, 1989.

208

J. C. P. Woodcock.
Industrial-strength refinement.
In IRW/FMP'98 [104], pp 33-44.

209

J. C. P. Woodcock and J. Davies.
Using Z: Specification, Refinement, and Proof.
Prentice Hall, 1996.

210

J. C. P. Woodcock and B. Dickinson.
Using VDM with rely and guarantee-conditions: Experiences of a real project.
In VDM'88, pp 434-458, 1988.

211

J. C. P. Woodcock and C. C. Morgan.
Refinement of state-based concurrent systems.
In D. Bjorner, C. A. R. Hoare, and H. Langmaack (Eds), VDM'90: VDM and Z!- Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

212

H. B. Zadeh.
Using ZEST for Specifying Managed Objects.
Technical report, British Telecom, January 1996.

213

P. Zave and M. Jackson.
Conjunction as composition.
ACM Transactions on Software Engineering and Methodology, 2(4):379-411, October 1993.

214

P. Zave and M. Jackson.
Where do operations come from? A multiparadigm specification technique.
IEEE Transactions on Software Engineering, 22(7):508-528, July 1996.