Abstract
This bibliography contains a list of references concerned with the formal Z notation that are either available as published papers, books, selected technical reports, or on-line. Some references on the related B-Method are also included. The bibliography is in alphabetical order by author name(s).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Z bibliography (1990) (onwards), http://www.comlab.ox.ac.uk/archive/z/bib.html (This bibliography is maintained in BibTEX database source format accessible in searchable form on the World Wide Web. To add entries, please send as complete information as possible to Jonathan Bowen on J.P.Bowen@reading.ac.uk)
Abowd, G.D.: Agents: Communicating interactive processes. In: Diaper, D., Gilmore, D., Cockton, G., Shackel, B. (eds.) Human-Computer Interaction: INTERACT 1990, pp. 143–148. Elsevier Science Publishers, North-Holland (1990)
Abowd, G.D.: Formal Aspects of Human-Computer Interaction. DPhil thesis, Oxford University Computing Laboratory,Wolfson Building, Parks Road, Oxford, UK (1991)
Abowd, G.D., Allen, R., Garlan, D.: Using style to understand descriptions of software architectures. ACM Software Engineering Notes 18(5), 9–20 (1993)
Abowd, G.D., Allen, R., Garlan, D.: Formalizing style to understand descriptions of software architecture. ACM Transactions on Software Engineering and Methodology (TOSEM) 4(4), 319–364 (1995) (The formal model is described using the Z specification language)
Abrial, J.-R.: Data semantics. In: Klimbie, J.W., Koffeman, K.L. (eds.) IFIP TC2 Working Conference on Data Base Management, April 1974, pp. 1–59. Elsevier Science Publishers, North-Holland (1974) (A seminal paper for the formal Z notation, as noted in [303])
Abrial, J.-R.: The B tool. In: Bloomfield, et al. [54], pp. 86–87
Abrial, J.-R.: The B method for large software, specification, design and coding (abstract). In: Prehn, Toetenel [531], pp. 398–405
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996) (This book is a reference manual for the B-Method developed by Jean-Raymond Abrial, also the originator of the Z notation. B is designed for tool-assisted software development whereas Z is designed mainly for specification. Contents: Mathematical reasoning; Set notation; Mathematical objects; Introduction to abstract machines; Formal definition of abstract machines; Theory of abstract machines; Constructing large abstract machines; Example of abstract machines; Sequencing and loop; Programming examples; Refinement; Constructing large software systems; Example of refinement; Appendices: Summary of the most current notations; Syntax; Definitions; Visibility rules; Rules and axioms; Proof obligations)
Abrial, J.-R., Börger, E., Langmaack, H. (eds.): Dagstuhl Seminar 1995. LNCS, vol. 1165. Springer, Heidelberg (1996) (A comparative collection of formal methods case studies. See [126,565])
Abrial, J.-R., Schuman, S.A., Meyer, B.: Specification language. In: McKeag, R.M., Macnaghten, A.M. (eds.) On the Construction of Programs: An Advanced Course, pp. 343–410. Cambridge University Press, Cambridge (1980)
Abrial, J.-R., Sørensen, I.H.: KWIC-index generation. In: Staunstrup, J. (ed.) Program Specification 1981. LNCS, vol. 134, pp. 88–95. Springer, Heidelberg (1982)
Achatz, K., Schulte, W.: A formal OO method inspired by Fusion and Object-Z. In: Bowen et al. [101], pp. 92–111
Ainsworth, M., Cruickshank, A.H., Wallis, P.J.L., Groves, L.J.: Viewpoint specification and Z. Information and Software Technology 36(1), 43–51 (1994)
Alencar, A.J., Goguen, J.A.: OOZE: An object-oriented Z environment. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 180–199. Springer, Heidelberg (1991)
Ardis, M.A., Chaves, J.A., Jagadeesan, L.J., Mataga, P., Puchol, C., Staskauskas, M.G., von Olnhausen, J.: A framework for evaluating specification methods for reactive systems experience report. IEEE Transactions on Software Engineering 22(6), 378–389 (1996) (Several different methods, including Modechart, VFSM, Esterel, Basic LOTOS, Z, SDL, and C, are applied to a problem encountered in the design of software for AT&T’s 5ESS telephone switching system)
Arnold, D.B., Duce, D.A., Reynolds, G.J.: An approach to the formal specification of configurable models of graphics systems. In: Maréchal, G. (ed.) Proc. EUROGRAPHICS 1987, European Computer Graphics Conference and Exhibition, pp. 439–463. Elsevier Science Publishers, North-Holland (1987) (The paper describes a general framework for the formal specification of modular graphics systems, illustrated by an example taken from the Graphical Kernel System (GKS) standard)
Arnold, D.B., Reynolds, G.J.: Configuring graphics systems components. IEE/BCS Software Engineering Journal 3(6), 248–256 (1988)
Arthan, R.D.: Formal specification of a proof tool. In: Prehn, Toetenel [530], pp. 356–370
Arthan, R.D.: On free type definitions in Z. In: Nicholls [506], pp. 40–58
Arthan, R.D.: Recursive definitions in Z. In: Bowen et al. [85], pp. 154–171
Ashoo, K.: The Genesis Z tool – an overview. BCS-FACS FACTS, Series II 3(1), 11–13 (1992)
Atkinson, S., Scholefield, D.: Transformational vs reactive refinement in realtime systems. Information Processing Letters 55(4), 201–210 (1995)
Aujla, S., Bryant, A., Semmens, L.: A rigorous review technique: Using formal notations within conventional development methods. In: Katsolakos [393], pp. 247–255
Austin, P.B., Murray, K.A., Wellings, A.J.: File system caching in large pointto- point networks. IEE/BCS Software Engineering Journal 7(1), 65–80 (1992)
Austin, S., Parkin, G.I.: Formal methods: A survey. Technical report, National Physical Laboratory, Queens Road, Teddington, Middlesex, TW11 0LW, UK (March 1993)
Bailes, C., Duke, R.: The ecology of class refinement. In: Morris, Shaw [487], pp. 185–196
Bailey, M.: Formal specification using Z. In: Proc. Software Engineering anniversary meeting (SEAS), p. 99 (1987)
Bainbridge, J., Whitty, R.W., Wordsworth, J.B.: Obtaining structural metrics of Z specifications for systems development. In: Nicholls [504], pp. 269–281
Banâtre, J.-P.: About programming environments. In: Banâtre, J.-P., Jones, S.B., de Métayer, D. (eds.) Prospects for Functional Programming in Software Engineering. ch. 1, pp. 1–22. Springer, Heidelberg (1991)
Bancroft, P., Hayes, I.J.: A formal semantics for a language with type extension. In: Bowen, Hinchey [99], pp. 299–314
Barden, R., Stepney, S.: Support for using Z. In: Bowen, Nicholls [102], pp. 255–280
Barden, R., Stepney, S., Cooper, D.: The use of Z. In: Nicholls [506], pp. 99–124
Barden, R., Stepney, S., Cooper, D.: Z in Practice. BCS Practitioner Series. Prentice-Hall, Englewood Cliffs (1994)
Barrett, G.: Formal methods applied to a floating-point number system. IEEE Transactions on Software Engineering 15(5), 611–621 (1989) (A formalization of the IEEE standard for binary floating-point arithmetic in Z is presented. The formal specification is refined into four components. The procedures presented form the basis for the floating-point unit of the Inmos IMS T800 Transputer. This work resulted in a joint UK Queen’s Award for Technological Achievement for Inmos Ltd and the Oxford University Computing Laboratory in 1990. It was estimated that the approach saved a year in development time compared to traditional methods)
Barroca, L.M., Fitzgerald, J.S., Spencer, L.: The architectural specification of an avionic subsystem. In: France, Gerhart [265], pp. 17–29
Barroca, L.M., McDermid, J.A.: Formal methods: Use and relevance for the development of safety-critical systems. The Computer Journal 35(6), 579–599 (1992)
Bates, B.W., Bruel, J.-M., France, R.B., Larrondo-Petrie, M.M.: Guidelines for formalizing Fusion object-oriented analysis models. In: Constantopoulos, P., Vassiliou, Y., Mylopoulos, J. (eds.) CAiSE 1996. LNCS, vol. 1080, pp. 222–233. Springer, Heidelberg (1996)
Baumann, P.: Z and natural semantics. In: Bowen, Hall [91], pp. 168–184
Baumann, P., Lermer, K.: A framework for the specification of reactive and concurrent systems in Z. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 62–79. Springer, Heidelberg (1995)
Baumann, P., Lermer, K.: Specifying parallel and distributed real-time systems in Z. In: Proc. 4th International Workshop on Parallel and Distributed Real-Time Systems, Hawaii, April 1996, pp. 216–222 (1996)
Benjamin, M.: A message passing system: An example of combining CSP and Z. In: Nicholls [502], pp. 221–228
Benveniste, M.: Writing operational semantics in Z: A structural approach. In: Prehn, Toetenel [530], pp. 164–188
Bera, S.: Structuring for the VDM specification language. In: Bloomfield et al. [54], pp. 2–25
Bernard, P., Laffitte, G.: The French population census for. In: Bowen, Hinchey [99], pp. 334–352 (1990)
Bert, D. (ed.): B 1998. LNCS, vol. 1393. Springer, Heidelberg (1998)
Bicarregui, J., Dick, J., Woods, E.: Supporting the length of formal development: From diagrams to VDM to B to C. In: Habrias [303], pp. 63–75
Bicarregui, J., Dick, J., Woods, E.: Quantitative analysis of formal methods. In: Gaudel, Woodcock [280], pp. 60–73
Bicarregui, J., Ritchie, B.: Invariants, frames and postconditions: A comparison of the VDM and B notations. IEEE Transactions on Software Engineering 21(2), 79–89 (1995)
Bishop, P.G. (ed.): Fault Avoidance, ch. 3. Applied Science, pp. 56–140. Elsevier Science Publishers, Amsterdam (1990) (Section 3.88 (pages 94–96) provides an overview of Z. Other sections describe related techniques)
Bjørner, D., Hoare, C.A.R., Langmaack, H. (eds.): VDM 1990. LNCS, vol. 428. Springer, Heidelberg (1990) (The 3rd VDM-Europe Symposium was held at Kiel, Germany, 17–21 April 1990. A significant number of papers concerned with Z were presented [138,231,277,194,294,308,399,562,607,660,692])
Bloesch, A., Kazmierczak, E., Kearney, P., Traynor, O.: Cogito: A methodology and system for formal software-development. International Journal of Software Engineering and Knowledge Engineering 5(4), 599–617 (1995)
Bloom, B., Cheng, A., Dsouza, A.: Using a Protean language to enhance expressiveness in specification. IEEE Transactions on Software Engineering 23(4), 224–234 (1997)
Bloomfield, R., Marshall, L., Jones, R. (eds.): VDM – The Way Ahead, VDM-Europe. LNCS, vol. 328. Springer, Heidelberg (1988) (The 2nd VDM-Europe Symposium was held at Dublin, Ireland, 11–16 September 1988. See [7,44])
Boiten, E.A., Bowman, H., Derrick, J., Steen, M.: Issues in multiparadigm viewpoint specification. In: Finkelstein, A., Spanoudakis, G. (eds.) SIGSOFT 1996 International Workshop on Multiple Perspectives in Software Development (Viewpoints 1996), pp. 162–166. ACM, New York (1996)
Boiten, E.A., Bowman, H., Derrick, J., Steen, M.: Viewpoint consistency in Z and LOTOS: A case study. In: Fitzgerald et al. [260], pp. 644–664 (The 4th FME Symposium was held at Graz, Austria, 15–19 September 1997. See the Z-related paper [56])
Boiten, E.A., Derrick, J., Bowman, H., Steen, M.: Unification and multiple views of data in Z. In: van Vliet, J.C. (ed.) Proc. Computing Science in the Netherlands, November 1995, pp. 73–85 (1995)
Boiten, E.A., Derrick, J., Bowman, H., Steen, M.: Consistency and refinement for partial specifications in Z. In: Gaudel, Woodcock [280], pp. 287–306
Boiten, E.A., Derrick, J., Bowman, H., Steen, M.: Coupling schemas: Data refinement and view(point) composition. In: Duke, D.J., Evans, A.S. (eds.) Northern Formal Methods Workshop, Electronic Workshops In Computing, Springer, Heidelberg (1997)
Börger, E., Mazzanti, S.: A practical method for rigorously controllable hardware design. In: Bowen et al. [101], pp. 151–187
Bosch, J., Mitchell, S. (eds.): ECOOP 1997 Workshops. LNCS, vol. 1357. Springer, Heidelberg (1998) (See Z-related papers [152,243,264])
Boswell, A.: Specification and validation of a security policy model. In: Woodcock, Larsen [689], pp. 42–51 (The 1st FME Symposium was held at Odense, Denmark, 19–23 April 1993. Zrelated papers include [103,165,254,372,447,526])
Boswell, A.: Specification and validation of a security policy model. IEEE Transactions on Software Engineering 21(2), 99–106 (1995) (This paper describes the development of a formal security model in Z for the NATO Air Command and Control System (ACCS): a large, distributed, multilevel-secure system. The model was subject to manual validation, and some of the issues and lessons in both writing and validating the model are discussed)
Bottaci, L., Jones, J.: Formal Specification Using Z: A Modelling Approach. International Thomson Publishing, London (1995)
Bowen, J.P.: Formal specification and documentation of microprocessor instruction sets. Microprocessing and Microprogramming 21(1-5), 223–230 (1987)
Bowen, J.P.: The formal specification of a microprocessor instruction set. Technical Monograph PRG-60, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (January 1987) (The Z notation is used to define the Motorola M6800 8-bit microprocessor instruction set)
Bowen, J.P. (ed.): Proc. Z Users Meeting, 1Wellington Square, Oxford, Wolfson Building, Parks Road, Oxford, UK, December 1987. Oxford University Computing Laboratory (1987) (Proceedings of the 2nd Z User Meeting, Department of External Studies, Rewley House, Oxford, UK, Friday 8 December 1987. Note that there were no written proceedings for the 1st Z User Meeting, held in Oxford, December 1986)
Bowen, J.P.: Formal specification in Z as a design and documentation tool. In: Proc. 2nd IEE/BCS Conference on Software Engineering, July 1988. Conference Publication, vol. 290, pp. 164–168. IEE/BCS (1988)
Bowen, J.P. (ed.): Proc. Third Annual Z Users Meeting,Wolfson Building, Parks Road, Oxford, UK (December 1988), Oxford University Computing Laboratory. Proceedings of the 3rd Z User Meeting, Department of External Studies, Rewley House, Oxford, UK, Friday 16 December 1988. Issued with A Miscellany of Handy Techniques by R. Macdonald, Practical Experience of Formal Specification: A programming interface for communications by J. B. Wordsworth, and a number of posters
Bowen, J.P.: Formal specification of window systems. Technical Monograph PRG- 74, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (June 1989); Three window systems, X from MIT, WM from Carnegie-Mellon University and the Blit from AT&T Bell Laboratories are covered
Bowen, J.P.: POS: Formal specification of a UNIX tool. IEE/BCS Software Engineering Journal 4(1), 67–72 (1989)
Bowen, J.P.: Formal specification of the ProCoS/safemos instruction set. Microprocessors and Microsystems 14(10), 631–643 (1990); This article is part of a special feature on Formal aspects of microprocessor design, edited by H. S. M. Zedan. See also [574]
Bowen, J.P.: X: Why Z? Computer Graphics Forum 11(4), 221–234 (1992); This paper asks whether window management systems would not be better specified through a formal methodology and gives examples in Z of the X Window System
Bowen, J.P.: Formal methods in safety-critical standards. In: Katsolakos [393], pp. 168–177
Bowen, J.P.: Report on Z User Meeting, London 1992. BCS-FACS FACTS, Series III 1(3), 7–8 (1993); Other versions of this report appeared as follows: – Z User Meetings, Safety Systems: The Safety-Critical Systems Club Newsletter 3(1), 13 (September 1993); – Z User Group activities, JFIT News 46, 5 (September 1993), – Report on Z User Meeting, Information and Software Technology 35(10), 613 (October 1993) – Z User Meeting Activities, High Integrity Systems 1(1), 93–94 (1994)
Bowen, J.P.: Glossary of Z notation. Information and Software Technology 37(5-6), 333–334 (1995)
Bowen, J. P.: Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press, 1996. Contents: Foreword; Preface; Part I: Introduction – Chapter 1: Formal Specification using Z, Chapter 2: Industrial Use of Formal Methods, Chapter 3: A Brief Introduction to Z; Part II: Network Services – Chapter 4: Documentation using Z, Chapter 5: A File Storage Service; Part III: UNIX Software – Chapter 6: A Text Formatting Tool, Chapter 7: An Event-based Input System; Part IV: Instruction Sets – Chapter 8: Machine Words, Chapter 9: The Transputer Instruction Set; Part V: Graphics – Chapter 10: Basic Graphical Concepts, Chapter 11: Raster- Op Functions; Part VI: Window Systems – Chapter 12: The ITC ‘WM’ Window Manager, Chapter 13: Blit Windows, Chapter 14: The X Window System, Chapter 15: Formal Specification of Existing Systems; Appendices – A: Information on Z, B: Z Glossary, C: Literature Guide
Bowen, J.P.: Comp.specification.z and Z FORUM frequently asked questions. In: Bowen et al. [101], pp. 425–433
Bowen, J.P.: Select Z bibliography. In: Bowen et al. [101], pp. 391–424
Bowen, J.P.: Comp.specification.z and Z FORUM frequently asked questions. In: Bowen et al. [85], pp. 407–415
Bowen, J.P.: Select Z bibliography. In: Bowen et al. [85], pp. 367–406
Bowen, J.P., Breuer, P.T., Lano, K.C.: A compendium of formal techniques for software maintenance. IEE/BCS Software Engineering Journal 8(5), 253–262 (1993)
Bowen, J.P., Breuer, P.T., Lano, K.C.: Formal specifications in software maintenance: From code to Z + + and back again. Information and Software Technology 35(11/12), 679–690 (1993)
Bowen, J.P., Chippington, D.: Z on the Web using Java. In: Bowen et al. [85], pp. 66–80
P. Bowen, J., Fett, A., Hinchey, M.G. (eds.): ZUM 1998. LNCS, vol. 1493. Springer, Heidelberg (1998); Proceedings of the 11th Z User Meeting, Technical University of Berlin, Germany. For individual papers presented at the main conference, see [21,84,149,188,242,259,269,301,342,375,425,429,440,443,489,516,517,564,598,615] [624,651,659]. The proceedings also includes as appendices this bibliography [81] and a section answering Frequently Asked Questions [80]
Bowen, J.P., Gimson, R.B., Topp-Jørgensen, S.: The specification of network services. Technical Monograph PRG-61, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (August 1987)
Bowen, J.P., Gimson, R.B., Topp-Jørgensen, S.: Specifying system implementations in Z. Technical Monograph PRG-63, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (February 1988)
Bowen, J.P., Gordon, M.J.C.: Z and HOL. In: Bowen and Hall [91], pp. 141–167
Bowen, J.P., Gordon, M.J.C.: A shallow embedding of Z in HOL. Information and Software Technology 37(5-6), 269–276 (1995); Revised version of [88]
Bowen, J.P., Gordon, M.J.C.: A shallow embedding of Z in HOL. Information and Software Technology 37(5-6), 269–276 (1995)
Bowen, J.P., Hall, J.A. (eds.): Z User Workshop, Cambridge 1994, Workshops in Computing. Springer-Verlag, 1994. Proceedings of the 8th Z User Meeting, St. John’s College, Cambridge, UK. Published in collaboration with the British Computer Society. For individual papers, see [39,88,110,137,139,198,246,248,275,309,312,317,321,409,449,524,591,668,688,694].The proceedings also includes an Introduction and Opening Remarks, a Select Z Bibliography and a section answering Frequently Asked Questions
Bowen, J.P., Jifeng, H., Hale, R.W.S., Herbert, J.M.J.: Towards verified systems: The SAFEMOS project. In: Mitchell, C.J., Stavridou, V. (eds.) The Mathematics of Dependable Systems. The Institute of Mathematics and its Applications Conference Series, vol. 55, pp. 23–48. Oxford University Press, Oxford (1995)
Bowen, J.P., Hinchey, M.G.: Formal methods and safety-critical standards. IEEE Computer 27(8), 68–71 (1994)
Bowen, J.P., Hinchey, M.G.: Seven more myths of formal methods: Dispelling industrial prejudices. In: Naftalin et al. [490], pp. 105–117
Bowen, J.P., Hinchey, M.G.: Editorial. Information and Software Technology 37(5-6), 258–259 (1995); A special issue on Z. See [76,96,89,105,276,424,446,451,654]
Bowen, J.P., Hinchey, M.G.: Report on Z User Meeting (ZUM 1994). Information and Software Technology 37(5-6), 335–336 (1995)
Bowen, J.P., Hinchey, M.G.: Seven more myths of formal methods. IEEE Software 12(4), 34–41 (1995); This article deals with further myths in addition to those presented in [307]. Previous versions issued as: – Technical Report PRG-TR-7-94, Oxford University Computing Laboratory (June 1994) – Technical Report 357, University of Cambridge, Computer Laboratory (January 1995)
Bowen, J.P., Hinchey, M.G.: Ten commandments of formal methods. IEEE Computer 28(4), 56–63 (1995); Previously issued as: Technical Report 350, University of Cambridge, Computer Laboratory (September 1994)
Bowen, J.P., Hinchey, M.G. (eds.): ZUM 1995. LNCS, vol. 967. Springer, Heidelberg (1995); Proceedings of the 9th Z User Meeting, University of Limerick, Ireland. For individual papers presented at the main conference, see [31,45,120,144,180,193,213,245,266,284,292,311,353,357,376,407,432,436,441,463] [520,543,552,592,611,628,658,665]. Some papers formed part of an associated Educational Issues Session organized by Neville Dean [143,181,300,465,521,673]. The proceedings also includes as appendices a Select Z Bibliography and a section answering Frequently Asked Questions
Bowen, J.P., Hinchey, M.G.: Formal models and the specification process. In: Tucker Jr., A.B. (ed.) The Computer Science and Engineering Handbook, vol. ch. 107, pp. 2302–2322. CRC Press, Boca Raton (1997); Section X, Software Engineering
Till, D., P. Bowen, J., Hinchey, M.G. (eds.): ZUM 1997. LNCS, vol. 1212. Springer, Heidelberg (1997); Proceedings of the 10th Z User Meeting, The University of Reading, UK. For individual papers presented at the main conference, see [13,60,130,148,191,201,249,310,306,339,340,345,377,402,406,416,412,554,623]. The proceedings also includes as appendices a Select Z Bibliography [79] and a section answering Frequently Asked Questions [78]
Bowen, J.P., Nicholls, J.E. (eds.) Z User Workshop, London 1992, Workshops in Computing, Springer, Heidelberg (1993); Proceedings of the 7th Z User Meeting, DTI Offices, London, UK. Published in collaboration with the British Computer Society. For individual papers, see [32,108,160,167,176,174,225,335,371,403,421,434,452,507,513,532,550,638,656]. The proceedings also includes an Introduction and Opening Remarks, a Select Z Bibliography and a section answering Frequently Asked Questions
Bowen, J.P., Stavridou, V.: The industrial take-up of formal methods in safety-critical and other areas: A perspective. In: Woodcock and Larsen [689], pp. 183–195
Bowen, J.P., Stavridou, V.: Safety-critical systems, formal methods and standards. IEE/BCS Software Engineering Journal 8(4), 189–209 (1993); A survey on the use of formal methods, including B and Z, for safety-critical systems. Winner of the 1994 IEE Charles Babbage Premium award. A previous version is also available as Oxford University Computing Laboratory Technical Report PRG-TR-5-92
Bowen, J.P., Stepney, S., Barden, R.: Annotated Z bibliography. Information and Software Technology 37(5-6), 317–332 (1995); See also Literature Guide, Appendix C, pages 239–251 of [77]
Bowman, H., Derrick, J.: Modelling distributed systems using Z. In: George, K.M. (ed.) ACM Symposium on Applied Computing, February 1995, pp. 147–151. ACM Press, New York (1995)
Bowman, H., Derrick, J., Linington, P., Steen, M.: FDTs for ODP. Computer Standards & Interfaces 17(5-6), 457–479 (1995)
Bradley, A.: Requirements for Defence Standard 00-55. In: Bowen and Nicholls [102], pp. 93–94
Breuer, P.T.: Z! in progress: Maintaining Z specifications. In: Nicholls [504], pp. 295–318
Breuer, P.T., Bowen, J.P.: Towards correct executable semantics for Z. In: Bowen and Hall [91], pp. 185–209
Brien, S.M.: The development of Z. In: Andrews, D.J., Groote, J.F., Middelburg, C.A. (eds.) Semantics of Specification Languages (SoSL), Workshops in Computing, pp. 1–14. Springer, Heidelberg (1994)
Brien, S.M., Nicholls, J.E.: Z base standard. Technical Monograph PRG-107, Oxford University Computing Laboratory,Wolfson Building, Parks Road, Oxford, UK, November 1992. Accepted for standardization under ISO/IEC JTC1/SC22. This is the first publicly available version of the proposed ISO Z Standard. The latest draft is Version 1.2 (September 1995), See also [604] for a widely used Z reference manual
Britton, C., Loomes, M., Mitchell, R.: Formal specification as constructive diagrams. Microprocessing and Microprogramming 37(1-5), 175–178 (1993)
Brossard-Guerlus, M., Klay, F.: Introducing formal specification in an industrial context: An experiment in Z. In: Habrias [303], pp. 229–242
Brown, D.J., Bowen, J.P.: The Event Queue: An extensible input system for UNIX workstations. In: Proc. European Unix Users Group Conference, Helsinki, Finland, May 12-14, pp. 29–52 (1987)
Brownbridge, D.: Using Z to develop a CASE toolset. In: Nicholls [502], pp. 142–149
Bruel, J.-M., Benzekri, A., Raymaud, Y.: Z and the specification of real-time systems. In: Habrias [303], pp. 77–91
Bryant, A.: Structured methodologies and formal notations: Developing a framework for synthesis and investigation. In: Nicholls [502], pp. 229–241
Bryant, A., Evans, A.S.: Formalizing the Object Management Group’s Core Object Model. Computer Standards & Interfaces 17(5-6), 481–489 (1995)
Bryant, A., Evans, A.S., Semmens, L., Milovanovic, R., Stockman, S., Norris, M., Selley, C.: Using Z to rigorously review a specification of a network management system. In: Bowen and Hinchey [99], pp. 423–433
Bryant, A., Semmens, L. (eds.) Methods Integration, Electronic Workshops in Computing, Springer, Heidelberg (1996); Proceedings of the Methods Integration Workshop, University of Leeds, UK, 25– 26 March 1996. See [241,267,347,352,391,415,539]
Buckberry, G.R.: ZED: A Z notation editor and syntax analyser. BCS-FACS FACTS, Series II 2(3), 13–23 (1991)
Burns, A., Morrison, I.W.: A formal description of the structure attribute model for tool interfacing. IEE/BCS Software Engineering Journal 4(2), 74–78 (1989)
Burns, A., Wellings, A.J.: Occam’s priority model and deadline scheduling. In: Proc. 7th Occam User Group Meeting, Grenoble (1987)
Busby, J.S., Hutchison, D.: The practical integration of manufacturing applications. Software Practice and Experience 22(2), 183–207 (1992)
Büssow, R., Weber, M.: A steam-boiler control specification with Statecharts and Z. In: Abrial et al. [10], pp. 109–128
Butcher, P.: A behavioural semantics for Linda-2. IEE/BCS Software Engineering Journal 6(4), 196–204 (1991)
Butler, G., Grogono, P., Khendek, F.: A Z specification of use cases: A preliminary report. In: Proc. Asia-Pacific Software Engineering Conference / International Computer Science Conference (APSEC 1997/ICSC 1997), Hong Kong, December 2-5, pp. 505–506. IEEE Computer Society Press, Los Alamitos (1997)
Butler, M.J.: Service extension at the specification level. In: Nicholls [504], pp. 319–336
Butler, M.J.: An approach to the design of distributed systems with B AMN. In: Bowen et al. [101], pp. 223–241
Butler, S., Duke, R.: Defining composition operators for object interaction. Object Oriented Systems 5(1), 1–16 (1998)
Campin, J., Paton, N., Williams, M.H.: Specifying active database systems in an object-oriented framework. International Journal of Software Engineering and Knowledge Engineering 7(1), 101–123 (1997)
Carrington, D.: ZOOM workshop report. In Nicholls [506], pp. 352–364. This paper records the activities of a workshop on Z and object-oriented methods held in August 1992at Oxford. A comprehensive bibliography is included
Carrington, D., Duke, D.J., Duke, R., King, P., Rose, G.A., Smith, G.: Object-Z: An object-oriented extension to Z. In: Vuong, S. (ed.) Formal Description Techniques, II (FORTE 1989), pp. 281–296. Elsevier Science Publishers, North- Holland (1990)
Carrington, D., Duke, D.J., Hayes, I.J., Welsh, J.: Deriving modular designs from formal specifications. ACM Software Engineering Notes 18(5), 89–98 (1993)
Carrington, D., Smith, G.: Extending Z for object-oriented specifications. In: Proc. 5th Australian Software Engineering Conference (ASWEC 1990), Australia, pp. 9–14 (1990), IREE
Carrington, D., Stocks, P.: A tale of two paradigms: Formal methods and software testing. In: Bowen and Hall [91], pp. 51–68. Also available as Technical Report 94-4, Department of Computer Science, University of Queensland, Australia (1994)
Chalin, P., Grogono, P.: Z specification of an object manager. In: Bjørner et al. [51], pp. 41–71
Chan, D.K.C., Trinder, P.W.: An object-oriented data model supporting multi-methods, multiple inheritance, and static type checking: A specification in Z. In: Bowen and Hall [91], pp. 297–315
Chantatub, W., Holcombe, M.: Software testing strategies for software requirements and design. In: Proc. EuroSTAR 1994, 3000-2 Hartley Road, Jacksonville, Florida 32257, USA, pp. 40/1–40/29 (1994); Software Quality Engineering. The paper describes how to construct a detailed Z specification using traditional software engineering techniques (ERDs, DFDs, etc.) in a top down manner. It introduces a number of notational devices to help with the management of large Z specifications. Some issues about proving consistency between levels are also addressed
Chauvet, J.Y.: Le cas “legislation viellesse”: Etude de cas. In: Habrias [303], pp. 243–264
Chung, C.M., Shih, T.K., Wang, C.C.: Object-oriented software testing and metric in Z specification. Information Sciences 98(1-4), 175–202 (1997)
Ciaccia, P., Ciancarini, P.: A course on formal methods in software engineering: Matching requirements with design. In: Bowen and Hinchey [99], pp. 482–496
Ciaccia, P., Ciancarini, P., Penzo, W.: A formal approach to software design: The Clepsydra methodology. In: Bowen and Hinchey [99], pp. 5–24
Ciaccia, P., Ciancarini, P., Penzo, W.: Formal requirements and design specifications: The Clepsydra methodology. International Journal of Software Engineering and Knowledge Engineering 7(1), 1–42 (1997)
Ciancarini, P., Cimato, S., Mascolo, C.: Engineering formal requirements: An analysis and testing method for Z documents. Annals of Software Engineering 3, 189–219 (1997)
Ciancarini, P., Mascolo, C.: Analyzing the dynamics of a Z specification. In: Limongelli, C., Calmet, J. (eds.) DISCO 1996. LNCS, vol. 1128, pp. 138–149. Springer, Heidelberg (1996)
Ciancarini, P., Mascolo, C.: Analysing and refining an architectural style. In: Bowen et al. [101], pp. 349–368
Ciancarini, P., Mascolo, C., Vitali, F.: Visualizing Z notation in HTML documents. In: Bowen et al. [85], pp. 81–95
Ciancarini, P., Rizzi, A., Vitali, F.: An extensible rendering engine for XML and HTML. Computer Networks and ISDN Systems 30(1-7), 225–237 (1998)
Cohen, B.: Justification of formal methods for system specifications & A rejustification of formal notations. IEE/BCS Software Engineering Journal 4(1), 26–38 (1989)
Cohen, B.: Set theory as a semantic framework for object-oriented modeling. In: Bosch and Mitchell [61]
Cohen, B., Mannering, D.: The rigorous specification and verification of the safety aspects of a real-time system. In: Proc. COMPASS 1990, Gaithersburg, USA (1990)
Coleman, D.L., Baker, A.L.: Synthesizing structured analysis and object-based formal specifications. Annals of Software Engineering 3, 221–253 (1997)
Collins, B.P., Nicholls, J.E., Sørensen, I.H.: Introducing formal methods: The CICS experience with Z. In: Neumann, B., et al. (eds.) Mathematical Structures for Software Engineering, Oxford University Press, Oxford (1991)
Cooke, J.: Editorial – formal methods: What? why? and when? The Computer Journal 35(5), 417–418 (1992); An editorial introduction to two special issues on Formal Methods. See also [37,157,471,570,685] for papers relevant to Z
Cooke, J.: Formal methods – mathematics, theory, recipes or what? The Computer Journal 35(5), 419–423 (1992)
Coombes, A.C., Barroca, L., Fitzgerald, J.S., McDermid, J.A., Spencer, L., Saeed, A.: Formal specification of an aerospace system: The attitude monitor. In: Hinchey and Bowen [348], pp. 307–332
Coombes, A.C., McDermid, J.A.: A tool for defining the architecture of Z specifications. In: Nicholls [504], pp. 77–92
Coombes, A.C., McDermid, J.A.: Using diagrams to give a formal specification of timing constraints in Z. In: Bowen and Nicholls [102], pp. 119–130
Cooper, D.: Educating management in Z. In: Nicholls [502], pp. 192–194
Cordeiro, V.A.O., Sampaio, A.C.A., Meira, S.L.: From MooZ to Eiffel – a rigorous approach to system development. In: Naftalin et al. [490], pp. 306–325
Craggs, S., Wordsworth, J.B.: Hursley Lab wins another Queen’s Award & Hursley and Oxford – a marriage of minds & Z stands for quality. Developments, IBM Hursley Park 8, 1–2 (1992)
Craig, I.: The Formal Specification of Advanced AI Architectures, September 1991. AI Series. Ellis Horwood (1991); This book contains two rather large (and relatively complete) specifications of Artificial Intelligence (AI) systems using Z. The architectures are the blackboard and Cassandra architectures. As well as showing that formal specification can be used in AI at the architecture level, the book is intended as a case-studies book, and also contains introductory material on Z (for AI people). The book assumes a knowledge of Z, so for non-AI people its primary use is for the presentation of the large specifications. The blackboard specification, with explanatory text, is around 100 pages
Craigen, D., Gerhart, S.L., Ralston, T.J.: Formal methods reality check: Industrial usage. In: Woodcock and Larsen [689], pp. 250–267; The 1st FME Symposium was held at Odense, Denmark, 19–23 April 1993. Zrelated papers include [103,165,254,372,447,526]
Craigen, D., Gerhart, S.L., Ralston, T.J.: . An international survey of industrial applications of formal methods. Technical Report NIST GCR 93/626-V1 & 2, Atomic Energy Control Board of Canada, US National Institute of Standards and Technology, and US Naval Research Laboratories (1993) Volume 1: Purpose, Approach, Analysis and Conclusions; Volume 2: Case Studies. Order numbers: PB93-178556/AS & PB93-178564/AS; National Technical Information Service, 5285 Port Royal Road, Springfield, VA 22161, USA.
Craigen, D., Gerhart, S.L., Ralston, T.J.: An international survey of industrial applications of formal methods. In: Bowen and Nicholls [102], pp. 1–5
Craigen, D., Gerhart, S.L., Ralston, T.J.: Formal methods reality check: Industrial usage. IEEE Transactions on Software Engineering 21(2), 90–98 (1995); Revised version of [165]
Craigen, D., Gerhart, S.L., Ralston, T.J.: Formal methods technology transfer: Impediments and innovation. In: Hinchey and Bowen [348], pp. 399–419
Craigen, D., Kromodimoeljo, S., Meisels, I., Pase, W., Saaltink, M.: EVES: An overview. In: Prehn and Toetenel [530], pp. 389–405
Crowcroft, J., d’Inverno, M.: Languages and formal methods. In: Crowcroft, J. (ed.) Open Distributed Systems, pp. 99–137. UCL Press, London (1996)
Cusack, E.: Inheritance in object oriented Z. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 167–179. Springer, Heidelberg (1991)
Cusack, E.: Object oriented modelling in Z for open distributed systems. In: de Meer, J. (ed.) Proc. International Workshop on ODP, Elsevier Science Publishers, North-Holland (1992)
Cusack, E.: Using Z in communications engineering. In: Bowen and Nicholls [102], pp. 196–202
Cusack, E., Lai, M.: Object oriented specification in LOTOS and Z (or my cat really is object oriented!). In: de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1990. LNCS, vol. 489, pp. 179–202. Springer, Heidelberg (1991)
Cusack, E., Wezeman, C.D.: Deriving tests for objects specified in Z. In: Bowen and Nicholls [102], pp. 180–195
de Barros, R.S.M.: Deriving relational database programs from formal specifications. In: Naftalin et al. [490], pp. 703–723
de Barros, R.S.M., Harper, D.J.: Formal development of relational database applications. In: Harper, D.J., Norrie, M.C. (eds.) Specifications of Database Systems, Glasgow 1991, Workshops in Computing, pp. 21–43. Springer, Heidelberg (1992)
de Barros, R.S.M., Harper, D.J.: A method for the specification of relational database applications. In: Nicholls [506], pp. 261–286
de Lima Machado, P.D., Meira, S.L.: On the use of formal specifications in the design and simulation of artificial neural nets. In: Bowen and Hinchey [99], pp. 63–82
Dean, N.: Mental models of Z: I – sets and logic. In: Bowen and Hinchey [99], pp. 498–507
Dean, N.: The Essence of Discrete Mathematics. The Essence of Computing Series. Prentice-Hall, Englewood Cliffs (1997); An introductory book using a Z-like notation
Dean, N., Hinchey, M.G.: Introducing formal methods through rôle-playing. ACM SIGCSE Bulletin 27(1), 302–306 (1995)
Dearden, A.M., Harrison, M.D.: A software engineering model for case memory systems. The Computer Journal 40(4), 167–182 (1997)
Dehbonei, B., Mejia, F.: Formal methods in the railways signalling industry. In: Naftalin et al. [490], pp. 26–34
Delisle, N., Garlan, D.: Formally specifying electronic instruments. In: Proc. 5th International Workshop on Software Specification and Design, May 1989, IEEE Computer Society, Los Alamitos (1989); Also published in ACM SIGSOFT Software Engineering Notes 14(3)
Delisle, N., Garlan, D.: A formal specification of an oscilloscope. IEEE Software 7(5), 29–36 (1990); Unlike most work on the application of formal methods, this research uses formal methods to gain insight into system architecture. The context for this case study is electronic instrument design
Derrick, J., Boiten, E.A.: Testing refinements by refining tests. In: Bowen et al. [85], pp. 265–283
Derrick, J., Boiten, E.A., Bowman, H., Steen, M.: Supporting ODP – translating LOTOS to Z. In: Najm, E., Stefani, J.-B. (eds.) Proc. 1st IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems, March 1996, pp. 399–406. Chapman & Hall, Boca Raton (1996)
Derrick, J., Boiten, E.A., Bowman, H., Steen, M.: Translating LOTOS to Object-Z. In: Duke, D.J., Evans, A.S. (eds.) Northern Formal Methods Workshop, Electronic Workshops In Computing, Springer, Heidelberg (1997)
Derrick, J., Boiten, E.A., Bowman, H., Steen, M.: Weak refinement in Z. In: Bowen et al. [101], pp. 369–388
Derrick, J., Bowman, H., Steen, M.: Maintaining cross viewpoint consistency using Z. In: Raymond, K., Armstrong, L. (eds.) IFIP TC6 International Conference on Open Distributed Processing, February 1995, pp. 413–424. Chapman & Hall, Boca Raton (1995)
Derrick, J., Bowman, H., Steen, M.: Viewpoints and objects. In: Bowen and Hinchey [99], pp. 449–468
Di Giovanni, R., Iachini, P.L.: HOOD and Z for the development of complex systems. In: Bjørner et al. [51], pp. 262–289
Dick, A.J.J., Krause, P.J., Cozens, J.: Computer aided transformation of Z into Prolog. In: Nicholls [502], pp. 71–85
Diller, A.: Z and Hoare logics. In: Nicholls [506], pp. 59–76
Diller, A.: Z: An Introduction to Formal Methods, 2nd edn. John Wiley & Sons, Chichester (1994); This book offers a comprehensive tutorial to Z from the practical viewpoint. Many natural deduction style proofs are presented and exercises are included. Z as defined in the 2nd edition of The Z Notation [604] is used throughout. Contents: Tutorial introduction; Methods of reasoning; Case studies; Specification animation; Reference manual; Answers to exercises; Glossaries of terms and symbols; Bibliography
Diller, A., Docherty, R.: Z and abstract machine notation: A comparison. In: Bowen and Hall [91], pp. 250–263
d’Inverno, M., Crowcroft, J.: Design, specification and implementation of a real time conferencing system. In: Proc. 10th Annual Joint Conference of IEEE INFOCOM 1991, New York, USA, pp. 1114–1125 (1991)
d’Inverno, M., Fisher, M., Lomuscio, A., Luck, M., de Rijke, M., Ryan, M., Wooldridge, M.: Formalisms for multi-agent systems. Knowledge Engineering Review 12(3), 315–321 (1997); Includes a discussion of the appropriateness of Z for multi-agent systems
d’Inverno, M., Hu, M.J.: A Z specification of the soft-link hypertext model. In: Bowen et al. [101], pp. 297–316
d’Inverno, M., Justo, G.R., Howells, P.: A formal framework for specifying design methodologies. In: El-Rewini, H., Shriver, B.D. (eds.) Proc. 29th Annual Hawaii International Conference on System Sciences, pp. 741–750. IEEE Computer Society Press, Los Alamitos (1996)
d’Inverno, M., Justo, G.R., Howells, P.: A formal framework for specifying design methodologies. Software Process: Improvement and Practice 2(3), 181–195 (1996)
d’Inverno, M., Kinny, D., Luck, M.: Interaction protocols in Agentis. In: Proc. 3rd International Conference on Multi-Agent Systems (ICMAS 1998), Paris, France (1998)
d’Inverno, M., Kinny, D., Luck, M., Wooldridge, M.: A formal specification of dMARS. In: Rao, A., Singh, M.P., Wooldridge, M.J. (eds.) ATAL 1997. LNCS, vol. 1365, pp. 155–176. Springer, Heidelberg (1998)
d’Inverno, M., Luck, M.: A formal view of social dependence networks. In: Zhang, C., Lukose, D. (eds.) DAI 1995. LNCS, vol. 1087, pp. 115–129. Springer, Heidelberg (1996)
d’Inverno, M., Luck, M.: Formalising the contract net as a goal directed system. In: Perram, J., Van de Velde, W. (eds.) MAAMAW 1996. LNCS (LNAI), vol. 1038, pp. 72–85. Springer, Heidelberg (1996)
d’Inverno, M., Luck, M.: Understanding autonomous interaction. In: Wahlster, W. (ed.) Proc. 13th European Conference on Artificial Intelligence (ECAI 1996), pp. 529–533. John Wiley & Sons, Chichester (1996)
d’Inverno, M., Luck, M.: Development and application of an formal agent framework. In: Hinchey and Liu [350], pp. 222–231
d’Inverno, M., Luck, M.: Making and breaking engagements: An operational analysis of agent relationships. In: Dickson, L., Zhang, C. (eds.) DAI 1996. LNCS (LNAI), vol. 1286, pp. 48–62. Springer, Heidelberg (1997)
d’Inverno, M., Luck, M.: A formal specification of AgentSpeak(L). Logic and Computation 8(3) (1998)
d’Inverno, M., Luck, M., Wooldridge, M.: Cooperation structures. In: Proc. 15th International Joint Conference on Artificial Intelligence, Nagoya, Japan, pp. 600–605 (1997)
d’Inverno, M., Priestley, M.: Structuring specification in Z to build a unifying framework for hypertext systems. In: Bowen and Hinchey [99], pp. 83–102
d’Inverno, M., Priestley, M., Luck, M.: A formal framework for hypertext systems. IEE Proceedings – Software Engineering 144(3), 175–184 (1997)
Dix, A.J.: Formal Methods for Interactive Systems. Computers and People Series. Academic Press, London (1991)
Dix, A.J., Finlay, J., Abowd, G.D., Beale, R.: Human-Computer Interaction. Prentice Hall International, Englewood Cliffs (1993)
Docherty, R.F.: Translation from Z to AMN. In: Habrias [303], pp. 205–228
Dodge, C.J.: A Fast Fourier Transform Accelerator for a Transputer System. PhD thesis, University of Aberdeen, Department of Biomedical Physics, Foresterhill, Aberdeen AB9 2ZD, UK, The design includes a detailed Z specification (1993)
Dodge, C.J., Ross, P.G.B., Allen, A.R., Undrill, P.E.: Formal methods in the design of an FFT accelerator for a Transputer based image processing system. Medical and Biological Engineering and Computing 29, 91 (1991)
Dodge, C.J., Undrill, P.E., Allen, A.R., Ross, P.G.B.: Application of Z in digital hardware design. IEE Proceedings – Computers and Digital Techniques 143(1), 79–86 (1996)
Doma, V., Nicholl, R.: EZ: A system for automatic prototyping of Z specifications. In: Prehn and Toetenel [530], pp. 189–203
Dong, J.S., Duke, R.: An object-oriented approach to the formal specification of ODP trader. In: Proc. IFIP TC6/WG6.1 International Conference on Open Distributed Processing, September 1993, pp. 341–352 (1993)
Dong, J.S., Duke, R., Rose, G.: An object-oriented denotational semantics of a small programming language. Object Oriented Systems 4(1), 29–52 (1997)
Dong, J.S., Duke, R., Rose, G.A.: An object-oriented approach to the semantics of programming languages. In: Proc. 17th Australian Computer Science Conference (ACSC-17), January 1994, pp. 767–775 (1994)
Draper, C.: Practical experiences of Z and SSADM. In: Bowen and Nicholls [102], pp. 240–251
Duce, D.A., Duke, D.J., ten Hagen, P.J.W., Herman, I., Reynolds, G.J.: Formal methods in the development of PREMO. Computer Standards & Interfaces 17(5-6), 491–509 (1995)
Duce, D.A., Duke, D.J., ten Hagen, P.J.W., Reynolds, G.J.: PREMO – an initial approach to a formal definition. Computer Graphics Forum 13(3), C–393–C–406 (1994); PREMO (Presentation Environments for Multimedia Objects) is a work item proposal by the ISO/IEC JTC11/SC24 committee, which is responsible for international standardization in the area of computer graphics and image processing
Duke, D.J.: Structuring Z specifications. Australian Computer Science Communications 12(1), 1–10 (1991); Proc. 14th Australian Computer Science Conference
Duke, D.J.: Enhancing the structures of Z specifications. In: Nicholls [506], pp. 329–351
Duke, D.J.: Object-Oriented Formal Specification. PhD thesis, Department of Computer Science, University of Queensland, St. Lucia 4072, Australia (1992)
Duke, D.J., Duke, R.: Towards a semantics for Object-Z. In: Bjørner et al. [51], pp. 244–261
Duke, D.J., Harrison, M.D.: Event model of human-system interaction. IEE/BCS Software Engineering Journal 10(1), 3–12 (1995)
Duke, D.J., Harrison, M.D.: Mapping user requirements to implementations. IEE/BCS Software Engineering Journal 10(1), 13–20 (1995)
Duke, R., Duke, D.J.: Aspects of object-oriented formal specification. In: Proc. 5th Australian Software Engineering Conference (ASWEC 1990), Australia, pp. 21–26 (1990), IREE
Duke, R., Hayes, I.J., King, P., Rose, G.A.: Protocol specification and verification using Z. In: Aggarwal, S., Sabnani, K. (eds.) Protocol Specification, Testing, and Verification VIII, pp. 33–46. Elsevier Science Publishers, North- Holland (1988)
Duke, R., King, P., Rose, G.A., Smith, G.: The Object-Z specification language. In: Korson, T., Vaishnavi, V., Meyer, B. (eds.) Technology of Object-Oriented Languages and Systems: TOOLS 5, pp. 465–483. Prentice-Hall, Englewood Cliffs (1991)
Duke, R., King, P., Rose, G.A., Smith, G.: The Object-Z specification language: Version 1. Technical Report 91-1, Department of Computer Science, University of Queensland, St. Lucia 4072, Australia (April 1991); The most complete (and currently the standard) reference on Object-Z. It has been reprinted by ISO JTC1 WG7 as document number 372. A condensed version of this report was published as [236]
Duke, R., Rose, G., Smith, G.: Object-Z: A specification language advocated for the description of standards. Computer Standards & Interfaces 17(5-6), 511–533 (1995)
Duke, R., Rose, G.A., Lee, A.: Object-oriented protocol specification. In: Logrippo, L., Probert, R.L., Ural, H. (eds.) Protocol Specification, Testing, and Verification X, pp. 325–338. Elsevier Science Publishers, North-Holland (1990)
Duke, R., Smith, G.: Temporal logic and Z specifications. Australian Computer Journal 21(2), 62–69 (1989)
Dunckley, L., Smith, A.: Improving access of the commercial software developer to formal methods: Integrating MERISE with Z. In: Bryant and Semmens [121]
Dupuy, S., Ledru, Y., Chabre-Peccoud, M.: Translating the OMT dynamic model into Object-Z. In: Bowen et al. [85], pp. 347–366
Ebert, J., Süttenbach, R.: Integration of Z-based semantics of OO-notations. In: Bosch and Mitchell [61]
Edmond, D.: Information Modeling: Specification and Implementation. Prentice-Hall, Englewood Cliffs (1992)
Edmond, D.: Refining database systems. In: Bowen and Hinchey [99], pp. 25–44
Engel, M.: Specifying real-time systems with Z and the Duration Calculus. In: Bowen and Hall [91], pp. 282–294
Evans, A.S.: Specifying & verifying concurrent systems using Z. In: Naftalin et al. [490], pp. 366–400
Evans, A.S.: Visualising concurrent Z specifications. In: Bowen and Hall [91], pp. 269–281
Evans, A.S.: An improved recipe for specifying reactive systems in Z. In: Bowen et al. [101], pp. 275–294
Fencott, P.C., Galloway, A.J., Lockyer, M.A., O’Brien, S.J., Pearson, S.: Formalising the semantics ofWard/Mellor SA/RT essential models using a process algebra. In: Naftalin et al. [490], pp. 681–702
Fenton, N.E., Mole, D.: A note on the use of Z for flowgraph transformation. Information and Software Technology 30(7), 432–437 (1988)
Fergus, E., Ince, D.C.: Z specifications and modal logic. In: Hall, P.A.V. (ed.) Proc. Software Engineering 1990. British Computer Society Conference Series, vol. 1, Cambridge University Press, Cambridge (1990)
Fidge, C.J.: Specification and verification of real-time behaviour using Z and RTL. In: Vytopil, J. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, pp. 393–410. Springer, Heidelberg (1992)
Fidge, C.J.: Real-time refinement. In: Woodcock and Larsen [689], pp. 314–331
Fidge, C.J.: Adding real time to formal program development. In: Naftalin et al. [490], pp. 618–638
Fidge, C.J.: Proof obligations for real-time refinement. In: Till [646], pp. 279– 305
Fidge, C.J., Utting, M., Kearney, P., Hayes, I.J.: Integrating real-time scheduling theory and program refinement. In: Gaudel and Woodcock [280], pp. 327– 346
Finney, K.: Mathematical notation in formal specification: Too difficult for the masses? IEEE Transactions on Software Engineering 22(2), 158–159 (1996)
Fischer, C.: How to combine Z with a process algebra. In: Bowen et al. [85], pp. 5–23
Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.): FME 1997. LNCS, vol. 1313. Springer, Heidelberg (1997); See the Z-related paper [56]
Flynn, M., Hoverd, T., Brazier, D.: Formaliser – an interactive support tool for Z. In: Nicholls [502], pp. 128–141
Fogg, I., Hicks, B., Lister, A., Mansfield, T., Raymond, K.: A comparison of LOTOS and Z for specifying distributed systems. Australian Computer Science Communications 12(1), 88–96 (1990)
Fowler, D.C., Swatman, P.A., Swatman, P.M.C.: Implementing EDI in the public sector: Including formality for enhanced control. In: Proc. 7th International Conference on Electronic Data Interchange (June 1993)
France, R.B., Bruel, J.-M.: Integrated informal object-oriented and formal modeling techniques. In: Bosch and Mitchell [61]
France, R.B., Gerhart, S.L. (eds.): Proc. Workshop on Industrial-strength Formal Specification Techniques. IEEE Computer Society Press, Los Alamitos (1995)
France, R.B., Larrondo-Petrie, M.M.: A two-dimensional view of integrated formal and informal specification techniques. In: Bowen and Hinchey [99], pp. 434–448
France, R.B., Wu, J., Larondo-Petrie, M.M., Bruel, J.-M.: A tale of two case studies: Using integrated methods to support rigorous requirements specification. In: Bryant and Semmens [121]; Includes a study of an integrated Object-Oriented Analysis (OOA) method (Fusion) and formal specification technique (Z) used to create requirements models that are graphical and analyzable
Friesen, V.: An exercise in hybrid system specification using an extension of Z. In: Bouajjani, A., Maler, O. (eds.) Proc. 2nd European Workshop on Real-Time and Hybrid Systems, pp. 311–316 (1995)
Friesen, V., Nordwig, A., Weber, M.: Object-oriented specification of hybrid systems using UMLh and ZimOO. In: Bowen et al. [85], pp. 328–346
Fuchs, N.E.: Specifications are (preferably) executable. IEE/BCS Software Engineering Journal 7(5), 323–334 (1992)
Galloway, A.J., Habrias, H.: Formalising the semantics of GRAFCET function charts using Z. Rapport de Recherche IRIN - 131, Université de Nantes, Institut de Recherche en Informatique de Nantes, France (1996)
Galloway, A.J., Habrias, H.: Integrating NIAM, JSD, CCS and Z. Rapport de Recherche IRIN - 130, Université de Nantes, Institut de Recherche en Informatique de Nantes, France (1996)
Gardiner, P.H.B., Lupton, P.J., Woodcock, J.C.P.: A simpler semantics for Z. In: Nicholls [504], pp. 3–11
Garlan, D.: The role of reusable frameworks. ACM SIGSOFT Software Engineering Notes 15(4), 42–44 (1990)
Garlan, D.: Integrating formal methods into a professional master of software engineering program. In: Bowen and Hall [91], pp. 71–85
Garlan, D.: Making formal methods effective for professional software engineers. Information and Software Technology 37(5-6), 261–268 (1995); Revised version of [275]
Garlan, D., Delisle, N.: Formal specifications as reusable frameworks. In: Bjørner et al. [51], pp. 150–163
Garlan, D., Delisle, N.: Formal specification of an architecture for a family of instrumentation systems. In: Hinchey and Bowen [348], pp. 55–72
Garlan, D., Notkin, D.: Formalizing design spaces: Implicit invocation mechanisms. In: Prehn and Toetenel [530], pp. 31–45
Gaudel, M.-C., Woodcock, J.C.P. (eds.): FME 1996. LNCS, vol. 1051. Springer, Heidelberg (1996); The proceedings includes Z-related papers [58,257,392,664] and B-related papers [48,351,663]
Gerhart, S.L.: Applications of formal methods: Developing virtuoso software. IEEE Software 7(5), 6–10 (1990); This is an introduction to a special issue on Formal Methods with an emphasis on Z in particular. It was published in conjunction with special Formal Methods issues of IEEE Transactions on Software Engineering and IEEE Computer. See also [187,307,491,602,672]
Gerhart, S.L., Craigen, D., Ralston, T.J.: Observations on industrial practice using formal methods. In: Proc. 15th International Conference on Software Engineering (ICSE), Baltimore, Maryland, USA (May 1993)
Gerhart, S.L., Craigen, D., Ralston, T.J.: Experience with formal methods in critical systems. IEEE Software 11(1), 21–28 (1994); Several commercial and exploratory cases in which Z features heavily are briefly presented on page 24. See also [404]
Germán, D.M., Cowan, D.D.: Experiments with the Z Interchange Format and SGML. In: Bowen and Hinchey [99], pp. 224–233
Gilmore, S.: Correctness-oriented approaches to software development. Technical Report ECS-LFCS-91-147 (also CST-76-91), Department of Computer Science, University of Edinburgh, Edinburgh EH9 3JZ, UK (1991); This PhD thesis provides a critical evaluation of Z, VDM and algebraic specifications
Gimson, R.B.: The formal documentation of a Block Storage Service. Technical Monograph PRG-62, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (August 1987)
Gimson, R.B., Morgan, C.C.: Ease of use through proper specification. In: Duce, D.A. (ed.) Distributed Computing Systems Programme, Peter Peregrinus, London (1984)
Gimson, R.B., Morgan, C.C.: The Distributed Computing Software project. Technical Monograph PRG-50, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (July 1985)
Ginbayashi, J.: Analysis of business processes specified in Z against an E-R data model. Technical Monograph PRG-103, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (December 1992)
Gonzalez, H.S.: A symbolic representation of transcendental logic using Z language and its role in knowledge base systems. In: Cantu, F.J., Soto, R., Liebowitz, J., Sucar, E. (eds.) Proc. 4th World Congress of Expert Systems: Application of Advanced Information Technologies, Mexico City, March 16-20, vol. 1&2, pp. 383–387. Scholium International Inc. (1998)
Goodman, H.S.: From Z specifications to Haskell porgrams: A three-pronged approach. In: Habrias [303], pp. 167–182
Goodman, H.S.: The Z-into-Haskell tool-kit: An illustrative case study. In: Bowen and Hinchey [99], pp. 374–388
Goodwin, R.: Formalizing properties of agents. Journal of Logic and Computation 5(6), 763–781 (1995)
Gotzhein, R.: Specifying open distributed systems with Z. In: Bjørner et al. [51], pp. 319–339
Grassmann, W.K., Tremblay, J.-P.: The Formal Specification of Requirements in Z, ch. 8, pp. 441–480. Prentice-Hall, Englewood Cliffs (1996)
Gravell, A.M.: Minimisation in formal specification and design. In: Nicholls [502], pp. 32–45
Gravell, A.M.: What is a good formal specification? In: Nicholls [504], pp. 137–150
Gravell, A.M., Henderson, P.: Executing formal specifications need not be harmful. IEE/BCS Software Engineering Journal 11(2), 104–110 (1996)
Gravell, A.M., Pratten, C.H.: Formal methods and open systems. Software—Concepts and Tools 16(4), 183–188 (1995)
Gries, D.: Equational logic: A great pedagogical tool for teaching a skill in logic. In: Bowen and Hinchey [99], pp. 508–509
Grimm, K.: Industrial requirements for the efficient development of reliable embedded systems. In: Bowen et al. [85], pp. 1–4, Extended abstract
H. Habrias. Z, ch. 10, pages 267–290. Méthodologies du Logiciel. Masson, Paris (1993)
Habrias, H. (ed.): Z Twenty Years on – What is its Future?, Université de Nantes, France, IRIN (Institut de Recherche en Informatique de Nantes) (1995); Proceedings of the 7th International Conference on Putting into Practice Methods and Tools for Information System Design, Nantes, France, 10–12O ctober 1995. This conference considered the future of Z, about twenty years after a seminal paper relating to Z [6], See [47,114,117,141,217,291,313,332,427,500,519,529,583,625,657]
Habrias, H., Dunne, S., Stoddart, W.J.: From natural language to Z specification. In: Labarre, J.E. (ed.) Proc. Conference on Information Systems and Global Competitiveness, Toronto, Canada, September 1995, pp. 126–145 (1995), International Association for Computer Information Systems
Halasz, F., Schwartz, M.: The Dexter hypertext reference model. In: Proc. NIST Hypertext Standardization Workshop, Gaithersburg, USA (January 1990)
Hall, J., Martin, A.: \(\mathcal{W}\) reconstructed. In: Bowen et al. [101], pp. 116–134
Hall, J.A.: Seven myths of formal methods. IEEE Software 7(5), 11–19 (1990); Formal methods are difficult, expensive, and not widely useful, detractors say. Using a case study and other real-world examples, this article challenges such common myths. See also [97]
Hall, J.A.: Using Z as a specification calculus for object-oriented systems. In: Bjørner et al. [51], pp. 290–318
Hall, J.A.: Specifying and interpreting class hierarchies in Z. In: Bowen and Hall [91], pp. 120–138
Hall, J.A.: Taking Z seriously. In: Bowen et al. [101], pp. 89–91, Extended abstract
Hall, J.A., Parnas, D.L., Plat, N., Rushby, J., Sennett, C.T.: The future of industrial formal methods. In: Bowen and Hinchey [99], pp. 238–242, Position statements for a panel session moderated by T. King
Hall, J.G., McDermid, J.A.: Towards a Z method: Axiomatic specification in Z. In: Bowen and Hall [91], pp. 213–229
Hall, J.G., McDermid, J.A., Toyn, I.: Model conjectures for Z specifications. In: Habrias [303], pp. 41–51
Hall, P.A.V.: Towards testing with respect to formal specification. In: Proc. 2nd IEE/BCS Conference on Software Engineering, number 290 in Conference Publication, July 1988, pp. 159–163. IEE/BCS (July 1988)
Hamer, U., Peleska, J.: Z applied to the A330/340 CICS cabin communication system. In: Hinchey and Bowen [348], pp. 253–284
Hamilton, V.: The use of Z within a safety-critical software system. In: Hinchey and Bowen [348], pp. 357–374
Hammond, J.A.R.: Producing Z specifications from object-oriented analysis. In: Bowen and Hall [91], pp. 316–336
Hammond, J.A.R.: Z. In: Marciniak, J.J. (ed.) Encyclopedia of Software Engineering, vol. 2, pp. 1452–1453. John Wiley & Sons, Chichester (1994)
Harrison, M.D.: Engineering human-error tolerant software. In: Nicholls [506], pp. 191–204
Harry, A.: Formal Methods Fact File: VDM and Z. John Wiley & Sons, Chichester (1996); Contents: Why do we need formal methods?; Background material; Formal specification styles; Introduction to model-based languages; VDM; The Z notation; Formal semantics; Tool support; The future of formal methods
Hasselbring, W.: Animation of Object-Z specifications with a set-oriented prototyping language. In: Bowen and Hall [91], pp. 337–356
Hasselbring, W.: Prototyping parallel algorithms in a set-oriented language. Dissertation, Department of Computer Science, University of Dortmund, Hamburg, Germany (1994); This dissertation presents the design and implementation of an approach to prototyping parallel algorithms with ProSet-Linda. The presented approach to designing and implementing ProSet-Linda relies on the use of the formal specification language Object-Z and the prototyping language ProSet itself
Haughton, H.P.: Using Z to model and analyse safety and liveness properties of communication protocols. Information and Software Technology 33(8), 575–580 (1991)
Hayes, I.J.: Applying formal specification to software development in industry. IEEE Transactions on Software Engineering 11(2), 169–178 (1985)
Hayes, I.J.: Specification directed module testing. IEEE Transactions on Software Engineering 12(1), 124–133 (1986)
Hayes, I.J.: Using mathematics to specify software. In: Proc. First Australian Software Engineering Conference. Institution of Engineers, Australia (May 1986)
Hayes, I.J.: A generalisation of bags in Z. In: Nicholls [502], pp. 113–127
Hayes, I.J.: Interpretations of Z schema operators. In: Nicholls [504], pp. 12–26
Hayes, I.J.: Multi-relations in Z: A cross between multi-sets and binary relations. Acta Informatica 29(1), 33–62 (1992)
Hayes, I.J.: VDM and Z: A comparative case study. Formal Aspects of Computing 4(1), 76–99 (1992)
Hayes, I.J. (ed.): Specification Case Studies, 2nd edn. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1993); This is a revised edition of the first ever book on Z, originally published in 1987; it contains substantial changes to every chapter. The notation has been revised to be consistent with The Z Notation: A Reference Manual by Mike Spivey [604]. The CAVIAR chapter has been extensively changed to make use of a form of modularization. Divided into four sections, the first provides tutorial examples of specifications, the second is devoted to the area of software engineering, the third covers distributed computing, analyzing the role of mathematical specification, and the fourth part covers the IBM CICS transaction processing system. Appendices include comprehensive glossaries of the Z mathematical and schema notation. The book will be of interest to the professional software engineer involved in designing and specifying large software projects. The other contributors are W. Flinn, R. B. Gimson, S. King, C. C. Morgan, I. H. Sørensen and B. A. Sufrin
Hayes, I.J.: Specification models. In: Habrias [303], pp. 1–10
Hayes, I.J., Jones, C.B.: Specifications are not (necessarily) executable. IEE/BCS Software Engineering Journal 4(6), 330–338 (1989)
Hayes, I.J., Jones, C.B., Nicholls, J.E.: Understanding the differences between VDM and Z. FACS Europe, Series I 1(1), 7–30 (1993); Also available as Technical Report UMCS-93-8-1, Department of Computer Science, University of Manchester, UK (1993)
Hayes, I.J., Wildman, L.: Towards libraries for Z. In: Bowen and Nicholls [102], pp. 9–36
He Jifeng, C.A.R., Hoare, M., Fränzle, M., Müller-Ulm, E.-R., Olderog, M., Schenke, A.P.: Provably correct systems. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 288–335. Springer, Heidelberg (1994)
Jifeng, H., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In B. Robinet and R. Wilhelm, editors, Proc. ESOP 86. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Heath, D., Allum, D., Dunckley, L.: Introductory Logic and Formal Methods. A. Waller, Henley-on-Thames, UK (1994)
Heitmeyer, C.: Formal methods: Panacea or academic poppycock. In: Bowen et al. [101], pp. 3–9
Helke, S., Neustupny, T., Santen, T.: Automating test case generation from Z specifications with Isabelle. In: Bowen et al. [101], pp. 52–71
Hennessey, P., Ibrahim, M.T., Fedorec, A.M.: Formal specification, object oriented design, and implementation of an ephemeral logger for database systems. In: Thoma, H., Wagner, R.R. (eds.) DEXA 1996. LNCS, vol. 1134, pp. 333–355. Springer, Heidelberg (1996)
Henson, M.C., Reeves, S.: A logic for the schema calculus. In: Bowen et al. [85], pp. 172–191
Hepworth, B.: ZIP: A unification initiative for Z standards, methods and tools. In: Nicholls [502], pp. 253–259
Hepworth, B., Simpson, D.: The ZIP project. In: Nicholls [504], pp. 129–133
Hewitt, M.A., O’Halloran, C.M., Sennett, C.T.: Experiences with PiZA, an animator for Z. In: Bowen et al. [101], pp. 37–51
Hinchey, M.G.: Formal methods for system specification: An ounce of prevention is worth a pound of cure. IEEE Potentials Magazine 12(3), 50–52 (1993)
Hinchey, M.G.: JSD =̂ ΔCSP ⊕ TLZ – a case study. In Bryant and Semmens [121]
Hinchey, M.G., Bowen, J.P. (eds.) Applications of Formal Methods. Prentice Hall International Series in Computer Science (1995); A collection on industrial examples of the use of formal methods. Chapters relevant to Z include [158,169,278,315,316,349,450]
Hinchey, M.G., Bowen, J.P.: Applications of formal methods FAQ. In: Applications of Formal Methods [348], pp. 1–15
Hinchey, M.G., Liu, S. (eds.) Formal Engineering Methods: Proc. 1st International Conference on Formal Engineering Methods (ICFEM 1997), Hiroshima, Japan, November 12-14, IEEE Computer Society Press, Los Alamitos (1997); See Z-related papers [209,566,644]
Hoare, J., Dick, J., Neilson, D., Sørensen, I.H.: Applying the B technologies to CICS. In: Gaudel and Woodcock [280], pp. 74–84
Hooker, S., Lockyer, M.A., Fencott, P.C.: CASE support for methods integration: Implementation of a translation from a structured to a formal notation. In: Bryant and Semmens [121]; The work presented takes the Z specification of the Semantic Function and implements it in the functional programming language, ML
Hörcher, H.-M.: Improving software tests using Z specifications. In: Bowen and Hinchey [99], pp. 152–166
Houston, I.S.C., Josephs, M.: Specifying distributed CICS in Z: Accessing local and remote resources (short communication). Formal Aspects of Computing 6(6), 569–579 (1994)
Houston, I.S.C., Josephs, M.B.: A formal description of the OMG’s Core Object Model and the meaning of compatible extension. Computer Standards & Interfaces 17(5-6), 553–558 (1995)
Houston, I.S.C., King, S.: CICS project report: Experiences and results from the use of Z in IBM. In: Prehn and Toetenel [530], pp. 588–596
Hughes, A.P., Donnelly, A.A.: An algebraic proof in VDM\(^\clubsuit\). In: Bowen and Hinchey [99], pp. 114–133
Hutcheon, A.D., Wellings, A.J.: Specifying restrictions on imperative programming languages for use in a distributed embedded environment. IEE/BCS Software Engineering Journal 5(2), 93–104 (1990)
Iachini, P.L.: Operation schema iterations. In: Nicholls [504], pp. 50–57
Imperato, M.: An Introduction to Z. Chartwell-Bratt (1991); Contents: Introduction; Set theory; Logic; Building Z specifications; Relations; Functions; Sequences; Bags; Advanced Z; Case study: a simple banking system
Ince, D.C.: Z and system specification. In: Ince, D.C., Andrews, D. (eds.) The Software Life Cycle, Butterworths, ch. 12, pp. 260–277 (1990)
Ince, D.C.: An Introduction to Discrete Mathematics, Formal System Specification and Z, 2nd edn. Applied Mathematics and Computing Science Series. Oxford University Press, Oxford (1993)
INMOS Limited. Specification of instruction set & Specification of floating point unit instructions. In: Transputer Instruction Set – A compiler writer’s guide, pp. 127–161. Prentice Hall, Englewood Cliffs (1988); Appendices F and G use a Z-like notation to give a specification of the instruction set of the IMS T212 and T414 Transputers, and the T800 floating-point Transputer
ISO/IEC. It – security techniques – hash-functions – part 3: Dedicated hashfunctions. International Standard ISO/IEC DIS 10118-3, International Standards Organization (1997); Contains a Z specification of the hash functions. This is believed to be the first published ISO standard which contains a complete specification in Z
Jack, A.: It’s hard to explain, but Z is much clearer than English. Financial Times, pp. 22, 21 (April 1992)
Jackson, D.: Abstract model checking of infinite specifications. In: Naftalin et al. [490], pp. 519–531
Jackson, D.: Structuring Z specifications with views. ACM Transactions on Software Engineering and Methodology (TOSEM) 4(4), 365–389 (1995)
Jackson, D., Damon, C.A.: Elements of style: Analyzing a software design feature with a counterexample detector. IEEE Transactions on Software Engineering 22(7), 484–495 (1996); Nitpick, a specification checker, is applied to the design of a style mechanism for a word processor, using a subset of Z
Jackson, D., Jackson, M.: Problem decomposition for reuse. IEE/BCS Software Engineering Journal 11(1), 19–30 (1996); An approach to software development based on the idea of problem frames and of structuring Z specifications as views
Jacky, J.: Formal specifications for a clinical cyclotron control system. ACM SIGSOFT Software Engineering Notes 15(4), 45–54 (1990)
Jacky, J.: Formal specification and development of control system input/output. In: Bowen and Nicholls [102], pp. 95–108
Jacky, J.: Specifying a safety-critical control system in Z. InWoodcock and Larsen [689], pp. 388–402; The 1st FME Symposium was held at Odense, Denmark, April 19-23 (1993), Zrelated papers include [103,165,254,372,447,526]
Jacky, J.: Specifying a safety-critical control system in Z. IEEE Transactions on Software Engineering 21(2), 99–106 (1995); Revised version of [372]
Jacky, J.: The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, Cambridge (1997)
J. Jacky. Modelling a real-time program in Z. In Bowen et al. [85], pages 136–153.
Jacky, J., Unger, J.: From Z to code: A graphical user interface for a radiation therapy machine. In: Bowen and Hinchey [99], pp. 315–333
Jacky, J., Unger, J., Patrick, M., Risler, R.: Experience with Z developing a control program for a radiation therapy machine. In: Bowen et al. [101], pp. 317–328
Jacob, J.: The varieties of refinements. In: Morris and Shaw [487], pp. 441–455
Johnson, C.W.: Using Z to support the design of interactive safety-critical systems. IEE/BCS Software Engineering Journal 10(2), 49–60 (1995)
Johnson, C.W.: Literate specification: Using design rationale to support formal methods in the development of human-machine interfaces. Human-Computer Interaction 11(4), 291–320 (1996)
Johnson, D.R., Kilov, H.: Can a flat notation be used to specify an OO system: using Z to describe RM-ODP constraints. In: Najm, E., Stefani, J.-B. (eds.) Proc. 1st IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems, March 1996, pp. 391–398. Chapman & Hall, Boca Raton (1996)
Johnson, D.R., Kilov, H.: An approach to an RM-ODP toolkit in Z. In: Leavens, G.T., Sitaraman, M. (eds.) Proc. Foundations of Component-based Systems Workshop, Zurich, Switzerland, September 26 (1997); European Software Engineering Conference
Johnson, M., Sanders, P.: From Z specifications to functional implementations. In: Nicholls [502], pp. 86–112
Johnson, P.: Using Z to specify CICS. In: Proc. Software Engineering anniversary meeting (SEAS), p. 303 (1987)
Jones, C.B.: Interference revisited. In: Nicholls [504], pp. 58–73
Jones, C.B., Shaw, R.C., Denvir, T. (eds.): 5th Refinement Workshop, Workshop in Computing. Springer, Heidelberg (1992); The workshop was held at Lloyd’s Register, London, UK, 8–10 January 1992. See [573]
Jones, R.B.: ICL ProofPower. BCS-FACS FACTS, Series III 1(1), 10–13 (1992)
Jordan, D., McDermid, J.A., Toyn, I.: CADiZ – computer aided design in Z. In: Nicholls [504], pp. 93–104
Josephs, M.B.: The data refinement calculator for Z specifications. Information Processing Letters 27(1), 29–33 (1988)
Josephs, M.B.: A state-based approach to communicating processes. Distributed Computing 3, 9–18 (1988); A theoretical paper on combining features of CSP and Z
Kasurinen, V., Sere, K.: Data modelling in ZIM. In: Bryant and Semmens [121]
Kasurinen, V., Sere, K.: Integrating action systems and Z in a medical system specification. In: Gaudel and Woodcock [280], pp. 105–119
Katsolakos, T. (ed.) Proc. 1993 Software Engineering Standards Symposium (SESS 1993), Brighton, UK, August 30–September 3 (1993); IEEE Computer Society Press. See Z-related papers [24,74,423]
Kilov, H.: Information modeling and Object Z: Specifying generic reusable associations. In: Etzion, O., Segev, A. (eds.) Proc. NGITS-93 (Next Generation Information Technology and Systems), June 1993, pp. 182–191 (1993)
Kilov, H., Ross, J.: Declarative specifications of collective behavior: Generic reusable frameworks. In: Kilov, H., Harvey, W. (eds.) Proc. Workshop on Specification of Behavioral Semantics in Object-Oriented Information Modeling, Washington DC, USA, pp. 71–75 (1993), OOPSLA
Kilov, H., Ross, J.: Appendix A: A more formal approach. In: Information Modeling: An Object-Oriented Approach [397], pp. 199–207
Kilov, H., Ross, J.: Information Modeling: An Object-Oriented Approach. Object-Oriented Series. Prentice-Hall, Englewood Cliffs (1994)
King, P.: Printing Z and Object-Z LaTeX documents. Department of Computer Science, University of Queensland (May 1990), A description of a Z style option ‘oz.sty’, an extended version of Mike Spivey’s original ‘zed.sty’ [601], for use with the LaTeX document preparation system [408]. It is particularly useful for printing Object-Z documents [134,231].
King, S.: Z and the refinement calculus. In: Bjørner et al. [51], pp. 164–188. Also published as Technical Monograph PRG-79, Oxford University Computing Laboratory, UK (February 1990)
King, S., Sørensen, I.H.: Specification and design of a library system. In: McDermid [457]
King, S., Sørensen, I.H., Woodcock, J.C.P.: Z: Grammar and concrete and abstract syntaxes. Technical Monograph PRG-68, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (1988)
J. C. Knight and S. S. Brilliant. Preliminary evaluation of a formal approach to user interface specification. In Bowen et al. [101], pages 329–346.
Knight, J.C., Kienzle, D.M.: Preliminary experience using Z to specify a safety-critical system. In: Bowen and Nicholls [102], pp. 109–118
Knight, J.C., Littlewood, B.: Critical task of writing dependable software. IEEE Software 11(1), 16–20 (1994); Guest editors’ introduction to a special issue of IEEE Software on Safety-Critical Systems. A short section on formal methods mentions several Z books on page 18. See also [283]
Knott, R.D., Krause, P.J.: The implementation of Z specifications using program transformation systems: The SuZan project. In: Rattray, C., Clark, R.G. (eds.) The Unified Computation Laboratory, Oxford, UK. IMA Conference Series, vol. 35, pp. 207–220. Clarendon Press (1992)
Kraan, I.: Using the rippling heuristic in set membership proofs. In: Bowen et al. [101], pp. 135–147
Kraan, I., Baumann, P.: Implementing Z in Isabelle. In: Bowen and Hinchey [99], pp. 355–373
Lamport, L.: LaTeX User’s Guide & Reference Manual: A document preparation system. Addison-Wesley Publishing Company. 2nd edn (1993); Z specifications may be produced using the document preparation system LaTeX together with a special LaTeX style option. The most widely used style files are fuzz.sty [603], zed.sty [601] and oz.sty [398]
Lamport, L.: TLZ. In: Bowen and Hall [91], pp. 267–268, Abstract
Lano, K.C.: Z + + , an object-orientated extension to Z. In: Nicholls [504], pp. 151–172
Lano, K.C.: Refinement in object-oriented specification languages. In: Till [646], pp. 236–259
Lano, K.C.: Specifying reactive systems in B AMN. In: Bowen et al. [101], pp. 242–274
Lano, K.C., Breuer, P.T.: From programs to Z specifications. In: Nicholls [502], pp. 46–70
Lano, K.C., Breuer, P.T., Haughton, H.P.: Reverse engineering COBOL via formal methods. Software Maintenance: Research and Practice 5, 13–35 (1993); Also published in a shortened form as Chapter 16 in [662]
Lano, K.C., Goldsack, S.: Integrated formal and object-oriented methods: The VDM + + approach. In: Bryant and Semmens [121], Structure Diagrams are formalized in terms of TLZ [409], a combination of the Z notation and the simple temporal logic of Lamport’s TLA, with changes in state being a function of the events in the RPT+ formalization
Lano, K.C., Goldsack, S., Bicarregui, J., Kent, S.: Integrating VDM++ and real-time system design. In: Bowen et al. [101], pp. 188–219
Lano, K.C., Haughton, H.P.: An algebraic semantics for the specification language Z + + . In: Proc. Algebraic Methodology and Software Technology Conference (AMAST 1991), Springer, Heidelberg (1992)
Lano, K.C., Haughton, H.P.: Reasoning and refinement in object-oriented specification languages. In: Lehrmann Madsen, O. (ed.) ECOOP 1992. LNCS, vol. 615, pp. 78–97. Springer, Heidelberg (1992)
Lano, K.C., Haughton, H.P.: The Z + + Manual. Lloyd’s Register of Shipping, 29 Wellesley Road, Croydon CRO 2AJ, UK (1992)
Lano, K.C., Haughton, H.P. (eds.): Object Oriented Specification Case Studies. Object Oriented Series. Prentice Hall International, Englewood Cliffs (1993); Contents: Chapters introducing object oriented methods, object oriented formal specification and the links between formal and structured object-oriented techniques; seven case studies in particular object oriented formal methods, including: The Unix Filing System: A MooZ Specification; An Object-Z Specification of a Mobile Phone System; Object-oriented Specification in VDM + + ; Specifying a Concept-recognition System in Z + + ; Specification in OOZE; Refinement in Fresco; SmallVDM: An Environment for Formal Specification and Prototyping in Smalltalk. A glossary, index and bibliography are also included. The contributors are some of the leading figures in the area, including the developers of the above methods and languages: Silvio Meira, Gordon Rose, Roger Duke, Antonio Alencar, Joseph Goguen, Alan Wills, Cassio Souza dos Santos, Ana Cavalcanti
Lano, K.C., Haughton, H.P.: Reuse and adaptation of Z specifications. In: Bowen and Nicholls [102], pp. 62–90
Lano, K.C., Haughton, H.P.: Reverse Engineering and Software Maintenance: A Practical Approach. International Series in Software Engineering. McGraw Hill, New York (1993)
Lano, K.C., Haughton, H.P.: Standards and techniques for object-oriented formal specification. In: Katsolakos [393], pp. 237–246
Lano, K.C., Haughton, H.P.: Formal development in B Abstract Machine Notation. Information and Software Technology 37(5-6), 303–316 (1995)
Lano, K.C., Kan, P., Sanchez, A.: Compositional specification of controllers for batch process operations. In: Bowen et al. [85], pp. 250–264
Laycock, G.: Formal specification and testing: A case study. Software Testing, Verification and Reliability 2(1), 7–23 (1992)
Ledru, Y., Chiaramella, Y.: Integrating and teaching Z and CSP. In: Habrias [303], pp. 131–147
Lee, J., Pan, J.I.: A rule-based approach to producing Z specifications from Jackson System Development. International Journal of Intelligent Systems 13(7), 587–611 (1998)
Leveson, N.: Designing a requirements specification language for reactive systems. In: Bowen et al. [85], pp. 135, Abstract
Lightfoot, D.: Formal Specification using Z. Macmillan, Basingstoke (1991); Contents: Introduction; Sets in Z; Using sets to describe a system – a simple example; Logic: propositional calculus; Example of a Z specification document; Logic: predicate calculus; Relations; Functions; A seat allocation system; Sequences; An example of sequences – the aircraft example again; Extending a specification; Collected notation; Books on formal specification; Hints on creating specifications; Solutions to exercises. Also available in French
Lindsay, P.A.: On transferring VDM verification techniques to Z. In: Naftalin et al. [490], pp. 190–213. Also available as Technical Report 94-10, Department of Computer Science, University of Queensland, Australia (1994)
Liskov, B., Wing, J.M.: Specifications and their use in defining subtypes. In: Bowen and Hinchey [99], pp. 246–263
London, R.L., Milsted, K.R.: Specifying reusable components using Z: Realistic sets and dictionaries. ACM SIGSOFT Software Engineering Notes 14(3), 120–127 (1989)
Love, M.: Animating Z specifications in SQL*Forms3.0. In: Bowen and Nicholls [102], pp. 294–306
Luck, M., d’Inverno, M.: A formal framework for agency and autonomy. In: Proc. 1st International Conference on Multi-Agent Systems, pp. 254–260. AAAI Press/MIT Press (1995)
Luck, M., d’Inverno, M.: Structuring a Z specification to provide a formal framework for autonomous agent systems. In: Bowen and Hinchey [99], pp. 47–62
Luck, M., d’Inverno, M.: Engagement and cooperation in motivated agent modelling. In: Zhang, C., Lukose, D. (eds.) DAI 1995. LNCS, vol. 1087, pp. 70–84. Springer, Heidelberg (1996)
Luck, M., Griffiths, N., d’Inverno, M.: From agent theory to agent construction: A case study. In: Jennings, N.R., Wooldridge, M.J., Müller, J.P. (eds.) ECAI-WS 1996 and ATAL 1996. LNCS (LNAI), vol. 1193, pp. 49–63. Springer, Heidelberg (1997)
Lupton, P.J.: Promoting forward simulation. In: Nicholls [504], pp. 27–49
Lüth, C., Karlsen, E.W., Kolyang, Westmeier, S., Wolff, B.: Hol-Z in the UniForM-workbench – a case study in tool integration for Z. In: Bowen et al. [85], pp. 116–134
MacDonald, A., Carrington, D.: Structuring Z specifications: Some choices. In: Bowen and Hinchey [99], pp. 203–223
Macdonald, R.: Z usage and abusage. Report no. 91003, RSRE, Ministry of Defence, Malvern, Worcestershire, UK (February 1991); This paper presents a miscellany of observations drawn from experience of using Z, shows a variety of techniques for expressing certain class of idea concisely and clearly, and alerts the reader to certain pitfalls which may trap the unwary
Mahony, B., Dong, J.S.: Adding timed concurrent processes to Object-Z: A case study in TCOZ. In: Bowen et al. [85], pp. 308–327
Mahony, B.P., Hayes, I.J.: A case-study in timed refinement: A central heater. In: Morris and Shaw [487], pp. 138–149
Mahony, B.P., Hayes, I.J.: A case-study in timed refinement: A mine pump. IEEE Transactions on Software Engineering 18(9), 817–826 (1992)
Mander, K.C., Polack, F.: Rigorous specification using structured systems analysis and Z. Information and Software Technology 37(5-6), 285–291 (1995); Revised version of [524]
Martin, A.: Encoding W: A logic for Z in 2OBJ. In: Woodcock and Larsen [689], pp. 462–481
Martin, A.: Machine-Assisted Theorem-Proving for Software Engineering. DPhil thesis, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (1995)
Mataga, P., Zave, P.: Formal specification of telephone features. In: Bowen and Hall [91], pp. 29–50
Mataga, P., Zave, P.: Multiparadigm specification of an AT&T switching system. In: Hinchey and Bowen [348], pp. 375–398
Mataga, P., Zave, P.: Using Z to specify telephone features. Information and Software Technology 37(5-6), 277–283 (1995); Revised version of [449]
Maung, I., Howse, J.R.: Introducing Hyper-Z – a new approach to object orientation in Z. In: Bowen and Nicholls [102], pp. 149–165
May, M.D.: Use of formal methods by a silicon manufacturer. In: Hoare, C.A.R. (ed.) Developments in Concurrency and Communication. University of Texas at Austin Year of Programming Series, ch. 4, pp. 107–129. Addison-Wesley Publishing Company, Reading (1990)
May, M.D., Barrett, G., Shepherd, D.E.: Designing chips that work. In: Hoare, C.A.R., Gordon, M.J.C. (eds.) Mechanized Reasoning and Hardware Design. Prentice Hall International Series in Computer Science, pp. 3–19 (1992)
May, M.D., Shepherd, D.E.: Verification of the IMS T800 microprocessor. In: Proc. Electronic Design Automation, London, UK, September 1987, pp. 605–615 (1987)
McDermid, J.A.: Special section on Z. IEE/BCS Software Engineering Journal 4(1), 25–72 (1989); A special issue on Z, introduced and edited by Prof. J. A. McDermid. See also [71,151,600,681]
McDermid, J.A. (ed.): The Theory and Practice of Refinement: Approaches to the Formal Development of Large-Scale Software Systems. Butterworth Scientific (1989); This book contains papers from the 1st Refinement Workshop held at the University of York, UK, 7–8 January 1988. Z-related papers include [400,496]
McDermid, J.A.: Formal methods: Use and relevance for the development of safety critical systems. In: Bennett, P.A. (ed.) Safety Aspects of Computer Control, Butterworth-Heinemann, Oxford (1993); This paper discusses a number of formal methods and summarizes strengths and weaknesses in safety critical applications; a major safety-related example is presented in Z
McMorran, M.A., Nicholls, J.E.: Z user manual. Technical Report TR12.274, IBM United Kingdom Laboratories Ltd, Hursley Park, Winchester, Hampshire SO21 2JN, UK (July 1989)
McMorran, M.A., Powell, S.: Z Guide for Beginners. Blackwell Scientific, Malden (1993)
Meira, S.L., Cavalcanti, A.L.C.: Modular object-oriented Z specifications. In: Nicholls [504], pp. 173–192
Meyer, B.: On formalism in specifications. IEEE Software 2(1), 6–26 (1985)
Mikk, E.: Compilation of Z specifications into C for automatic test result evaluation. In: Bowen and Hinchey [99], pp. 167–180
Mikušiak, L., Adamy, M., Seidmann, T.: Publishing formal specifications in Z notation on the WWW. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 871–874. Springer, Heidelberg (1997)
Mikušiak, L., Vojtek, V., Hasaralejko, J., Hanzelová, J.: Z browser – tool for visualization of Z specifications. In: Bowen and Hinchey [99], pp. 510–523
Minkowitz, C., Rann, D., Turner, J.H.: A C++ library for implementing specifications. In: France and Gerhart [265], pp. 61–75
Mitchell, R., Loomes, M., Howse, J.: Structuring formal specifications: A lesson relearned. Microprocessors and Microsystems 18(10), 593–599 (1994)
Mišić, V.B., Moser, S.: Formal approach to metamodeling: A generic objectoriented perspective. In: Embley, D.W. (ed.) ER 1997. LNCS, vol. 1331, pp. 243–256. Springer, Heidelberg (1997)
Mišić, V.B., Moser, S.: From formal metamodels to metrics: An object-oriented approach. In: Chen, J., Li, M., Mingins, C., Meyer, B. (eds.) Proc. 24th Conference on Technology of Object-Oriented Languages and Systems (TOOLS Asia), Beijing, China, September 1997, pp. 413–422 (1997)
Mišić, V.B., Velašević, D.: Formal specifications in software development: An overview. Yugoslav Journal for Operations Research 7(1), 79–96 (1997)
Mišić, V.B., Velašević, D., Lazarević, B.: Formal specification of a data dictionary for an extended ER data model. The Computer Journal 35(6), 611–622 (1992)
Moffett, J.D., Sloman, M.S.: A case study representing a model: To Z or not to Z. In: Nicholls [504], pp. 254–268
Monahan, B.Q.: Book review. Formal Aspects of Computing 1(1), 137–142 (1989); A review of Understanding z: A Specification Language and Its Formal Semantics by Mike Spivey [599]
Monahan, B.Q., Shaw, R.C.: Model-based specifications. In: McDermid, J.A. (ed.) Software Engineer’s Reference Book, ch. 21, Butterworth-Heinemann, Oxford (1991); This chapter contains a case study in Z, followed by a discussion of the respective trade-offs in specification between Z and VDM
Morgan, C.C.: Data refinement using miracles. Information Processing Letters 26(5), 243–246 (1988)
Morgan, C.C.: Procedures, parameters, and abstraction: Separate concerns. Science of Computer Programming 11(1) (October 1988)
Morgan, C.C.: The specification statement. ACM Transactions on Programming Languages and Systems (TOPLAS) 10(3) (July 1988)
Morgan, C.C.: Types and invariants in the refinement calculus. In: Proc. Mathematics of Program Construction Conference, Twente, The Netherlands (June 1989)
Morgan, C.C.: Programming from Specifications, 2nd edn. International Series in Computer Science (1994); This book presents a rigorous treatment of most elementary program development techniques, including iteration, recursion, procedures, parameters, modules and data refinement
Morgan, C.C., Robinson, K.A.: Specification statements and refinement. IBM Journal of Research and Development 31(5) (September 1987)
Morgan, C.C., Sanders, J.W.: Laws of the logical calculi. Technical Monograph PRG-78, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (September 1989); This document records some important laws of classical predicate logic. It is designed as a reservoir to be tapped by users of logic, in system development
Morgan, C.C., Sufrin, B.A.: Specification of the Unix filing system. IEEE Transactions on Software Engineering 10(2), 128–142 (1984)
Morgan, C.C., Vickers, T. (eds.) On the Refinement Calculus. Formal Approaches to Computing and Information Technology series (FACIT), Springer, Heidelberg (1994); This book collects together the work accomplished at the Oxford University Computing Laboratory on the refinement calculus: the rigorous development, from state-based assertional specification, of executable imperative code
Morgan, C.C., Woodcock, J.C.P.: What is a specification? In: Craigen, D., Summerskill, K. (eds.) Formal Methods for Trustworthy Computer Systems (FM 1989), Workshops in Computing, pp. 38–43. Springer, Heidelberg (1990)
Morgan, C.C., Woodcock, J.C.P. (eds.) 3rd Refinement Workshop, Workshops in Computing, Springer, Heidelberg (1991); The workshop was held at the IBM Laboratories, Hursley Park, UK, 9–11 January 1990. See [572]
Morrey, I., Siddiqi, J., Hibberd, R., Buckberry, G.: A toolset to support the construction and animation of formal specifications. Journal of Systems and Software 41(3), 147–160 (1998)
Morris, J.M., Shaw, R.C. (eds.) 4th Refinement Workshop, Workshops in Computing, Springer, Heidelberg (1991); The workshop was held at Cambridge, UK, 9–11 January 1991. For Z related papers, see [27,378,444,675,683,671]
Moser, S., Mišić, V.B.: Measuring class coupling and cohesion: A formal metamodel approach. In: Proc. 4th Asia Pacific Software Engineering Conference APSEC 1997, Hong Kong (December 1997)
Murray, L., Carrington, D., MacColl, I., McDonald, J., Strooper, P.: Formal derivation of finite state machines for class testing. In: Bowen et al. [85], pp. 42–59
Naftalin, M., Bertrán, M., Denvir, T. (eds.): FME 1994. LNCS, vol. 873. Springer, Heidelberg (1994); Z-related papers include [94,162,177,247,250,255,366,431,514]. B-related papers include [185,546,627]
Narayana, K.T., Dharap, S.: Formal specification of a look manager. IEEE Transactions on Software Engineering 16(9), 1089–1103 (1990); A formal specification of the look manager of a dialog system is presented in Z. This deals with the presentation of visual aspects of objects and the editing of those visual aspects
Narayana, K.T., Dharap, S.: Invariant properties in a dialog system. ACM SIGSOFT Software Engineering Notes 15(4), 67–79 (1990)
Nash, T.C.: Using Z to describe large systems. In: Nicholls [502], pp. 150–178
Nehlig, P.W., Duce, D.A.: GKS-9x: The design output primitive, an approach to specification. Computer Graphics Forum 13(3), C–381–C–392 (1994)
Neil, M., Ostrolenk, G., Tobin, M., Southworth, M.: Lessons from using Z to specify a software tool. IEEE Transactions on Software Engineering 24(1), 15–23 (1998)
Neilson, D.S.: Hierarchical refinement of a Z specification. In: McDermid [457]
Neilson, D.S.: From Z to C: Illustration of a rigorous development method. Technical Monograph PRG-101, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (1990)
Neilson, D.S.: Machine support for Z: The zedB tool. In: Nicholls [504], pp. 105–128
Neilson, D.S., Prasad, D.: zedB: A proof tool for Z built on B. In: Nicholls [506], pp. 243–258
Nguyen, K., Duke, R.: A formal analysis method for conceptual modelling of information systems. In: Habrias [303], pp. 93–110
Nicholls, J.E.: Working with formal methods. Journal of Information Technology 2(2), 67–71 (1987)
Nicholls, J.E. (ed.): Z User Workshop, Oxford 1989. Workshops in Computing. Springer, Heidelberg (1990); Proceedings of the 4th Z User Meeting, Wolfson College & Rewley House, Oxford, UK, 14–15 December 1989. Published in collaboration with the British Computer Society. For the opening address see [515]. For individual papers, see [42,116,118,161,195,261,296,327,343,383,413,493,522,588,608,669]
Nicholls, J.E.: A survey of Z courses in the UK. In: Z User Workshop, Oxford, [504], pp. 343–350 (1990)
Nicholls, J.E. (ed.): Z User Workshop, Oxford 1990, Workshops in Computing. Springer, Heidelberg (1991); Proceedings of the 5th Z User Meeting, Lady Margaret Hall, Oxford, UK, 17–18 December 1990. Published in collaboration with the British Computer Society. For individual papers, see [29,109,129,159,273,297,328,344,359,385,388,410,461,472,498,503,512,534,569] [670,697]. The proceedings also includes an Introduction and Opening Remarks, a Selected Z Bibliography, a selection of posters and information on Z tools
Nicholls, J.E.: Domains of application for formal methods. In: Z User Workshop, York 1991, [506], pp. 145–156 (1991)
Nicholls, J.E. (ed.) Z User Workshop, York 1991, Workshops in Computing, Springer, Heidelberg (1992); Proceedings of the 6th Z User Meeting, York, UK. Published in collaboration with the British Computer Society. For individual papers, see [20,33,179,133,196,229,319,499,505,525,553,589,639,655,686,702]
Nicholls, J.E.: Plain guide to the Z base standard. In: Bowen and Nicholls [102], pp. 52–61
Nicholls, J.E., et al.: Z in the development process. Technical Report PRG-TR- 1-89, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (June 1989); Proceedings of a discussion workshop held on 15 December 1988 in Oxford, UK, with contributions by Peter Collins, David Cooper, Anthony Hall, Patrick Hall, Brian Hepworth, Ben Potter and Andrew Ricketts
Nix, C.J., Collins, B.P.: The use of software engineering, including the Z notation, in the development of CICS. Quality Assurance 14(3), 103–110 (1988)
Norcliffe, A., Slater, G.: Mathematics for Software Construction. Series in Mathematics and its Applications. Ellis Horwood (1991); Contents: Why mathematics; Getting started: sets and logic; Developing ideas: schemas; Functions; Functions in action; A real problem from start to finish: a drinks machine; Sequences; Relations; Generating programs from specifications: refinement; The role of proof; More examples of specifications; Concluding remarks; Answers to exercises
Norcliffe, A., Valentine, S.: Z readers video course. PAVIC Publications (1992); Sheffield Hallam University, 33 Collegiate Crescent, Sheffield S10 2BP, UK. Video-based Training Course on the Z Specification Language. The course consists of 5 videos, each of approximately one hour duration, together with supporting texts and case studies
Norcliffe, A., Valentine, S.H.: A video-based training course in reading Z specifications. In: Nicholls [504], pp. 337–342
Normington, G.: Cleanroom and Z. In: Bowen and Nicholls [102], pp. 281–293
O’ Halloran, C.: Evaluation semantics in Z. In: Naftalin et al. [490], pp. 502–518
Oakley, B.: The state of use of formal methods. In: Nicholls [502], pp. 1–5; A record of the opening address at ZUM 1989
Olderog, E.-R.: Combining specification techniques for processes, data and time. In: Bowen et al. [85], pp. 192, Abstract
Paige, R.: Comparing extended Z with a heterogeneous notation for reasoning about time and space. In: Bowen et al. [85], pp. 214–232
Parker, C.E.: Z tools catalogue. ZIP project report ZIP/BAe/90/020, British Aerospace, Software Technology Department,Warton PR4 1AX, UK (May 1991)
Parker, H., Polack, F., Mander, K.C.: The industrial trial of SAZ: Reflections on the use of an integrated specification method. In: Habrias [303], pp. 111–129
Parnas, D.L.: Language-free mathematical models for software design. In: Bowen and Hinchey [99], pp. 3–4; Extended abstract.
Parnas, D.L.: Teaching programming as engineering. In: Bowen and Hinchey [99], pp. 471–481
Phillips, M.: CICS/ESA 3.1 experiences. In: Nicholls [502], pp. 179–185 (Z was used to specify 37,000 lines out of 268,000 lines of code in the IBM CICS/ESA 3.1 release. The initial development benefit from using Z was assessed as being a 9% improvement in the total development cost of the release, based on the reduction of programmer days fixing problems)
Pilling, M., Burns, A., Raymond, K.: Formal specifications and proofs of inheritance protocols for real-time scheduling. IEE/BCS Software Engineering Journal 5(5), 263–279 (1990)
Polack, F., Mander, K.C.: Software quality assurance using the SAZ method. In: Bowen and Hall [91], pp. 230–249
Polack, F., Whiston, M., Hitchcock, P.: Structured analysis – a draft method for writing Z specifications. In: Nicholls [506], pp. 261–286
Polack, F., Whiston, M., Mander, K.C.: The SAZ project: Integrating SSADM and Z. In: Woodcock and Larsen [689], pp. 541–557
Potter, B.F., Sinclair, J.E., Till, D.: An Introduction to Formal Specification and Z, 2nd edn. Prentice Hall International Series in Computer Science (1996) (Contents: Formal specification in the context of software engineering; An informal introduction to logic and set theory; A first specification; The Z notation: the mathematical language, relations and functions, schemas and specification structure; A first specification; Formal reasoning; From specification to program: data and operation refinement, operation decomposition; From theory to practice)
Potter, B.F., Till, D.: The specification in Z of gateway functions within a communications network. In: Proc. IFIP WG10.3 Conference on Distributed Processing, October 1987, Elsevier Science Publishers, North-Holland (1987)
Pratten, C.H.: An introduction to proving AMN specifications with PVS and the AMN-PROOF tool. In: Habrias [303], pp. 149–165
Prehn, S., Toetenel, W.J. (eds.): VDM 1991. LNCS, vol. 551. Springer, Heidelberg (1991) (The 4th VDM-Europe Symposium was held at Noordwijkerhout, The Netherlands, 21–25 October 1991. Papers with relevance to Z include [19,43,170,221,279,356,661,674,701]. See also [531])
Prehn, S., Toetenel, W.J. (eds.): VDM 1991. LNCS, vol. 552. Springer, Heidelberg (1991) (Papers with relevance to Z include [8,684]. See also [530])
Rafsanjani, G.-H.B., Colwill, S.J.: From Object-Z to C + + : A structural mapping. In: Bowen and Nicholls [102], pp. 166–179
RAISE Language Group. The RAISE Specification Language. BCS Practitioner Series. Prentice Hall International (1992)
Randell, G.P.: Data flow diagrams and Z. In: Nicholls [504], pp. 216–227
Rann, D., Turner, J., Whitworth, J.: Z: A Beginner’s Guide. Chapman & Hall, London (1994)
Ratcliff, B.: Introducing Specification Using Z: A Practical Case Study Approach. International Series in Software Engineering. McGraw-Hill, New York (1994)
Ravn, A.P., Rischel, H., Stavridou, V.: Provably correct safety critical software. In: Proc. IFAC Safety of Computer Controlled Systems 1990 (SAFECOMP 1990), Pergamon Press, Oxford (1990)
Rawson, M.: OOPSLA 1993: Workshop on formal specification of object-oriented systems – position paper. In: Kilov, H., Harvey, W. (eds.) Proc. Workshop on Specification of Behavioral Semantics in Object-Oriented Information Modeling, Washington DC, USA, pp. 125–135. OOPSLA (1993)
Rawson, M., Allen, P.: Synthesis – an integrated, object-oriented method and tool for requirements specification in Z. In: Bryant and Semmens [121]
Read, T.J.: Formal specification of reusable Ada software packages. In: Burns, A. (ed.) Proc. Towards Ada 9X Conference, pp. 98–117 (1991)
Reed, J.N.: Semantics-based tools for a specification support environment. In: Main, M.G., Mislove, M.W., Melton, A.C., Schmidt, D. (eds.) MFPS 1987. LNCS, vol. 298, Springer, Heidelberg (1988)
Reed, J.N., Sinclair, J.E.: An algorithm for type-checking Z: A Z specification. Technical Monograph PRG-81, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (March 1990)
Reilly, C.: Exploring specifications with Mathematica. In: Bowen and Hinchey [99], pp. 408–420
Reizer, N.R., Abowd, G.D., Meyers, B.C., Place, P.R.H.: Using formal methods for requirements specification of a proposed POSIX standard. In: Proc. IEEE International Conference on Requirements Engineering (ICRE 1994) (April 1994)
Reynolds, G.J.: Yet another approach to the formal specification of a configurable graphics system. In: Proc. Eurographics Association Formal Methods in Computer Graphics (June 1991)
Ritchie, B., Bicarregui, J., Haughton, H.P.: Experiences in using the abstract machine notation in a GKS case study. In: Naftalin et al. [490], pp. 93–104
Robinson, K.A.: Refining Z specifications to programs. In: Proc. Australian Software Engineering Conference, pp. 87–97 (1987)
Rose, G.A.: Object-Z. In: Stepney et al. [613], pp. 59–77
Rose, G.A., Robinson, P.: A case study in formal specifications. In: Proc. First Australian Software Engineering Conference (May 1986)
Ruddle, A.R.: Formal methods in the specification of real-time, safety-critical control systems. In: Bowen and Nicholls [102], pp. 131–146
Rudkin, P.: Modelling information objects in Z. In: de Meer, J. (ed.) Proc. International Workshop on ODP, Elsevier Science Publishers, North-Holland (1992)
Rushby, J.: Mechanizing formal methods: Challenges and opportunities. In: Bowen and Hinchey [99], pp. 105–113
Saaltink, M.: Z and Eves. In: Nicholls [506], pp. 223–242
Saaltink, M.: The Z/EVES system. In: Bowen et al. [101], pp. 72–85
Saiedian, H.: Mathematics of computing. Journal of Computer Science Education 3(3), 203–221 (1992)
Saiedian, H.: Information systems and the engineering paradigm: Integrating the formal methods technology into the development process. International Journal of Computing and Information Technology 2(4), 277–290 (1994)
Saiedian, H.: An invitation to formal methods. IEEE Computer 29(4), 16–30 (1996) (This article includes an introduction to and commentaries by Jonathan P. Bowen, Ricky W. Butler, David L. Dill, Robert L. Glass, David Gries, J. Anthony Hall, Michael G. Hinchey, C. Michael Holloway, Daniel Jackson, Cliff B. Jones, Michael J. Lutz, David L. Parnas, John Rushby, Jeannette Wing, and Pamela Zave in a virtual roundtable on formal methods)
Saiedian, H.: Formal methods in information systems engineering. In: Thayer, R., Dorfman, M. (eds.) Software Requirements Engineering, pp. 336–349. IEEE Computer Society Press, Los Alamitos (1997)
Saiedian, H.: Information systems design is an engineering process. In: Kent, A. (ed.) Encyclopedia of Information Science, vol. 60, pp. 120–133. Marcel Dekker, New York (1997)
Saiedian, H., Hinchey, M.G.: Issues surrounding the transferring of formal methods technology into the actual workplace. In: Proc. International Workshop on Formal Methods Application in Software Engineering Practice. 17th International Conference on Software Engineering, Seattle, USA, April 1995, pp. 69–76. IEEE Computer Society Press, Los Alamitos (1995)
Saiedian, H., Hinchey, M.G.: Challenges in the successful transfer of formal methods technology into industrial applications. Information and Software Technology 38(5), 313–321 (1996)
Sampaio, A.C.A., Meira, S.L.: Modular extensions to Z. In: Bjørner et al. [51], pp. 211–232
Sanders, P., Johnson, M., Tinker, R.: From Z specifications to functional implementations. British Telecom Technology Journal 7(4) (October 1989)
Santen, T.: On the semantic relation of Z and HOL. In: Bowen et al. [85], pp. 96–115
Schenke, M., Ravn, A.P.: Refinement from a control problem to programs. In: Abrial et al. [10], pp. 403–427
Scholz, D., Petersohn, C.: Towards a formal semantics for an integrated SA/RT & Z specification language. In: Hinchey and Liu [350], pp. 28–37
Schuman, S.A., Pitt, D.H.: Object-oriented subsystem specification. In: Meertens, L.G.L.T. (ed.) Program Specification and Transformation, pp. 313–341. Elsevier Science Publishers, North-Holland (1987)
Schuman, S.A., Pitt, D.H., Byers, P.J.: Object-oriented process specification. In: Rattray, C. (ed.) Specification and Verification of Concurrent Systems, pp. 21–70. Springer, Heidelberg (1990)
Semmens, L.T., Allen, P.M.: Using Yourdon and Z: An approach to formal specification. In: Nicholls [504], pp. 228–253
Semmens, L.T., France, R.B., Docker, T.W.G.: Integrated structured analysis and formal specification techniques. The Computer Journal 35(6), 600–610 (1992)
Sennett, C.T.: Formal specification and implementation. In: Sennett, C.T. (ed.) High-Integrity Software. Computer Systems Series, Pitman (1989)
Sennett, C.T.: Using refinement to convince: Lessons learned from a case study. In: Morgan and Woodcock [485], pp. 172–197
Sennett, C.T.: Demonstrating the compliance of Ada programs with Z specifications. In: Jones et al. [386]
Shepherd, D.E.: Verified microcode design. Microprocessors and Microsystems 14(10), 623–630 (1990) (This article is part of a special feature on Formal aspects of microprocessor design, edited by H. S. M. Zedan. See also [72])
Shepherd, D.E., Wilson, G.: Making chips that work. New Scientist 1664, 61–64 (1989) (A general article containing information on the formal development of the T800 floating-point unit for the Transputer including the use of Z)
Sheppard, D.: An Introduction to Formal Specification with Z and VDM. International Series in Software Engineering. McGraw-Hill, New York (1995)
Sherrell, L.B., Carver, D.L.: Z meets Haskell: A case study. In: COMPSAC 1993: Proc. 17th Annual International Computer Software and Applications Conference, November 1993, pp. 320–326. IEEE Computer Society Press, Los Alamitos (1993) (The paper traces the development of a simple system, the class manager’s assistant, from an existing Z specification, through design in Z, to a Haskell implementation)
Sherrell, L.B., Carver, D.L.: Experiences in translating Z designs to Haskell implementations. Software—Practice and Experience 24(12), 1159–1178 (1994)
Sherrell, L.B., Carver, D.L.: FunZ: An intermediate specification language. The Computer Journal 38(3), 193–206 (1995)
Shih, T.K.: A Z specification approach to multimedia modeling. Computers and Artificial Intelligence 16(5), 465–495 (1997)
Shih, T.K., Lin, F.Y.: An operational semantics approach to disciplined exceptions in logic programming. Computers and Artificial Intelligence 14(1), 1–33 (1995)
Shih, T.K., Wang, C.C., Chung, C.M.: Using Z to specify object-oriented software complexity measures. Information and Software Technology 39(8), 515–529 (1997)
Sinclair, J.E., Ince, D.C.: The use of Z in specifying securuty properties. In: Habrias [303], pp. 27–39
Sinnott, R.O., Turner, K.J.: Modeling ODP viewpoints. In: Kilov, H., Harvey, W., Mili, H. (eds.) Proc. Workshop on Precise Behavioral Specifications in Object-Oriented Information Modeling, OOPSLA 1994, Portland, USA, October 24, pp. 121–128. OOPSLA (1994)
Sinnott, R.O., Turner, K.J.: Specifying multimedia binding objects in Z. In: Spaniol, O., Meyer, B., Linnhoff-Popien, C. (eds.) TreDS 1996. LNCS, vol. 1161, pp. 244–258. Springer, Heidelberg (1996)
Sinnott, R.O., Turner, K.J.: Specifying ODP computational objects in Z. In: Najm, E., Stefani, J.-B. (eds.) Proc. 1st IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems, March 1996, pp. 375–390. Chapman & Hall, Boca Raton (1996)
Sinnott, R.O., Turner, K.J.: Type checking in open distributed systems: A complete model and its Z specification. In: Rolia, J., Slonim, J., Botsford, J. (eds.) Proc. IFIP/IEEE International Conference on Open Distributed Processing and Distributed Platforms (ICODP/ICDP), Toronto, Canada, May 26-30, pp. 85–96. Chapman & Hall, Boca Raton (1997)
Smith, A.: The Knuth-Bendix completion algorithm and its specification in Z. In: Nicholls [502], pp. 195–220
Smith, A.: On recursive free types in Z. In: Nicholls [506], pp. 3–39
Smith, G.: An Object-Oriented Approach to Formal Specification. PhD thesis, Department of Computer Science, University of Queensland, St. Lucia 4072, Australia (October 1992) (A detailed description of a version of Object-Z similar to (but not identical to) that in [237]. The thesis also includes a formalization of temporal logic history invariants and a fully-abstract model of classes in Object-Z)
Smith, G.: A object-oriented development framework for Z. In: Bowen and Hall [91], pp. 89–107
Smith, G.: Extending W for Object-Z. In: Bowen and Hinchey [99], pp. 276–295
Smith, G.: A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing 7(3), 289–313 (1995)
Smith, G., Duke, R.: Modelling a cache coherence protocol using Object-Z. In: Proc. 13th Australian Computer Science Conference (ACSC-13), pp. 352–361 (1990)
Smith, P., Keighley, R.: The formal development of a secure transaction mechanism. In: Prehn and Toetenel [530], pp. 457–476
Sommerville, I.: Software Engineering, 4th edn. ch. 9, pp. 153–168. Addison-Wesley Publishing Company, Reading (1992) (A chapter entitled Model-Based Specification including examples using Z)
Sørensen, I.H.: A specification language. In: Staunstrup, J. (ed.) Program Specification 1981. LNCS, vol. 134, pp. 381–401. Springer, Heidelberg (1981)
Sørensen, I.H.: Using B to specify, verify and design hardware circuits. In: Bowen et al. [85], pp. 60–65 (Extended abstract)
Spivey, J.M.: Understanding Z: A Specification Language and its Formal Semantics. Cambridge Tracts in Theoretical Computer Science, vol. 3. Cambridge University Press, Cambridge (January 1988) (Published version of 1985 DPhil thesis)
Spivey, J.M.: An introduction to Z and formal specifications. IEE/BCS Software Engineering Journal 4(1), 40–50 (1989)
Spivey, J.M.: A guide to the zed style option. Oxford University Computing Laboratory, Oxford (1990) (A description of the Z style option ‘zed.sty’ for use with the LaTeX document preparation system [408]. This early and influential style option is now largely superseded by fuzz.sty [603], oz.sty [398] and other style options)
Spivey, J.M.: Specifying a real-time kernel. IEEE Software 7(5), 21–28 (1990) (This case study of an embedded real-time kernel shows that mathematical techniques have an important role to play in documenting systems and avoiding design flaws)
Spivey, J.M.: The fuzz Manual. Computing Science Consultancy, 34 Westlands Grove, Stockton Lane, York YO3 0EF, UK, 2nd edn. (July 1992) (The manual describes a Z type-checker and ‘fuzz.sty’ style option for LaTeX documents [408]. The package is compatible with the book, The Z Notation: A Reference Manual by the same author [604])
Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science (1992) (This is a revised edition of the first widely available reference manual on Z originally published in 1989. The book provides a complete and definitive guide to the use of Z in specifying information systems, writing specifications and designing implementations. See also the draft Z standard [112]. Contents: Tutorial introduction; Background; The Z language; The mathematical tool-kit; Sequential systems; Syntax summary; Changes from the first edition; Glossary)
Spivey, J.M.: The consistency theorem for free type definitions in Z. Formal Aspects of Computing 8, 369–375 (1996)
Spivey, J.M.: Richer types for Z. Formal Aspects of Computing 8, 565–584 (1996)
Spivey, J.M., Sufrin, B.A.: Type inference in Z. In: Bjørner et al. [51], pp. 426–438 (Also published as [608])
Spivey, J.M., Sufrin, B.A.: Type inference in Z. In: Nicholls [502], pp. 6–31
Steggles, P., Hulance, J.: Z tools survey. Imperial Software Technology Ltd. / Formal Systems (Europe) Ltd. (June 1994)
Stepney, S.: High Integrity Compilation: A Case Study. Prentice-Hall, Englewood Cliffs (1993) (Outlines a method for developing a high assurance compiler based on many concepts and notations, including denotational semantics, the Z specification language and the Prolog programming language based on a fully worked case study)
Stepney, S.: Testing as abstraction. In: Bowen and Hinchey [99], pp. 137–151
Stepney, S., Barden, R.: Annotated Z bibliography. Bulletin of the European Association of Theoretical Computer Science 50, 280–313 (1993)
Stepney, S., Barden, R., Cooper, D. (eds.): Object Orientation in Z. Workshops in Computing. Springer, Heidelberg (1992) (This is a collection of papers describing various OOZ approaches – Hall, ZERO, MooZ, Object-Z, OOZE, Schuman & Pitt, Z + + , ZEST and Fresco (an objectoriented VDM method) – in the main written by the methods’ inventors, and all specifying the same two examples. The collection is a revised and expanded version of a ZIP report distributed at the 1991 Z User Meeting at York)
Stepney, S., Barden, R., Cooper, D.: A survey of object orientation in Z. IEE/BCS Software Engineering Journal 7(2), 150–160 (1992)
Stepney, S., Cooper, D., Woodcock, J.C.P.: More powerful data refinement in Z. In: Bowen et al. [85], pp. 284–307
Stepney, S., Lord, S.P.: Formal specification of an access control system. Software—Practice and Experience 17(9), 575–593 (1987)
Stocks, P.: Applying Formal Methods to Software Testing. PhD thesis, Department of Computer Science, University of Queensland, St. Lucia 4072, Australia (1993)
Stocks, P., Carrington, D.: A framework for specification-based testing. IEEE Transactions on Software Engineering 22(11), 777–793 (1996)
Stocks, P., Carrington, D.A.: Deriving software test cases from formal specifications. In: 6th Australian Software Engineering Conference, July 1991, pp. 327–340 (1991)
Stocks, P., Carrington, D.A.: Test template framework: A specification-based testing case study. In: Proc. International Symposium on Software Testing and Analysis (ISSTA 1993), June 1993, pp. 11–18 (1993) (Also available in a longer form as Technical Report UQCS-255, Department of Computer Science, University of Queensland)
Stocks, P., Carrington, D.A.: Test templates: A specification-based testing framework. In: Proc. 15th International Conference on Software Engineering, May 1993, pp. 405–414 (1993) (Also available in a longer form as Technical Report UQCS-243, Department of Computer Science, University of Queensland)
Stocks, P., Raymond, K., Carrington, D., Lister, A.: Modelling open distributed systems in Z. Computer Communications 15(2), 103–113 (1992) (In a special issue on the practical use of FDTs (Formal Description Techniques) in communications and distributed systems, edited by Dr. Gordon S. Blair)
Stoddart, W.J.: An introduction to the Event Calculus. In: Bowen et al. [101], pp. 10–34
Stoddart, W.J.: The specification and refinement of an environmental model. In: Bowen et al. [85], pp. 24–41
Stoddart, W.J., Fencott, C., Dunne, S.: Modelling hybrid systems in Z. In: Habrias [303], pp. 11–25
Stoddart, W.J., Knaggs, P.: The Event Calculus (formal specification of real time systems by means of diagrams and Z schemas). In: Proc. 5th International Conference on Putting into Practice Methods and Tools for Information System Design, Nantes, France, September 1992, University of Nantes, Institute Universitaire de Technologie (1992)
Storey, A.C., Haughton, H.P.: A strategy for the production of verifiable code using the B method. In: Naftalin et al. [490], pp. 346–365
Strulo, B.: How firing conditions help inheritance. In: Bowen and Hinchey [99], pp. 264–275
Sufrin, B.A.: Formal system specification: Notation and examples. In: Neel, D. (ed.) Tools and Notations for Program Construction, Cambridge University Press, Cambridge (1982) (An example of a filing system specification, this was the first published use of the schema notation to put together states)
Sufrin, B.A.: Towards formal specification of the ICL data dictionary. ICL Technical Journal (August 1984)
Sufrin, B.A.: Formal methods and the design of effective user interfaces. In: Harrison, M.D., Monk, A.F. (eds.) People and Computers: Designing for Usability, Cambridge University Press, Cambridge (1986)
Sufrin, B.A.: Formal specification of a display-oriented editor. In: Gehani, N., McGettrick, A.D. (eds.) Software Specification Techniques. International Computer Science Series, pp. 223–267. Addison-Wesley Publishing Company, Reading (1986) (Originally published in Science of Computer Programming, 1:157–202, 1982)
Sufrin, B.A.: A formal framework for classifying interactive information systems. In: IEE Colloquium on Formal Methods and Human-Computer Interaction, London, UK. IEE Digest, vol. 09, pp. 4/1–14. The Institution of Electrical Engineers (1987)
Sufrin, B.A.: Effective industrial application of formal methods. In: Ritter, G.X. (ed.) Information Processing 89: Proc. 11th IFIP Computer Congress, pp. 61–69. Elsevier Science Publishers, North-Holland (1989) (This paper presents a Z model of the Unix make utility)
Sufrin, B.A., Jifeng, H.: Specification, analysis and refinement of interactive processes. In: Harrison, M.D., Thimbleby, H. (eds.) Formal Methods in Human-Computer Interaction, ch. 6. Cambridge Series on Human- Computer Interaction, vol. 2, pp. 153–200. Cambridge University Press, Cambridge (1990) (A case study on using Z for process modelling)
Sufrin, B.A., Woodcock, J.C.P.: Towards the formal specification of a simple programming support environment. IEE/BCS Software Engineering Journal 2(4), 86–94 (1987)
Swatman, P.A.: Increasing Formality in the Specification of High-Quality Information Systems in a Commercial Context. PhD thesis, Curtin University of Technology, School of Computing, Perth, Western Australia (July 1992)
Swatman, P.A.: Using formal specification in the acquisition of information systems: Educating information systems professionals. In: Bowen and Nicholls [102], pp. 205–239
Swatman, P.A., Fowler, D., Gan, C.Y.M.: Extending the useful application domain for formal methods. In: Nicholls [506], pp. 125–144
Swatman, P.A., Swatman, P.M.C.: Formal specification: An analytic tool for (management) information systems. Journal of Information Systems 2(2), 121–160 (1992)
Swatman, P.A., Swatman, P.M.C.: Is the information systems community wrong to ignore formal specification methods? In: Clarke, R., Cameron, J. (eds.) Managing Information Technology’s Organisational Impact, October 1992, Elsevier Science Publishers, North-Holland (1992)
Swatman, P.A., Swatman, P.M.C.: Managing the formal specification of information systems. In: Proc. International Conference on Organization and Information Systems (September 1992)
Swatman, P.A., Swatman, P.M.C., Duke, R.: Electronic data interchange: A high-level formal specification in Object-Z. In: Proc. 6th Australian Software Engineering Conference (ASWEC 1991), Sidney, Australia (July 1991)
Taguchi, K., Araki, K.: The state-based CCS semantics for concurrent Z specification. In: Hinchey and Liu [350], pp. 283–292
Thompson, S.: Specification techniques [9004-0316]. ACM Computing Reviews 31(4), 213 (1990) (A review of Formal methods applied to a floating-point number system [35])
Till, D. (ed.): 6th Refinement Workshop. Workshop in Computing. Springer, Heidelberg (1994) (The workshop was held at City University, London, UK, 5–7 January 1994. See [256,411])
Todd, B.S.: A model-based diagnostic program. IEE/BCS Software Engineering Journal 2(3), 54–63 (1987)
Todd, B.S., Ledger, W.L.: A computer-based flowcharting system for clinical protocols. Medical Informatics 20(3), 177–198 (1995)
Took, R.: The presenter – a formal design for an autonomous display manager. In: Sommerville, I. (ed.) Software Engineering Environments, pp. 151–169. Peter Peregrinus, London (1986)
Toyn, I.: Formal reasoning in the Z notation using CADiZ. In: Proc. 2nd Workshop on User Interfaces to Theorem Provers, York (July 1996)
Toyn, I.: Innovations in standard Z notation. In: Bowen et al. [85], pp. 193–213
Toyn, I., McDermid, J.A.: CADiZ: An architecture for Z tools and its implementation. Software—Practice and Experience 25(3), 305–330 (1995)
Traynor, O., Kearney, P., Kazmierczak, E.: Li Wang, and E. Karlsen. Extending Z with modules. Australian Computer Science Communications 17(1) (1995); Kanchanasut, K., Levy, J.-J. (eds.): ACSC 1995. LNCS, vol. 1023. Springer, Heidelberg (1995)
Valentine, S.: The programming language Z− −. Information and Software Technology 37(5-6), 293–301 (1995)
Valentine, S.H.: Z− −, an executable subset of Z. In: Nicholls [506], pp. 157–187
Valentine, S.H.: Putting numbers into the mathematical toolkit. In: Bowen and Nicholls [102], pp. 9–36
Valentine, S.H.: An algebraic introduction of real numbers into Z. In: Habrias [303], pp. 183–204
Valentine, S.H.: Equal rights for schemas in Z. In: Bowen and Hinchey [99], pp. 183–202
Valentine, S.H.: Inconsistency and undefinedness in Z – a practical guide. In: Bowen et al. [85], pp. 233–249
van Diepen, M.J., van Hee, K.M.: A formal semantics for Z and the link between Z and the relational algebra. In: Bjørner et al. [51], pp. 526–551
van Hee, K.M., Somers, L.J., Voorhoeve, M.: Z and high level Petri nets. In: Prehn and Toetenel [530], pp. 204–219
van Zuylen, H.J. (ed.): The REDO Compendium: Reverse Engineering for Software Maintenance. John Wiley & Sons, Chichester (1993) (An overview of the results of the ESPRIT REDO project, including the use of Z and Z + + . See in particular Chapter 16, also published in a longer form as [414])
Waldén, M., Sere, K.: Refining action systems with B-tool. In: Gaudel and Woodcock [280], pp. 85–104
Weber, M.: Combining Statecharts and Z for the design of safety-critical control systems. In: Gaudel and Woodcock [280], pp. 307–326
West, M.M.: Types and sets in Gödel and Z. In: Bowen and Hinchey [99], pp. 389–407
West, M.M., Eaglestone, B.M.: Software development: Two approaches to animation of Z specifications using Prolog. IEE/BCS Software Engineering Journal 7(4), 264–276 (1992)
Wezeman, C.D.: Using Z for network modelling: An industrial experience report. Computer Standards & Interfaces 17(5-6), 631–638 (1995)
Wezeman, C.D., Judge, A.: Z for managed objects. In: Bowen and Hall [91], pp. 108–119
Whitty, R.W.: Structural metrics for Z specifications. In: Nicholls [502], pp. 186–191
Whysall, P.J., McDermid, J.A.: An approach to object-oriented specification using Z. In: Nicholls [504], pp. 193–215
Whysall, P.J., McDermid, J.A.: Object-oriented specification and refinement. In: Morris and Shaw [487], pp. 151–184
Wing, J.M.: A specifier’s introduction to formal methods. IEEE Computer 23(9), 8–24 (1990)
Wing, J.M.: Hints for writing specifications. In: Bowen and Hinchey [99], pp. 497
Wing, J.M., Zaremski, A.M.: Unintrusive ways to integrate formal specifications in practice. In: Prehn and Toetenel [530], pp. 545–570
Wood, K.R.: The elusive software refinery: a case study in program development. In: Morris and Shaw [487], pp. 281–325
Wood, K.R.: A practical approach to software engineering using Z and the refinement calculus. ACM Software Engineering Notes 18(5), 79–88 (1993)
Wood, W.G.: Application of formal methods to system and software specification. ACM SIGSOFT Software Engineering Notes 15(4), 144–146 (1990)
Woodcock, J.C.P.: Teaching how to use mathematics for large-scale software development. Bulletin of BCS-FACS (July 1988)
Woodcock, J.C.P.: Calculating properties of Z specifications. ACM SIGSOFT Software Engineering Notes 14(4), 43–54 (1989)
Woodcock, J.C.P.: Mathematics as a management tool: Proof rules for promotion. In: Proc. 6th Annual CSR Conference on Large Software Systems, Bristol, UK (September 1989)
Woodcock, J.C.P.: Structuring specifications in Z. IEE/BCS Software Engineering Journal 4(1), 51–66 (1989)
Woodcock, J.C.P.: Z. In: Craigen, D., Summerskill, K. (eds.) Formal Methods for Trustworthy Computer Systems (FM 1989). Workshops in Computing, pp. 57–62. Springer, Heidelberg (1990)
Woodcock, J.C.P.: Implementing promoted operations in Z. In: Morris and Shaw [487], pp. 366–378
Woodcock, J.C.P.: A tutorial on the refinement calculus. In: Prehn and Toetenel [531], pp. 79–140
Woodcock, J.C.P.: The rudiments of algorithm design. The Computer Journal 35(5), 441–450 (1992)
Woodcock, J.C.P., Brien, S.M.: \(\mathcal{W}\): A logic for Z. In: Nicholls [506], pp. 77–96
Woodcock, J.C.P., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science (1996) (This book contains enough material for three complete courses of study. It provides an introduction to the world of logic, sets and relations. It explains the use of the Z notation in the specification of realistic systems. It shows how Z specifications may be refined to produce executable code; this is demonstrated in a selection of case studies. The book strikes a balance between the formality of mathematics and the practical needs of industrial software development, following to the draft ISO standard for Z. It is based upon the experience of the authors in teaching Z to a wide variety of audiences. A set of exercises, solutions, and transparency masters is available on-line to complement the book)
Woodcock, J.C.P., Gardiner, P.H.B., Hulance, J.R.: The formal specification in Z of Defence Standard 00-56. In: Bowen and Hall [91], pp. 9–28
Woodcock, J.C.P., Larsen, P.G. (eds.): FME 1993. LNCS, vol. 670. Springer, Heidelberg (1993) (The 1st FME Symposium was held at Odense, Denmark, 19–23 April 1993. Zrelated papers include [103,165,254,372,447,526])
Woodcock, J.C.P., Larsen, P.G.: Guest editorial. IEEE Transactions on Software Engineering 21(2), 61–62 (1995) (Best papers from the FME’93 Symposium [689]. See [49,63,168,373])
Woodcock, J.C.P., Loomes, M.: Software Engineering Mathematics: Formal Methods Demystified. Pitman (1988) (Also published as: Software Engineering Mathematics, Addison-Wesley, 1989)
Woodcock, J.C.P., Morgan, C.C.: Refinement of state-based concurrent systems. In: Bjørner et al. [51], pp. 340–351 (Work on combining Z and CSP)
Woon, I.M.Y., Loh, W.L.: Formal derivation to object-oriented implementation of financial policies. International Journal of Computer Applications in Technology 10(5-6), 316–326 (1997)
Worden, R.: Fermenting and distilling. In: Bowen and Hall [91], pp. 1–6
Wordsworth, J.B.: Teaching formal specification methods in an industrial environment. In: Proc. Software Engineering 1986, London, IEE/BCS, Peter Peregrinus (1986)
Wordsworth, J.B.: Specifying and refining programs with Z. In: Proc. 2nd IEE/BCS Conference on Software Engineering, July 1988. Conference Publication, vol. 290, pp. 8–16. IEE/BCS (1988)
Wordsworth, J.B.: The CICS application programming interface definition. In: Nicholls [504], pp. 285–294
Wordsworth, J.B.: Software Development with Z: A Practical Approach to Formal Methods in Software Engineering. Addison-Wesley Publishing Company, Reading (1993) (This book provides a guide to developing software from specification to code, and is based in part on work done at IBM’s UK Laboratory that won the UK Queen’s Award for Technological Achievement in 1992. Contents: Introduction; A simple Z specification; Sets and predicates; Relations and functions; Schemas and specifications; Data design; Algorithm design; Specification of an oil terminal control system)
Jia, X.: ZTC: A Type Checker for Z – User’s Guide. Institute for Software Engineering, Department of Computer Science and Information Systems, DePaul University, Chicago, IL 60604, USA (1994) (ZTC is a type checker for the Z specification language. ZTC accepts two forms of input: LaTeX [408] with the oz.sty / zed.sty [398,601] style options and ZSL, an ASCII version of Z. ZTC can also perform translations between the two input forms. This document is intended to serve as both a user’s guide and a reference manual for ZTC)
Young, W.D.: Comparing specifications paradigms: Gypsy and Z. In: Proc. 12th National Computer Security Conference, Baltimore, Maryland, USA, October 10-13 (1989)
Zave, P., Jackson, M.: Techniques for partial specification and specification of switching systems. In: Prehn and Toetenel [530], pp. 511–525 (Also published as [702])
Zave, P., Jackson, M.: Techniques for partial specification and specification of switching systems. In: Nicholls [506], pp. 205–219
Zave, P., Jackson, M.: Conjunction as composition. ACM Transactions on Software Engineering and Methodology (TOSEM) 2(4), 379–411 (1993) (Partial specifications written in many different specification languages can be composed if they are all given semantics in the same domain, or alternatively, all translated into a common style of predicate logic. A Z specification is used as an example)
Zave, P., Jackson, M.: Where do operations come from? A multiparadigm technique. IEEE Transactions on Software Engineering 22(7), 508–528 (1996) (Z is supplemented, primarily with automata and grammars, to provide a rigorous and systematic mapping from input stimuli to convenient operations and arguments for the Z specification)
Zhang, Y., Hitchcock, P.: EMS: Case study in methodology for designing knowledge-based systems and information systems. Information and Software Technology 33(7), 518–526 (1991)
Z archive, http://www.comlab.ox.ac.uk/archive/z.html (1994) (onwards). On-line information on the Z notation is available for use by anyone with World Wide Web (WWW) and anonymous FTP access. In particular, this Z bibliography [1] is available. The preferred method of access to the Z archive is under the ‘URL’ (Uniform Resource Locator) given above. Some of the archive (mainly older files) is accessible via anonymous FTP under the ftp://ftp.comlab.ox.ac.uk/pub/Zforum/directory
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bowen, J.P. (1998). Select Z Bibliography. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds) ZUM ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive