@STRING{oucl = "Oxford University Computing Laboratory" } @STRING{oxford = "Wolfson Building, Parks Road, Oxford, UK" } @STRING{uk = "UK" } @STRING{lncs = "Lecture Notes in Computer Science" } @Misc{ z:00bib, key = {00bibliography}, title = {{Z} Bibliography}, howpublished = {URL: \verb"http://www.comlab.ox.ac.uk/archive/z/bib.html"}, year = {1990 onwards}, url = {http://www.comlab.ox.ac.uk/archive/z/bib.html}, annote = {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 \verb"J.P.Bowen@reading.ac.uk".}, comment = {Master Z Bibliography in BibTeX database format. Maintained by Jonathan Bowen. The University of Reading, Department of Computer Science, Whiteknights, PO Box 225, Reading, Berks RG6 6AY, England. Tel: +44-1734-316544. Fax: +44-1734-751994. Email: J.P.Bowen@reading.ac.uk Please send new entries to Jonathan Bowen. Copyright © 1990-1998 Jonathan Bowen. All rights reserved. Created 30 October 1990 from a UNIX "refer" format database. Acknowledgement: Ruaridh Macdonald, RSRE, Malvern, started and helped maintain the original database. Joan Arnold, ESPRIT ProCoS-WG Working Group secretary at the Oxford University Computing Laboratory, has also helped in maintaining the bibliography. Last major update, 3 August 1998. Last minor update, 17 October 1998. Entries not included in the Master Z Bibliography may be in an alternative Z Bibliography file. This includes older unpublished documents such as technical reports, MSc theses, draft papers, etc., particularly if they have subsequently been published elsewhere. Non-standard fields: abstract - abstract of paper, etc.; annote - extra annotation to appear after entry; comment - comment not to be printed; contact - contact name; email - electronic mail address for contact; ISBN - International Standard Book Number; ISSN - International Standard Series Number; length - number of pages for book, etc.; location - location (and date) of a workshop, conference, etc.; other - other information not to be printed; price - cost in pounds and/or dollars (may be out-of-date!); telephone - telephone number for contact; URL - Uniform Resource Locator for on-line access.} } @InProceedings{ z:abow90, author = {G. D. Abowd}, title = {Agents: Communicating Interactive Processes}, editor = {D. Diaper and D. Gilmore and G. Cockton and B. Shackel}, booktitle = {Human-Computer Interaction: {INTERACT'90}}, publisher = {Elsevier Science Publishers (North-Holland)}, location = {Cambridge, UK, 27--31 August 1990}, isbn = {0-444-8817-9}, year = 1990, pages = {143-148}, other = {Proc.\ IFIP TC13 3rd International Conference on Human-Computer Interaction.} } @PhDThesis{ z:abow91, author = {G. D. Abowd}, title = {Formal Aspects of Human-Computer Interaction}, school = oucl, address = oxford, type = {{DPhil} thesis}, year = 1991 } @Article{ z:abow93, author = {G. D. Abowd and R. Allen and D. Garlan}, title = {Using Style to Understand Descriptions of Software Architectures}, booktitle = {Proc.\ SIGSOFT'93 Symposium on the Foundations of Software Engineering}, journal = {ACM Software Engineering Notes}, volume = 18, number = 5, pages = {9-20}, url = {ftp://ftp.sei.cmu.edu/pub/gda/papers/sigsoft93.ps.Z}, month = dec, year = 1993 } @Article{ z:abow95, author = {G. D. Abowd and R. Allen and D. Garlan}, title = {Formalizing Style to Understand Descriptions of Software Architecture}, journal = {ACM Transactions on Software Engineering and Methodology (TOSEM)}, volume = 4, number = 4, pages = {319-364}, month = oct, year = 1995, annote = {The formal model is described using the Z specification language.} } @InProceedings{ z:abri74, author = {J.-R. Abrial}, title = {Data Semantics}, editor = {J. W. Klimbie and K. L. Koffeman}, booktitle = {IFIP TC2 Working Conference on Data Base Management}, pages = {1-59}, publisher = {Elsevier Science Publishers (North-Holland)}, month = apr, year = 1974, annote = {A seminal paper for the formal Z notation, as noted in \cite{z:habr95}.} } @InCollection{ z:abri80, author = {J.-R. Abrial and S. A. Schuman and B. Meyer}, editor = {R. M. McKeag and A. M. Macnaghten}, title = {Specification Language}, booktitle = {On the Construction of Programs: An Advanced Course}, publisher = {Cambridge University Press}, pages = {343-410}, year = 1980 } @InProceedings{ z:abri81, author = {J.-R. Abrial and I. H. S{\o}rensen}, title = {{KWIC}-index generation}, editor = {J. Staunstrup}, booktitle = {Program Specification: Proceedings of a Workshop}, publisher = {Springer-Verlag}, series = lncs, volume = 134, pages = {88-95}, year = 1981, location = {{\AA}rhus, Denmark, August 1981} } @InProceedings{ z:abri88, author = {J.-R. Abrial}, title = {The {B} Tool}, pages = {86-87}, annote = {}, crossref = {z:bloo88} } @InProceedings{ z:abri91, author = {J.-R. Abrial}, title = {The {B} Method for Large Software, Specification, Design and Coding (Abstract)}, annote = {}, note = {}, crossref = {z:preh91b}, pages = {398-405} } @Book{ z:abri96, author = {J.-R. Abrial}, title = {The {B}-Book: Assigning Programs to Meanings}, publisher = {Cambridge University Press}, year = 1996, price = {\pounds 40.00}, isbn = {0-521-49619-5}, length = 850, annote = {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. \par 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; \par Appendices: Summary of the most current notations; Syntax; Definitions; Visibility rules; Rules and axioms; Proof obligations.} } @Book{ z:abri96b, editor = {J.-R. Abrial and E. B\"orger and H. Langmaack}, title = {Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler}, booktitle = {Formal Methods for Industrial Applications}, publisher = {Springer-Verlag}, series = lncs, volume = 1165, year = 1996, isbn = {3-540-61929-1}, length = 509, url = {http://www.informatik.uni-kiel.de/~procos/dag9523/dag9523.html} , annote = {A comparative collection of formal methods case studies. See \cite{z:buss96,z:sche96}.} } @InProceedings{ z:acha97, author = {K. Achatz and W. Schulte}, title = {A Formal {OO} Method inspired by {Fusion} and {Object-Z}}, annote = {}, pages = {92-111}, crossref = {z:z97} } @Article{ z:ains94, author = {M. Ainsworth and A. H. Cruickshank and P. J. L. Wallis and L. J. Groves}, title = {Viewpoint specification and {Z}}, journal = {Information and Software Technology}, volume = 36, number = 1, pages = {43-51}, year = 1994 } @InProceedings{ z:alen91, author = {A. J. Alencar and J. A. Goguen}, title = {{OOZE}: An Object-Oriented {Z} Environment}, editor = {P. America}, booktitle = {Proc.\ {ECOOP'91} {European} Conference on Object-Oriented Programming}, publisher = {Springer-Verlag}, series = lncs, volume = 512, location = {Geneva, Switzerland, July 1991}, isbn = {3-540-54262-0}, pages = {180-199}, year = 1991 } @Article{ z:ardi96, author = {M. A. Ardis and J. A. Chaves and L. J. Jagadeesan and P. Mataga and C. Puchol and M. G. Staskauskas and J. {von Olnhausen}}, title = {A Framework for Evaluating Specification Methods for Reactive Systems Experience Report}, journal = {IEEE Transactions on Software Engineering}, year = 1996, volume = 22, number = 6, month = jun, pages = {378-389}, abstract = {Numerous formal specification methods for reactive systems have been proposed in the literature. Because the significant differences between the methods are hard to determine, choosing the best method for a particular application can be difficult. We have applied several different methods, including Modechart, VFSM, ESTEREL, Basic LOTOS, Z, SDL, and C, to an application problem encountered in the design of software for AT&T's 5ESS. telephone switching system. We have developed a set of criteria for evaluating and comparing the different specification methods. We argue that the evaluation of a method must take into account not only academic concerns, but also the maturity of the method, its compatibility with the existing software development process and system execution environment, and its suitability for the chosen application domain.}, annote = {Several different methods, including Modechart, VFSM, {\sc 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.}, keywords = {Formal methods, specification languages, industrial applications, technology assessment, ESTEREL, LOTOS, Modechart, SDL, VFSM, Z} } @InProceedings{ z:arno87, author = {D. B. Arnold and D. A. Duce and G. J. Reynolds}, title = {An Approach to the Formal Specification of Configurable Models of Graphics Systems}, editor = {G. Mar\'echal}, booktitle = {Proc.\ {EUROGRAPHICS'87}, {European} Computer Graphics Conference and Exhibition}, publisher = {Elsevier Science Publishers (North-Holland)}, location = {Amsterdam, The Netherlands, 24--28 August 1987}, year = 1987, pages = {439-463}, isbn = {0-444-70291-1}, annote = {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.} } @Article{ z:arno88, author = {D. B. Arnold and G. J. Reynolds}, title = {Configuring graphics systems components}, journal = {IEE/BCS Software Engineering Journal}, pages = {248-256}, volume = 3, number = 6, month = nov, year = 1988, abstract = {Computer graphics systems have traditionally been described in terms of a conceptual model of the so-called `graphics processing pipeline'. This model explains the relationship between graphics information defined by an application and the realization of that information on a display in terms of a sequence of transformation stages. Although adequate for giving an outline of a single graphics system, the model lacks flexibility and detail when placed in the sphere of may difference graphics systems designs, as in the `family of graphics systems' under ISO standardization at the current time. An alternative approach is needed which provides a sufficient level of detail and flexibility to describe both existing graphics systems and possible extensions to these which at the same time permits the comparison of graphics systems designs in a well defined framework. The computer graphics reference model presented in this paper meets many of these objectives.} } @InProceedings{ z:arth91, author = {R. D. Arthan}, title = {Formal Specification of a Proof Tool}, annote = {}, note = {}, crossref = {z:preh91}, pages = {356-370} } @InProceedings{ z:arth92, author = {R. D. Arthan}, title = {On Free Type Definitions in {Z}}, annote = {}, crossref = {z:z92}, pages = {40-58} } @InProceedings{ z:arth98, title = {Recursive Definitions in {Z}}, author = {R. D. Arthan}, annote = {}, pages = {154-171}, crossref = {z:z98} } @Article{ z:asho92, author = {K. Ashoo}, title = {The {Genesis} {Z} Tool -- An Overview}, journal = {BCS-FACS FACTS}, volume = {Series II, 3}, number = 1, pages = {11-13}, month = may, year = 1992 } @Article{ z:atki95, title = {Transformational vs Reactive Refinement in Real-Time Systems}, author = {Atkinson, S. and Scholefield, D.}, journal = {Information Processing Letters}, year = 1995, volume = 55, number = 4, pages = {201-210}, issn = {0020-0190}, abstract = {Real-time software development is investigated in an extended form of the Z language, and compared with development in the Temporal Agent Model (TAM): a theory specifically designed for real-time systems. Both of these theories use refinement as the main development method, and by defining a translation between the extended Z language, and the TAM language, we are able to compare the two refinement relations in terms of an example real-time system refinement.}, keywords = {formal development, program specification, real-time systems, refinement, specification languages, Temporal Agent Model, Z} } @InProceedings{ z:aujl93, author = {S. Aujla and A. Bryant and L. Semmens}, title = {A Rigorous Review Technique: Using Formal Notations within Conventional Development Methods}, pages = {247-255}, annote = {}, crossref = {z:kats93} } @Article{ z:aust92, author = {P. B. Austin and K. A. Murray and A. J. Wellings}, title = {File System Caching in Large Point-to-point Networks}, journal = {IEE/BCS Software Engineering Journal}, pages = {65-80}, volume = 7, number = 1, month = jan, year = 1992 } @TechReport{ z:aust93, author = {S. Austin and G. I. Parkin}, title = {Formal Methods: A Survey}, institution = {National Physical Laboratory}, address = {Queens Road, Teddington, Middlesex, TW11 0LW, UK}, month = mar, year = 1993 } @InProceedings{ z:bail87, author = {M. Bailey}, title = {Formal Specification using {Z}}, booktitle = {Proc.\ Software Engineering anniversary meeting ({SEAS})}, other = {SEA}, year = 1987, pages = 99 } @InProceedings{ z:bail91, author = {C. Bailes and R. Duke}, title = {The Ecology of Class Refinement}, pages = {185-196}, annote = {}, crossref = {z:morr91} } @InProceedings{ z:bain91, author = {J. Bainbridge and R. W. Whitty and J. B. Wordsworth}, title = {Obtaining Structural Metrics of {Z} Specifications for Systems Development}, annote = {}, crossref = {z:z91}, pages = {269-281} } @InCollection{ z:bana91, author = {J.-P. Ban\^atre}, title = {About Programming Environments}, editor = {J.-P. Ban\^atre and S. B. Jones and D. {de M\'etayer}}, booktitle = {Prospects for Functional Programming in Software Engineering}, other = {Research Reports, Volume 1}, publisher = {Springer-Verlag}, isbn = {3-540-53852-6}, chapter = 1, pages = {1-22}, year = 1991, comment = {ESPRIT Project 302} } @InProceedings{ z:banc95, author = {P. Bancroft and I. J. Hayes}, title = {A Formal Semantics for a Language with Type Extension}, pages = {299-314}, annote = {}, crossref = {z:z95} } @InProceedings{ z:bard92, author = {R. Barden and S. Stepney and D. Cooper}, title = {The Use of {Z}}, annote = {}, crossref = {z:z92}, pages = {99-124} } @InProceedings{ z:bard93, author = {R. Barden and S. Stepney}, title = {Support for Using {Z}}, annote = {}, crossref = {z:z93}, pages = {255-280} } @Book{ z:bard94, author = {R. Barden and S. Stepney and D. Cooper}, title = {{Z} in Practice}, publisher = {Prentice Hall}, series = {BCS Practitioner Series}, price = {\pounds 22.95}, isbn = {0131249347}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0131249347}, year = 1994 } @Article{ z:barr89, author = {G. Barrett}, title = {Formal Methods Applied to a Floating-Point Number System}, journal = {IEEE Transactions on Software Engineering}, volume = 15, number = 5, pages = {611-621}, month = may, year = 1989, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-58-IEEETSE.ps.gz} , annote = {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.} } @Article{ z:barr92b, author = {L. M. Barroca and J. A. McDermid}, title = {Formal Methods: Use and Relevance for the Development of Safety-Critical Systems}, journal = {The Computer Journal}, volume = 35, number = 6, pages = {579-599}, month = dec, year = 1992 } @InProceedings{ z:barr95, author = {L. M. Barroca and J. S. Fitzgerald and L. Spencer}, title = {The Architectural Specification of an Avionic Subsystem}, crossref = {z:wift95}, pages = {17-29} } @InProceedings{ z:bate96, author = {Bates, B. W. and Bruel, J.-M. and France, R. B. and Larrondo-Petrie, M. M.}, title = {Guidelines for Formalizing {Fusion} Object-Oriented Analysis Models}, editor = {Constantopoulos, P. and Mylopoulos, J. and Vassiliou, Y.}, booktitle = {Advanced Information Systems Engineering}, location = {Heraklion, Crete, Greece, 20--24 May 1996}, series = lncs, publisher = {Springer-Verlag}, year = 1996, volume = 1080, pages = {222-233}, issn = {0302-9743}, abstract = {The growing interest in object-oriented analysis and design methods (OOMs) in the software development industry can be attributed to the support they give to some of the more significant software engineering principles, for example, separation of concerns and generality. On the other hand, most OOMs, like their structured analysis and design predecessors, produce models that are not amenable to rigorous semantic analyses. This problem can be attributed to the lack of firm semantic bases for the modeling notations and concepts. In this paper we show how a particular OOM, the Fusion analysis method, can be made more formal while preserving its essential qualities. Our approach involves integrating the Z formal specification style with the Fusion method. The result is an OOM that produces semantically analyzable Fusion models of behavior at the requirements level.}, keywords = {systems, formal specification techniques, object-oriented analysis, transformations} } @InProceedings{ z:baum94, author = {P. Baumann}, title = {{Z} and Natural Semantics}, pages = {168-184}, annote = {}, crossref = {z:z94} } @InProceedings{ z:baum95, author = {P. Baumann and K. Lermer}, title = {A Framework for the Specification of Reactive and Concurrent Systems in {Z}}, editor = {P. S. Thiagarajan}, booktitle = {Foundations of Software Technology and Theoretical Computer Science}, other = {Proc.\ 15th Conference}, publisher = {Springer-Verlag}, series = lncs, volume = 1026, pages = {62-79}, year = 1995 } @InProceedings{ z:baum96, author = {P. Baumann and K. Lermer}, title = {Specifying Parallel and Distributed Real-Time Systems in {Z}}, booktitle = {Proc.\ 4th International Workshop on Parallel and Distributed Real-Time Systems, Hawaii}, location = {Hawaii, USA, April 1996}, pages = {216-222}, month = apr, year = 1996 } @InProceedings{ z:benj90, author = {M. Benjamin}, title = {A Message Passing System: An Example of combining {CSP} and {Z}}, annote = {}, crossref = {z:z90}, pages = {221-228}, year = 1990 } @InProceedings{ z:benv91, author = {M. Benveniste}, title = {Writing Operational Semantics in {Z}: A Structural Approach}, annote = {}, note = {}, crossref = {z:preh91}, pages = {164-188} } @InProceedings{ z:bera88, author = {S. Bera}, title = {Structuring for the {VDM} Specification Language}, pages = {2-25}, annote = {}, crossref = {z:bloo88} } @InProceedings{ z:bern95, author = {P. Bernard and G. Laffitte}, title = {The {French} Population Census for 1990}, pages = {334-352}, annote = {}, crossref = {z:z95} } @Book{ z:bert98, editor = {D. Bert}, title = {{B'98}: Recent Developments in the Use of the {B Method}}, publisher = {Springer-Verlag}, series = lncs, volume = 1393, year = 1998, annote = {Proceedings of the 2nd B Conference, Montpellier, France, 22--24 April 1998.} } @Article{ z:bica95, author = {J. Bicarregui and B. Ritchie}, title = {Invariants, Frames and Postconditions: A Comparison of the {VDM} and {B} Notations}, journal = {IEEE Transactions on Software Engineering}, volume = 21, number = 2, pages = {79-89}, month = feb, year = 1995 } @InProceedings{ z:bica95b, author = {J. Bicarregui and J. Dick and E. Woods}, title = {Supporting the Length of Formal Development: From Diagrams to {VDM} to {B} to {C}}, pages = {63-75}, annote = {}, crossref = {z:habr95} } @InProceedings{ z:bica96, author = {J. Bicarregui and J. Dick and E. Woods}, title = {Quantitative Analysis of Formal Methods}, pages = {60-73}, annote = {}, crossref = {z:gaud96} } @InBook{ z:bish90, editor = {P. G. Bishop}, title = {Fault Avoidance}, booktitle = {Dependability of Critical Computer Systems 3: Techniques Directory}, chapter = 3, pages = {56-140}, publisher = {Elsevier Science Publishers}, series = {Applied Science}, isbn = {1-85166-544-7}, year = 1990, annote = {Section 3.88 (pages 94--96) provides an overview of Z. Other sections describe related techniques.} } @Proceedings{ z:bjor90, editor = {D. Bj{\o}rner and C. A. R. Hoare and H. Langmaack}, title = {{VDM} and {Z} -- Formal Methods in Software Development}, booktitle = {{VDM} and {Z} -- Formal Methods in Software Development}, publisher = {Springer-Verlag}, other = {Proc.\ 3rd {VDM-Europe} Symposium}, organization = {VDM-Europe}, location = {Kiel, Germany, 17--21 April 1990}, series = lncs, volume = 428, year = 1990, isbn = {3-540-52513-0, 0-387-52513-0}, annote = {The 3rd VDM-Europe Symposium was held at Kiel, Germany, 17--21 April 1990. A significant number of papers concerned with Z were presented \cite{z:chal90,z:duke90,z:garl90,z:giov90,z:gotz90,% z:hall90,z:king90b,z:samp90,z:spiv90,z:diep90,z:wood90}.} } @Article{ z:bloe95, title = {{Cogito}: A Methodology and System for Formal Software-Development}, author = {Bloesch, A. and Kazmierczak, E. and Kearney, P. and Traynor, O.}, journal = {International Journal of Software Engineering and Knowledge Engineering}, year = 1995, volume = 5, number = 4, pages = {599-617}, issn = {0218-1940}, abstract = {Cogito 1 is the first iteration of a Z-based integrated methodology and support system for formal software development. This paper gives an overview of the Cogito methodology and associated tools. Particular emphasis is placed on the way in which Cogito integrates the various phases of the formal development process and provides comprehensive tools support for all phases of development addressed by the methodology.}, keywords = {formal methods, formal specification, refinement} } @Proceedings{ z:bloo88, editor = {R. Bloomfield and L. Marshall and R. Jones}, title = {{VDM} -- The Way Ahead}, booktitle = {{VDM} -- The Way Ahead}, other = {Proc.\ 2nd {VDM-Europe} Symposium}, publisher = {Springer-Verlag}, organization = {VDM-Europe}, location = {Dublin, Ireland, 11--16 September 1988}, series = lncs, volume = 328, year = 1988, isbn = {0-387-50214-9}, annote = {The 2nd VDM-Europe Symposium was held at Dublin, Ireland, 11--16 September 1988. See \cite{z:abri88,z:bera88}.} } @Article{ z:bloo97, title = {Using a {Protean} Language to Enhance Expressiveness in Specification}, author = {Bloom, B. and Cheng, A. and Dsouza, A.}, journal = {IEEE Transactions on Software Engineering}, year = 1997, volume = 23, number = 4, pages = {224-234}, issn = {0098-5589}, abstract = {A Protean specification language [6] based on Structured Operational Semantics (SOS) allows the user to invent appropriate operations to improve abstraction and readability. This is in contrast to traditional specification languages, where the set of operations is fixed. An efficient algorithm, described in [10], uses binary decision diagrams (BDDs) to verify properties of finite specifications written in a Protean language and provides the basis for a model checker we have developed. This paper provides a synthesis of our work on Protean languages and relates the work to other specification techniques. We show how abstraction and refinement in the Protean framework can improve the effectiveness of model checking. We rewrite and verify properties of an existing Z specification by defining suitable operations. We also show how a Protean language can be used to model restricted I/O automata, action refinement, and 1-safe and k-bounded Petri nets.}, keywords = {formal methods, specification, verification, structured operational semantics, process algebra, model checking} } @InProceedings{ z:boit95, author = {E. A. Boiten and J. Derrick and H. Bowman and M. Steen}, title = {Unification and Multiple Views of Data in {Z}}, editor = {J. C. {van Vliet}}, booktitle = {Proc.\ Computing Science in the Netherlands}, pages = {73-85}, month = nov, year = 1995, isbn = {90-6196-460-1}, url = {http://alethea.ukc.ac.uk/Dept/Computing/Research/NDS/staff/eab2/csn95.html} } @InProceedings{ z:boit96, author = {E. A. Boiten and J. Derrick and H. Bowman and M. Steen}, title = {Consistency and Refinement for Partial Specifications in {Z}}, pages = {287-306}, annote = {}, crossref = {z:gaud96}, url = {http://alethea.ukc.ac.uk/Dept/Computing/Research/NDS/staff/eab2/fme.html} } @InProceedings{ z:boit96b, author = {E. A. Boiten and H. Bowman and J. Derrick and M. Steen}, title = {Issues in Multiparadigm Viewpoint Specification}, editor = {A. Finkelstein and G. Spanoudakis}, booktitle = {SIGSOFT '96 International Workshop on Multiple Perspectives in Software Development (Viewpoints '96)}, isbn = {0-89791-867-3}, url = {http://alethea.ukc.ac.uk/Dept/Computing/Research/NDS/consistency/vpts.html} , publisher = {ACM}, pages = {162-166}, year = 1996 } @InProceedings{ z:boit97, author = {E. A. Boiten and J. Derrick and H. Bowman and M. Steen}, title = {Coupling Schemas: Data Refinement and View(point) Composition}, editor = {D. J. Duke and A. S. Evans}, booktitle = {Northern Formal Methods Workshop}, series = {Electronic Workshops In Computing}, publisher = {Springer-Verlag}, year = 1997, url = {http://ewic.springer.co.uk/workshops/NFM97/} } @InProceedings{ z:boit97b, author = {E. A. Boiten and H. Bowman and J. Derrick and M. Steen}, title = {Viewpoint Consistency in {Z} and {LOTOS}: A Case Study}, pages = {644-664}, crossref = {z:fitz97} } @InProceedings{ z:borg97, title = {A Practical Method for Rigorously Controllable Hardware Design}, author = {E. B\"orger and S. Mazzanti}, comment = {Invited speaker}, annote = {}, pages = {151-187}, crossref = {z:z97} } @Proceedings{ z:bosc97, editor = {J. Bosch and S. Mitchell}, title = {Object-Oriented Technology: {ECOOP'97} Workshop Reader}, booktitle = {Object-Oriented Technology: {ECOOP'97} Workshop Reader}, publisher = {Springer-Verlag}, series = lncs, volume = 1357, location = {Jyv\"askyl\"a, Finland, June 1997}, year = 1997, annote = {See Z-related papers \cite{z:cohe97,z:elbe97,z:fran97}.} } @InProceedings{ z:bosw93, author = {A. Boswell}, title = {Specification and Validation of a Security Policy Model}, other = {Revised version in \cite{z:bosw95}.}, crossref = {z:wood93}, pages = {42-51} } @Article{ z:bosw95, author = {A. Boswell}, title = {Specification and Validation of a Security Policy Model}, journal = {IEEE Transactions on Software Engineering}, volume = 21, number = 2, pages = {99-106}, month = feb, year = 1995, annote = {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.} } @Book{ z:bott95, author = {L. Bottaci and J. Jones}, title = {Formal Specification Using {Z}: A Modelling Approach}, publisher = {International Thomson Publishing}, address = {London}, isbn = {1-850-32109-4}, price = {\pounds19.95, paperback}, length = 320, other = {University of Hull, UK}, url = {http://itp.thomson.com/catalogs/srch_isbn?1850321094}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?1850321094}, year = 1995 } @Article{ z:bowe87, author = {J. P. Bowen}, editor = {H. Schumny and J. M{\o}lgaard}, title = {Formal Specification and Documentation of Microprocessor Instruction Sets}, booktitle = {Proc.\ {EUROMICRO'87}, Microcomputers: Usage, Methods and Structures}, journal = {Microprocessing and Microprogramming}, publisher = {Elsevier Science Publishers (North-Holland)}, location = {Portsmouth, UK, 14--17 September 1987}, volume = 21, number = {1--5}, pages = {223-230}, length = 690, month = aug, year = 1987 } @TechReport{ z:bowe87b, author = {J. P. Bowen and R. B. Gimson and S. Topp-J{\o}rgensen}, title = {The Specification of Network Services}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-61}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-61.html} , length = 106, month = aug, year = 1987, isbn = {0-902928-43-0} } @Proceedings{ z:bowe87c, author = {J. P. Bowen and others}, editor = {J. P. Bowen}, title = {Proc.\ {Z} Users Meeting, 1 Wellington Square, Oxford}, publisher = oucl, address = oxford, length = 23, month = dec, year = 1987, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/proc87.ps.Z}, annote = {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.} } @TechReport{ z:bowe87d, author = {J. P. Bowen}, title = {The Formal Specification of a Microprocessor Instruction Set}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-60}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-60.html} , length = 72, month = jan, year = 1987, isbn = {0-902928-42-2}, annote = {The Z notation is used to define the Motorola M6800 8-bit microprocessor instruction set.} } @Proceedings{ z:bowe88, author = {J. P. Bowen and others}, editor = {J. P. Bowen}, title = {Proc.\ Third Annual {Z} Users Meeting}, publisher = oucl, address = oxford, length = 21, month = dec, year = 1988, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/proc88.ps.Z}, annote = {Proceedings of the 3rd Z User Meeting, Department of External Studies, Rewley House, Oxford, UK, Friday 16 December 1988. Issued with {\em A Miscellany of Handy Techniques} by R.\ Macdonald, {\em Practical Experience of Formal Specification: A programming interface for communications} by J.~B.\ Wordsworth, and a number of posters.} } @TechReport{ z:bowe88b, author = {J. P. Bowen and R. B. Gimson and S. Topp-J{\o}rgensen}, title = {Specifying System Implementations in {Z}}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-63}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-63.html} , length = 88, month = feb, year = 1988, isbn = {0-902928-45-7} } @InProceedings{ z:bowe88c, author = {J. P. Bowen}, title = {Formal Specification in {Z} as a Design and Documentation Tool}, booktitle = {Proc.\ 2nd {IEE}/{BCS} Conference on Software Engineering}, organization = {IEE/BCS}, location = {Liverpool, UK, July 1988}, series = {Conference Publication}, number = 290, pages = {164-168}, month = jul, year = 1988 } @Article{ z:bowe89b, author = {J. P. Bowen}, title = {{POS}: Formal Specification of a {UNIX} Tool}, journal = {IEE/BCS Software Engineering Journal}, volume = 4, number = 1, pages = {67-72}, month = jan, year = 1989 } @TechReport{ z:bowe89c, author = {J. P. Bowen}, title = {Formal Specification of Window Systems}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-74}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-74.html} , length = 88, month = jun, year = 1989, isbn = {0-902928-56-2}, annote = {Three window systems, X from MIT, WM from Carnegie-Mellon University and the Blit from AT\&T Bell Laboratories are covered.} } @Article{ z:bowe90d, author = {J. P. Bowen}, editor = {H. S. M. Zedan}, title = {Formal Specification of the {ProCoS/safemos} Instruction Set}, journal = {Microprocessors and Microsystems}, month = dec, year = 1990, volume = 14, number = 10, pages = {631-643}, abstract = {This article gives a preview of the work of two European government-sponsored projects investigating design methods for `provable' computer systems. As a common interface both projects use subsets of Occam and the Transputer instruction set. A number of Transputer instructions are presented using Z.}, annote = {This article is part of a special feature on {\em Formal aspects of microprocessor design}, edited by H.~S.~M.\ Zedan. See also \cite{z:shep90}.} } @Article{ z:bowe92, author = {J. P. Bowen}, title = {{X}: Why {Z}?}, journal = {Computer Graphics Forum}, publisher = {Elsevier Science Publishers (North-Holland)}, volume = 11, number = 4, pages = {221-234}, month = oct, year = 1992, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/xyz.ps.Z} , annote = {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.} } @Article{ z:bowe93c, author = {J. P. Bowen}, title = {Report on {Z User Meeting}, {London} 1992}, journal = {BCS-FACS FACTS}, volume = {Series III, 1}, number = 3, pages = {7-8}, month = {Summer}, year = 1993, annote = {Other versions of this report appeared as follows: \begin{itemize} \item Z User Meetings, {\em Safety Systems: The Safety-Critical Systems Club Newsletter}, 3(1):13, September 1993. \item Z User Group activities, {\em JFIT News}, 46:5, September 1993. \item Report on Z User Meeting, {\em Information and Software Technology}, 35(10):613, October 1993. \item Z User Meeting Activities, {\em High Integrity Systems}, 1(1):93--94, 1994. \end{itemize}} } @Article{ z:bowe93d, author = {J. P. Bowen and P. T. Breuer and K. C. Lano}, title = {A Compendium of Formal Techniques for Software Maintenance}, journal = {IEE/BCS Software Engineering Journal}, volume = 8, number = 5, pages = {253-262}, month = sep, year = 1993, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/sum-sej.ps.Z} } @Article{ z:bowe93e, author = {J. P. Bowen and P. T. Breuer and K. C. Lano}, title = {Formal Specifications in Software Maintenance: From code to {Z$^{++}$} and back again}, journal = {Information and Software Technology}, volume = 35, number = {11/12}, pages = {679-690}, month = {November/December}, year = 1993, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/sum-ist.ps.Z} } @Article{ z:bowe93f, author = {J. P. Bowen and V. Stavridou}, title = {Safety-Critical Systems, Formal Methods and Standards}, journal = {IEE/BCS Software Engineering Journal}, volume = 8, number = 4, pages = {189-209}, month = jul, year = 1993, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/sfs-sej.ps.Z} , annote = {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.} } @InProceedings{ z:bowe93g, author = {J. P. Bowen and V. Stavridou}, title = {The Industrial Take-up of Formal Methods in Safety-Critical and Other Areas: A Perspective}, annote = {}, crossref = {z:wood93}, pages = {183-195}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/fme93.ps.Z} } @InProceedings{ z:bowe93h, author = {J. P. Bowen}, title = {Formal Methods in Safety-Critical Standards}, pages = {168-177}, annote = {}, crossref = {z:kats93}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/sess93.ps.Z} } @InProceedings{ z:bowe94b, author = {J. P. Bowen and M. J. C. Gordon}, title = {{Z} and {HOL}}, pages = {141-167}, annote = {}, crossref = {z:z94}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/zhol.ps.Z} , other = {Invited paper} } @InProceedings{ z:bowe94e, author = {J. P. Bowen and M. G. Hinchey}, title = {Seven More Myths of Formal Methods: Dispelling Industrial Prejudices}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/fme94.ps.Z} , annote = {}, crossref = {z:naft94}, pages = {105-117} } @Article{ z:bowe94g, author = {J. P. Bowen and M. G. Hinchey}, title = {Formal Methods and Safety-Critical Standards}, journal = {IEEE Computer}, volume = 27, number = 8, pages = {68-71}, month = aug, year = 1994 } @Article{ z:bowe95, title = {A Shallow Embedding of {Z} in {HOL}}, author = {Bowen, J. P. and Gordon, M. J. C.}, journal = {Information and Software Technology}, year = 1995, volume = 37, number = {5--6}, pages = {269-276}, issn = {0950-5849}, abstract = {A simple `shallow' semantic embedding of the Z notation into the higher order logic, as supported by the HOL theorem proving system, is presented. Z is typically used for human-readable formal specification whereas HOL is used for machine-checked verification. The paper is intended to show how a tool such as HOL can be used to provide mechanical support for Z, including mechanization of proofs. No specialized knowledge of Z or HOL is assumed. An explanation of shallow and deep embedding as well as a survey of other related research are also included.}, keywords = {formal methods, Higher Order Logic, mechanical verification, theorem proving, Z notation} } @Article{ z:bowe95b, author = {J. P. Bowen and M. G. Hinchey}, title = {Ten Commandments of Formal Methods}, journal = {IEEE Computer}, volume = 28, number = 4, pages = {56-63}, month = apr, year = 1995, url = {http://www.cl.cam.ac.uk/users/mgh1001/10comms.html}, annote = {Previously issued as: Technical Report 350, University of Cambridge, Computer Laboratory, September 1994.} } @Article{ z:bowe95c, author = {J. P. Bowen and M. G. Hinchey}, title = {Seven More Myths of Formal Methods}, journal = {IEEE Software}, volume = 12, number = 4, pages = {34-41}, month = jul, year = 1995, url = {http://www.cl.cam.ac.uk/users/mgh1001/TECHREPORTS/7myths.ps.Z} , annote = {This article deals with further myths in addition to those presented in \cite{z:hall90b}. Previous versions issued as: \begin{itemize} \item Technical Report PRG-TR-7-94, Oxford University Computing Laboratory, June 1994. \item Technical Report 357, University of Cambridge, Computer Laboratory, January 1995. \end{itemize}} } @Article{ z:bowe95e, author = {J. P. Bowen and M. J. C. Gordon}, title = {A Shallow Embedding of {Z} in {HOL}}, journal = {Information and Software Technology}, volume = 37, number = {5--6}, pages = {269-276}, month = {May--June}, year = 1995, annote = {Revised version of \cite{z:bowe94b}.} } @Article{ z:bowe95f, author = {J. P. Bowen and S. Stepney and R. Barden}, title = {Annotated {Z} Bibliography}, journal = {Information and Software Technology}, volume = 37, number = {5--6}, pages = {317-332}, month = {May--June}, year = 1995, annote = {See also {\em Literature Guide}, Appendix C, pages 239--251 of \cite{z:bowe96}.} } @Article{ z:bowe95g, author = {J. P. Bowen}, title = {Glossary of {Z} Notation}, journal = {Information and Software Technology}, month = {May--June}, year = 1995, volume = 37, number = {5--6}, pages = {333-334}, issn = {0950-5849} } @Article{ z:bowe95h, author = {J. P. Bowen and M. G. Hinchey}, title = {Report on {Z User Meeting} {(ZUM'94)}}, journal = {Information and Software Technology}, volume = 37, number = {5--6}, pages = {335-336}, month = {May--June}, year = 1995 } @Article{ z:bowe95i, author = {J. P. Bowen and M. G. Hinchey}, editor = {J. P. Bowen and M. G. Hinchey}, title = {Editorial}, journal = {Information and Software Technology}, volume = 37, number = {5--6}, pages = {258-259}, month = {May--June}, year = 1995, url = {http://www.elsevier.nl/cas/estoc/contents/SAC/09505849/SZ955894.html} , annote = {A special issue on Z. See \cite{z:bowe95g,z:bowe95h,z:bowe95e,z:bowe95f,z:garl95b,z:lano95,% z:mand95,z:mata95b,z:vale95}.} } @InProceedings{ z:bowe95k, author = {J. P. Bowen and {He Jifeng} and R. W. S. Hale and J. M. J. Herbert}, title = {Towards Verified Systems: The {SAFEMOS} Project}, editor = {C. J. Mitchell and V. Stavridou}, booktitle = {The Mathematics of Dependable Systems}, publisher = {Oxford University Press}, series = {The Institute of Mathematics and its Applications Conference Series}, location = {Royal Holloway, University of London, UK, September 1993}, volume = 55, pages = {23-48}, year = 1995 } @Book{ z:bowe96, author = {J. P. Bowen}, title = {Formal Specification and Documentation Using {Z}: A Case Study Approach}, publisher = {International Thomson Computer Press}, comment = {London / Boston}, url = {http://www.comlab.ox.ac.uk/oucl/users/jonathan.bowen/zbook.html} , price = {\pounds 24.95}, length = 302, isbn = {1-85032-230-9}, year = 1996, annote = {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.} } @InCollection{ z:bowe97, author = {J. P. Bowen and M. G. Hinchey}, title = {Formal Models and the Specification Process}, editor = {A. B. {Tucker, Jr.}}, booktitle = {The Computer Science and Engineering Handbook}, note = {Section X, Software Engineering}, chapter = 107, pages = {2302-2322}, publisher = {CRC Press}, year = 1997, other = {Published in cooperation with the ACM.} } @InProceedings{ z:bowe97b, author = {J. P. Bowen}, title = {Select {Z} Bibliography}, pages = {391-424}, annote = {}, crossref = {z:z97}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/z97.ps.Z} } @InProceedings{ z:bowe97c, author = {J. P. Bowen}, title = {{Comp.specification.z} and {Z FORUM} Frequently Asked Questions}, pages = {425-433}, annote = {}, crossref = {z:z97}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/faq97.ps.Z} } @InProceedings{ z:bowe98, title = {{Z} on the {Web} using {Java}}, author = {J. P. Bowen and D. Chippington}, annote = {}, pages = {66-80}, crossref = {z:z98}, url = {http://www.fmse.cs.reading.ac.uk/z/java/} } @InProceedings{ z:bowe98b, author = {J. P. Bowen}, title = {Select {Z} Bibliography}, annote = {}, pages = {367-406}, crossref = {z:z98}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/z98.ps.Z} } @InProceedings{ z:bowe98c, author = {J. P. Bowen}, title = {{Comp.specification.z} and {Z FORUM} Frequently Asked Questions}, annote = {}, pages = {407-415}, crossref = {z:z98}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/faq98.ps.Z} } @Article{ z:bowm95, author = {H. Bowman and J. Derrick and P. Linington and M. Steen}, title = {{FDTs} for {ODP}}, journal = {Computer Standards \& Interfaces}, volume = 17, number = {5--6}, pages = {457-479}, month = sep, year = 1995, publisher = {Elsevier Science Publishers (North-Holland)}, url = {http://alethea.ukc.ac.uk/Dept/Computing/Research/NDS/consistency/fdtodp.html} } @InProceedings{ z:bowm95b, author = {H. Bowman and J. Derrick}, title = {Modelling Distributed Systems using {Z}}, editor = {K. M. George}, booktitle = {ACM Symposium on Applied Computing}, publisher = {ACM Press}, location = {Nashville, USA}, pages = {147-151}, month = feb, year = 1995, url = {http://alethea.ukc.ac.uk/Dept/Computing/Research/NDS/consistency/sac.html} } @InProceedings{ z:brad93, author = {A. Bradley}, title = {Requirements for {Defence Standard 00-55}}, annote = {}, crossref = {z:z93}, pages = {93-94} } @InProceedings{ z:breu91, author = {P. T. Breuer}, title = {{Z!} in Progress: Maintaining {Z} Specifications}, annote = {}, crossref = {z:z91}, pages = {295-318} } @InProceedings{ z:breu94, author = {P. T. Breuer and J. P. Bowen}, title = {Towards Correct Executable Semantics for {Z}}, pages = {185-209}, annote = {}, crossref = {z:z94}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/zx.ps.Z} } @TechReport{ z:brie92, author = {S. M. Brien and J. E. Nicholls}, title = {{Z} Base Standard}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-107}, url = { http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-107.html ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zstandard1.0.ps.Z ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zstandard-annex1.0.ps.Z http://www.comlab.ox.ac.uk/oucl/groups/zstandards/}, isbn = {0-902928-84-8}, month = nov, year = 1992, note = {Accepted for standardization under ISO/IEC JTC1/SC22.}, annote = {This is the first publicly available version of the proposed ISO Z Standard. The latest draft is Version 1.2, September 1995. See also \cite{z:spiv92} for a widely used Z reference manual.}, other = {Obtainable from the OUCL Librarian. This has also been produced as a ZIP Project Technical Report ZIP/PRG/92/121, SRC Document: 132, Version 1.0.} } @InProceedings{ z:brie94, author = {S. M. Brien}, title = {The Development of {Z}}, booktitle = {Semantics of Specification Languages (SoSL)}, editor = {D. J. Andrews and J. F. Groote and C. A. Middelburg}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, other = {Proc.\ International Workshop on Semantics of Specification Languages}, location = {Utrecht, The Netherlands, 25-27 October 1993}, pages = {1-14}, isbn = {3-540-19854-7}, year = 1994 } @Article{ z:brit93, author = {C. Britton and M. Loomes and R. Mitchell}, editor = {A. N\'u{\~n}ez and D. Fay}, title = {Formal Specification as Constructive Diagrams}, booktitle = {Special Volume: Short Notes {EUROMICRO'92}}, journal = {Microprocessing and Microprogramming}, publisher = {Elsevier Science Publishers (North-Holland)}, volume = 37, number = {1--5}, pages = {175-178}, month = jan, year = 1993 } @InProceedings{ z:bros95, author = {M. Brossard-Guerlus and F. Klay}, title = {Introducing Formal Specification in an Industrial Context: An Experiment in {Z}}, pages = {229-242}, annote = {}, crossref = {z:habr95} } @InProceedings{ z:brow87, author = {D. J. Brown and J. P. Bowen}, title = {The {Event} {Queue}: An Extensible Input System for {UNIX} Workstations}, booktitle = {Proc.\ {European Unix Users Group} Conference}, other = {EUUG}, location = {Helsinki, Finland, 12--14 May 1987}, pages = {29-52}, address = {Helsinki, Finland}, month = {12--14 May}, year = 1987, comment = {Available from EUUG Secretariat, Owles Hall, Buntingford, Hertfordshire SG9 9PL, UK.} } @InProceedings{ z:brow90, author = {D. Brownbridge}, title = {Using {Z} to Develop a {CASE} Toolset}, annote = {}, crossref = {z:z90}, pages = {142-149}, year = 1990 } @InProceedings{ z:brue95, author = {J.-M. Bruel and A. Benzekri and Y. Raymaud}, title = {{Z} and the Specification of Real-time Systems}, pages = {77-91}, annote = {}, crossref = {z:habr95} } @InProceedings{ z:brya90, author = {A. Bryant}, title = {Structured Methodologies and Formal Notations: Developing a Framework for Synthesis and Investigation}, annote = {}, crossref = {z:z90}, pages = {229-241}, year = 1990 } @InProceedings{ z:brya95, author = {A. Bryant and A. S. Evans and L. Semmens and R. Milovanovic and S. Stockman and M. Norris and C. Selley}, title = {Using {Z} to Rigorously Review a Specification of a Network Management System}, pages = {423-433}, annote = {}, crossref = {z:z95} } @Article{ z:brya95b, author = {A. Bryant and A. S. Evans}, title = {Formalizing the {Object Management Group}'s {Core Object Model}}, journal = {Computer Standards \& Interfaces}, volume = 17, number = {5--6}, pages = {481-489}, month = sep, year = 1995, publisher = {Elsevier Science Publishers (North-Holland)} } @Proceedings{ z:brya96, editor = {A. Bryant and L. Semmens}, title = {Methods Integration}, booktitle = {Methods Integration}, publisher = {Springer-Verlag}, series = {Electronic Workshops in Computing}, location = {Leeds, UK, 25-26 March 1996}, isbn = {3-540-76065-2}, price = {\pounds29.00, BCS member price: \pounds23.00}, year = 1996, url = {http://www.springer.co.uk/ewic/workshops/MI96/}, annote = {Proceedings of the Methods Integration Workshop, University of Leeds, UK, 25--26 March 1996. See \cite{z:dunc96,z:fran96,z:hinc96,z:hook96,z:kasu96b,z:lano96,z:raws96}.} } @Article{ z:buck91, author = {G. R. Buckberry}, title = {{ZED}: A {Z} Notation Editor and Syntax Analyser}, journal = {BCS-FACS FACTS}, volume = {Series II, 2}, number = 3, pages = {13-23}, month = nov, year = 1991 } @InProceedings{ z:burn87, author = {A. Burns and A. J. Wellings}, title = {{Occam}'s Priority Model and Deadline Scheduling}, booktitle = {Proc.\ 7th {Occam} User Group Meeting, {Grenoble}}, year = 1987 } @Article{ z:burn89c, author = {A. Burns and I. W. Morrison}, title = {A Formal Description of the Structure Attribute Model for Tool Interfacing}, journal = {IEE/BCS Software Engineering Journal}, volume = 4, number = 2, pages = {74-78}, month = mar, year = 1989 } @Article{ z:busb92, author = {J. S. Busby and D. Hutchison}, title = {The Practical Integration of Manufacturing Applications}, journal = {Software Practice and Experience}, address = {GEC Alsthom Tract Ltd, Strand Road, Preston PR1 8XL, UK and University of Lancaster, Department of Computer Science, Lancaster LA1 4YR, UK}, pages = {183-207}, volume = 22, number = 2, year = 1992 } @InCollection{ z:buss96, author = {R. B\"ussow and M. Weber}, title = {A Steam-Boiler Control Specification with {Statecharts} and {Z}}, editor = {J.-R. Abrial and E. B\"orger and H. Langmaack}, booktitle = {Formal Methods for Industrial Applications}, annote = {}, crossref = {z:abri96b}, pages = {109-128} } @Article{ z:butc91, author = {P. Butcher}, title = {A Behavioural Semantics for {Linda-2}}, journal = {IEE/BCS Software Engineering Journal}, pages = {196-204}, volume = 6, number = 4, month = jul, year = 1991 } @InProceedings{ z:butl91, author = {M. J. Butler}, title = {Service Extension at the Specification Level}, annote = {}, crossref = {z:z91}, pages = {319-336} } @InProceedings{ z:butl97, title = {An Approach to the Design of Distributed Systems with {B AMN}}, author = {M. J. Butler}, annote = {}, pages = {223-241}, crossref = {z:z97} } @InProceedings{ z:butl97b, title = {A {Z} Specification of Use Cases: A Preliminary Report}, author = {Butler, G. and Grogono, P. and Khendek, F.}, year = 1997, month = {2--5 December}, pages = {505-506}, publisher = {IEEE Computer Society Press}, issn = {0-81-868271-X}, booktitle = {Proc.\ Asia-Pacific Software Engineering Conference / International Computer Science Conference (APSEC'97/ICSC'97)}, address = {Hong Kong}, location = {Hong Kong, 2--5 December 1997} } @Article{ z:butl98, title = {Defining Composition Operators for Object Interaction}, author = {Butler, S. and Duke, R.}, journal = {Object Oriented Systems}, year = 1998, volume = 5, number = 1, pages = {1-16}, issn = {0969-9767}, abstract = {Operations in object-oriented systems are often a composition of other operations, defined across multiple objects. The aim of this paper is to formally develop a suite of composition operators for specifying object interaction through operation composition. Experience with using Object-Z to design a range of object-oriented systems has suggested that four composition operators - conjunction, parallel, choice and sequential composition - are necessary and, at least for commonly occurring architectures, sufficient. In this paper, an abstract model of operations in object-oriented systems is first developed and used as the basis for defining the formal semantics of these composition operators.}, keywords = {object interaction, composing operations, denotational semantics, modelling object-oriented systems, formal methods} } @Article{ z:camp97, title = {Specifying Active Database Systems in an Object-Oriented Framework}, author = {Campin, J. and Paton, N. and Williams, M. H.}, journal = {International Journal of Software Engineering and Knowledge Engineering}, year = 1997, volume = 7, number = 1, pages = {101-123}, issn = {0218-1940}, abstract = {This paper presents a framework for the formal specification of active database systems, and shows how the framework can be used to describe the functionality of three well known example systems, namely Starburst, POSTGRES and Ariel. The framework has been developed using Object-Z to structure specifications in a way that emphasises commonalities and key differences between the designs, and that is readily extensible to support new constructs and systems. Such a formal framework can be used to provide formal descriptions of systems that have previously been described only informally, to compare the functionalities of different systems by contrasting support for fundamental concepts, and as a basis for reasoning about rule bases in the context of different active rule systems. The paper also demonstrates the applicability of object-oriented formal methods to the specification of advanced database functionality.}, keywords = {active databases, formal specification, DBMS, object-oriented} } @InProceedings{ z:carr90, author = {D. Carrington and D. J. Duke and R. Duke and P. King and G. A. Rose and G. Smith}, editor = {S. Vuong}, title = {{Object-Z}: An Object-Oriented Extension to {Z}}, booktitle = {Formal Description Techniques, {II} ({FORTE'89})}, publisher = {Elsevier Science Publishers (North-Holland)}, location = {Vancouver, Canada, December 1989}, pages = {281-296}, year = 1990, other = {Proc.\ 2nd International Conference FORTE'89. Originally published as Technical Report 105, Department of Computer Science, University of Queensland, Australia, 1989.} } @InProceedings{ z:carr90b, author = {D. Carrington and G. Smith}, title = {Extending {Z} for Object-oriented Specifications}, booktitle = {Proc.\ 5th Australian Software Engineering Conference ({ASWEC'90})}, publisher = {IREE}, address = {Australia}, pages = {9-14}, year = 1990 } @InProceedings{ z:carr92, author = {D. Carrington}, title = {{ZOOM} Workshop Report}, crossref = {z:z92}, pages = {352-364}, annote = {This paper records the activities of a workshop on Z and object-oriented methods held in August 1992 at Oxford. A comprehensive bibliography is included.} } @Article{ z:carr93, author = {D. Carrington and D. J. Duke and I. J. Hayes and J. Welsh}, title = {Deriving Modular Designs from Formal Specifications}, booktitle = {Proc.\ SIGSOFT'93 Symposium on the Foundations of Software Engineering}, journal = {ACM Software Engineering Notes}, volume = 18, number = 5, pages = {89-98}, month = dec, year = 1993, abstract = {We consider the problem of designing the top-level modular structure of an implementation. Our starting point is a formal specification of the system. Our approach is to analyse the references to the state variables by the operations of the system. Operations that reference/modify similar sets of variables are likely candidates for grouping into a module. We evaluate the strategy by applying it to a large Z specification of a language-based editor.} } @InProceedings{ z:carr94, author = {D. Carrington and P. Stocks}, title = {A Tale of Two Paradigms: Formal Methods and Software Testing}, pages = {51-68}, url = {ftp://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr94-4.ps.Z}, annote = {Also available as Technical Report 94-4, Department of Computer Science, University of Queensland, Australia, 1994.}, crossref = {z:z94} } @InProceedings{ z:chal90, author = {P. Chalin and P. Grogono}, title = {{Z} Specification of an Object Manager}, annote = {}, crossref = {z:bjor90}, pages = {41-71} } @InProceedings{ z:chan94, author = {D. K. C. Chan and P. W. Trinder}, title = {An Object-Oriented Data Model Supporting Multi-Methods, Multiple Inheritance, and Static Type Checking: A Specification in {Z}}, pages = {297-315}, annote = {}, crossref = {z:z94} } @InProceedings{ z:chan94b, author = {W. Chantatub and M. Holcombe}, title = {Software testing strategies for software requirements and design}, booktitle = {Proc.\ EuroSTAR'94}, location = {Brussels, Belgium, 10-13 October 1994}, publisher = {Software Quality Engineering}, address = {3000-2 Hartley Road, Jacksonville, Florida 32257, USA}, pages = {40/1-40/29}, year = 1994, annote = {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.} } @InProceedings{ z:chau95, author = {J. Y. Chauvet}, title = {Le Cas ``Legislation Viellesse'': Etude de cas}, pages = {243-264}, annote = {}, crossref = {z:habr95} } @Article{ z:chun97, title = {Object-Oriented Software Testing and Metric in {Z} Specification}, author = {Chung, C. M. and Shih, T. K. and Wang, C. C.}, journal = {Information Sciences}, year = 1997, volume = 98, number = {1--4}, pages = {175-202}, issn = {0020-0255}, abstract = {Software testing and metrics are key issues to improve software quality. They are important issues in the research of software engineering. In line with the methodologies of object-oriented analysis and design widely developed, many testing and metrics techniques have been proposed. However, not many focus on the testing criteria and metrics evaluation of an inheritance hierarchy. In this paper, we introduce a concept named unit repeated inheritance (URI) in Z to realize object-oriented testing and object-oriented metrics. The approach describes an inheritance level technique (ILT) method as a guide to test and measure the software complexity of an inheritance hierarchy. The measurement of inheritance metrics and some testing criteria thus can be formed based on the proposed mechanism.} } @InProceedings{ z:ciac95, author = {P. Ciaccia and P. Ciancarini and W. Penzo}, title = {A Formal Approach to Software Design: The {Clepsydra} Methodology}, pages = {5-24}, annote = {}, crossref = {z:z95} } @InProceedings{ z:ciac95b, author = {P. Ciaccia and P. Ciancarini}, title = {A Course on Formal Methods in Software Engineering: Matching Requirements with Design}, pages = {482-496}, annote = {}, crossref = {z:z95} } @Article{ z:ciac97, title = {Formal Requirements and Design Specifications: The {Clepsydra} Methodology}, author = {Ciaccia, P. and Ciancarini, P. and Penzo, W.}, journal = {International Journal of Software Engineering and Knowledge Engineering}, year = 1997, volume = 7, number = 1, pages = {1-42}, issn = {0218-1940}, abstract = {The use of formal methods early in the development process has been advocated as a way of improving the quality of software products and their production process. Here we study the influence of a formal requirements document on the next phase in the software process, that is design. We suggest that formal design should coherently follow from formal requirements. We show that two different formal notations can be effectively used, one for writing requirements specification and one for design specification. We also consider how a design specification can be formally checked with respect to requirements specification. The notations we choose are well known: the Z notation for requirements and the Larch two-tiered language for design. We show how a number of tools based on these notations can be used to improve the quality of the documents produced during the development process.}, keywords = {interface language, software process, formal methods, verification tools, Z, Larch} } @InProceedings{ z:cian96, title = {Analyzing the Dynamics of a {Z} Specification}, author = {Ciancarini, P. and Mascolo, C.}, editor = {Calmet, J. and Limongelli, C.}, isbn = {3-54-061697-7}, booktitle = {Proc.\ 4th International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO'96)}, location = {Karlsruhe, Germany, 18--20 September 1996}, series = lncs, publisher = {Springer-Verlag}, year = 1996, volume = 1128, pages = {138-149}, issn = {0302-9743}, abstract = {We present a method for analyzing the dynamics of a Z document describing a non-sequential system. First a formal operational semantics based on the chemical metaphor is given to Z. Then, some Unity-like temporal logic constructs are defined on such a formal operational semantics in order to allow the specification and analysis of dynamic and temporal properties of concurrent systems, such as safety and liveness properties.} } @InProceedings{ z:cian97, title = {Analysing and Refining an Architectural Style}, author = {P. Ciancarini and C. Mascolo}, annote = {}, pages = {349-368}, crossref = {z:z97} } @Article{ z:cian97b, title = {Engineering Formal Requirements: An Analysis and Testing Method for {Z} Documents}, author = {Ciancarini, P. and Cimato, S. and Mascolo, C.}, journal = {Annals of Software Engineering}, year = 1997, volume = 3, pages = {189-219}, issn = {1022-7091}, abstract = {Z is a declarative, non-executable specification language; its diffusion in the field of requirements engineering outside academia is slow but growing. In this paper we focus on some methods for analyzing and testing Z specification documents, with special emphasis on non-sequential systems specifications. We describe two techniques we have adopted: the former allows the specifier to add to the requirements document a number of properties that then can be checked using a formal semantics; the latter makes it possible to build directly from the requirements specification document a distributed prototype which can be executed and tested over a network of workstations.}, keywords = {chemical abstract machine, specifications, system} } @InProceedings{ z:cian98, title = {Visualizing {Z} Notation in {HTML} Documents}, author = {P. Ciancarini and C. Mascolo and F. Vitali}, annote = {}, pages = {81-95}, crossref = {z:z98} } @Article{ z:cian98b, title = {An Extensible Rendering Engine for {XML} and {HTML}}, author = {Ciancarini, P. and Rizzi, A. and Vitali, F.}, journal = {Computer Networks and ISDN Systems}, year = 1998, volume = 30, number = {1--7}, pages = {225-237}, issn = {0169-7552}, abstract = {XML has been proposed in order to bring to the Web a markup language free of the shortcomings of HTML, in particular the inextensibility of the set of valid elements (tags). Stylesheet languages have been proposed for XML, in order to provide precise and sophisticated typographical control over the appearance of text-based data. We have developed a rendering engine for HTML and XML documents, providing rudimentary support for typography, but allowing easy extensions (displets) for any kind of data, including non-textual ones, such as math, charts, graphs, etc. Some extensions have already been developed: here we present the one for supporting Z, a notation for formal specifications of software systems.}, keywords = {XML, markup languages, XSL, stylesheet languages, displets} } @Article{ z:cohe89, author = {B. Cohen}, title = {Justification of Formal Methods for System Specifications \& {A} Rejustification of Formal Notations}, journal = {IEE/BCS Software Engineering Journal}, volume = 4, number = 1, pages = {26-38}, month = jan, year = 1989 } @InProceedings{ z:cohe90, author = {B. Cohen and D. Mannering}, title = {The Rigorous Specification and Verification of the Safety Aspects of a Real-Time System}, booktitle = {Proc.\ COMPASS '90}, address = {Gaithersburg, USA}, year = 1990 } @InProceedings{ z:cohe97, author = {B. Cohen}, title = {Set Theory as a Semantic Framework for Object-Oriented Modeling}, annote = {}, length = 6, crossref = {z:bosc97} } @Article{ z:cole97, title = {Synthesizing Structured Analysis and Object-Based Formal Specifications}, author = {Coleman, D. L. and Baker, A. L.}, journal = {Annals of Software Engineering}, year = 1997, volume = 3, pages = {221-253}, issn = {1022-7091}, abstract = {Structured Analysis (SA) is a widely-used software development method. SA specifications are based on Data mow Diagrams (DFD's), Data Dictionaries (DD's) and Process Specifications (P-Specs). As used in practice, SA specifications are not formal. Seemingly orthogonal approaches to specifications are those using formal, object-based, abstract model specification languages, e.g., VDM, Z, Larch/C++ and SPECS. These languages support object-based software development in that they are designed to specify abstract data types (ADT's). We suggest formalizing SA specifications by: (i) formally specifying flow value types as ADT's in DD's, (ii) formally specifying P-Specs using both the assertional style of the aforementioned specification languages and ADT operations defined in DD's, and (iii) adopting a formal semantics for DFD ''execution steps''. The resulting formalized SA specifications, DFD-SPECS, are well-suited to the specification of distributed or concurrent systems. We provide an example DFD-SPEC for a client-server system with a replicated server. When synthesized with our recent results in the direct execution of formal, model-based specifications, DFD-SPECS will also support the direct execution of specifications of concurrent or distributed systems.}, keywords = {data flow diagram, distributed software, Petri nets, systems} } @InCollection{ z:coll91, author = {B. P. Collins and J. E. Nicholls and I. H. S{\o}rensen}, editor = {B. Neumann and others}, title = {Introducing Formal Methods: The {CICS} Experience with {Z}}, booktitle = {Mathematical Structures for Software Engineering}, publisher = {Oxford University Press}, year = 1991, other = {Originally published as IBM Technical Report TR12.260, December 1987.} } @InCollection{ z:comb95, author = {A. C. Coombes and L. Barroca and J. S. Fitzgerald and J. A. McDermid and L. Spencer and A. Saeed}, title = {Formal Specification of an Aerospace System: The Attitude Monitor}, crossref = {z:hinc95}, pages = {307-332}, annote = {} } @Article{ z:cook92, author = {J. Cooke}, title = {Editorial -- Formal Methods: What? Why? and When?}, journal = {The Computer Journal}, volume = 35, number = 5, pages = {417-418}, month = oct, year = 1992, annote = {An editorial introduction to two special issues on {\em Formal Methods}. See also \cite{z:barr92b,z:cook92b,z:misi92,z:semm92,z:wood92b} for papers relevant to Z.} } @Article{ z:cook92b, author = {J. Cooke}, title = {Formal methods -- Mathematics, Theory, Recipes or what?}, journal = {The Computer Journal}, volume = 35, number = 5, pages = {419-423}, month = oct, year = 1992 } @InProceedings{ z:coom91, author = {A. C. Coombes and J. A. McDermid}, title = {A Tool for Defining the Architecture of {Z} Specifications}, annote = {}, crossref = {z:z91}, pages = {77-92} } @InProceedings{ z:coom93, author = {A. C. Coombes and J. A. McDermid}, title = {Using Diagrams to Give a Formal Specification of Timing Constraints in {Z}}, annote = {}, crossref = {z:z93}, pages = {119-130} } @InProceedings{ z:coop90, author = {D. Cooper}, title = {Educating Management in {Z}}, annote = {}, crossref = {z:z90}, pages = {192-194}, year = 1990 } @InProceedings{ z:cord94, author = {V. A. O. Cordeiro and A. C. A. Sampaio and S. L. Meira}, title = {From {MooZ} to {Eiffel} -- A Rigorous Approach to System Development}, annote = {}, crossref = {z:naft94}, pages = {306-325} } @Article{ z:crag92, author = {S. Craggs and J. B. Wordsworth}, editor = {S. Harvey}, title = {{Hursley Lab} wins another {Queen's Award} \& {Hursley} and {Oxford} -- A marriage of minds \& {Z} stands for quality}, journal = {Developments, IBM Hursley Park}, volume = 8, pages = {1-2}, month = {21 April}, year = 1992 } @InProceedings{ z:crai91, author = {D. Craigen and S. Kromodimoeljo and I. Meisels and W. Pase and M. Saaltink}, title = {{EVES}: An Overview}, annote = {}, note = {}, crossref = {z:preh91}, pages = {389-405}, url = {http://www.ora.on.ca/biblio.html#ckmps:eves} } @Book{ z:crai91c, author = {I. Craig}, title = {The Formal Specification of Advanced {AI} Architectures}, publisher = {Ellis Horwood}, series = {AI Series}, length = 320, month = sep, year = 1991, annote = {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 {\em 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.} } @TechReport{ z:crai93, author = {D. Craigen and S. L. Gerhart and T. J. Ralston}, title = {An International Survey of Industrial Applications of Formal Methods}, institution = {Atomic Energy Control Board of Canada, US National Institute of Standards and Technology, and US Naval Research Laboratories}, number = {NIST GCR 93/626-V1 \& 2}, url = {http://nemo.ncsl.nist.gov/ahis/formal_methods/}, annote = {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.}, other = {Phone: +1-703-487-4650}, year = 1993 } @InProceedings{ z:crai93b, author = {D. Craigen and S. L. Gerhart and T. J. Ralston}, title = {Formal Methods Reality Check: Industrial Usage}, other = {Revised version in \cite{z:crai95b}.}, crossref = {z:wood93}, pages = {250-267} } @InProceedings{ z:crai93c, author = {D. Craigen and S. L. Gerhart and T. J. Ralston}, title = {An International Survey of Industrial Applications of Formal Methods}, annote = {}, crossref = {z:z93}, pages = {1-5} } @InCollection{ z:crai95, author = {D. Craigen and S. L. Gerhart and T. J. Ralston}, title = {Formal Methods Technology Transfer: Impediments and Innovation}, crossref = {z:hinc95}, pages = {399-419}, annote = {} } @Article{ z:crai95b, author = {D. Craigen and S. L. Gerhart and T. J. Ralston}, title = {Formal Methods Reality Check: Industrial Usage}, journal = {IEEE Transactions on Software Engineering}, volume = 21, number = 2, pages = {90-98}, month = feb, year = 1995, annote = {Revised version of \cite{z:crai93b}.} } @InCollection{ z:crow96, author = {Crowcroft, J. and d'Inverno, M.}, title = {Languages and Formal Methods}, booktitle = {Open Distributed Systems}, editor = {Crowcroft, J.}, pages = {99-137}, publisher = {UCL Press}, address = {London}, year = 1996 } @InProceedings{ z:cusa90, author = {E. Cusack and M. Lai}, editor = {J. W. {de Bakker} and W. P. {de Roever} and G. Rozenberg}, title = {Object Oriented Specification in {LOTOS} and {Z} (or My Cat Really is Object Oriented!)}, booktitle = {{REX/FOOL} School/Workshop on Foundations of Object-Oriented Languages}, location = {Noordwijkerhout, The Netherlands, May 1990}, publisher = {Springer-Verlag}, series = lncs, volume = 489, pages = {179-202}, year = 1990 } @InProceedings{ z:cusa91, author = {E. Cusack}, editor = {P. America}, title = {Inheritance in Object Oriented {Z}}, booktitle = {Proc.\ {ECOOP'91} {European} Conference on Object-Oriented Programming}, publisher = {Springer-Verlag}, series = lncs, volume = 512, location = {Geneva, Switzerland, July 1991}, isbn = {3-540-54262-0}, pages = {167-179}, year = 1991 } @InProceedings{ z:cusa92, author = {E. Cusack}, editor = {J. {de Meer}}, title = {Object Oriented Modelling in {Z} for Open Distributed Systems}, booktitle = {Proc.\ International Workshop on {ODP}}, location = {Berlin, October 1991}, publisher = {Elsevier Science Publishers (North-Holland)}, year = 1992 } @InProceedings{ z:cusa93, author = {E. Cusack and C. D. Wezeman}, title = {Deriving Tests for Objects Specified in {Z}}, annote = {}, crossref = {z:z93}, pages = {180-195} } @InProceedings{ z:cusa93b, author = {E. Cusack}, title = {Using {Z} in Communications Engineering}, annote = {}, crossref = {z:z93}, pages = {196-202} } @Article{ z:dean95, author = {N. Dean and M. G. Hinchey}, title = {Introducing Formal Methods through R\^ole-Playing}, booktitle = {Proc.\ ACM SIGCSE'95, ACM Conference on Computer Science Education}, journal = {ACM SIGCSE Bulletin}, location = {Nashville, Tennessee, USA, March 1995}, organization = {ACM}, url = {http://www.cl.cam.ac.uk/users/mgh1001/EDUCATION/sigcse95.ps} , volume = 27, number = 1, pages = {302-306}, month = mar, year = 1995 } @InProceedings{ z:dean95b, author = {N. Dean}, title = {Mental Models of {Z}: {I} -- Sets and Logic}, pages = {498-507}, annote = {}, crossref = {z:z95} } @Book{ z:dean97, author = {N. Dean}, title = {The Essence of Discrete Mathematics}, publisher = {Prentice Hall}, series = {The Essence of Computing Series}, isbn = {0-13-345943-8}, year = 1997, annote = {An introductory book using a Z-like notation.} } @Article{ z:dear97, title = {A Software Engineering Model for Case Memory Systems}, author = {Dearden, A. M. and Harrison, M. D.}, journal = {The Computer Journal}, year = 1997, volume = 40, number = 4, pages = {167-182}, issn = {0010-4620}, abstract = {This paper describes a generic model for case memory systems expressed using the Z notation, A case memory system is an essential part of any case-based reasoning system, and provides a mechanism for storing old cases, and for assessing the relationship between the stored cases and a new problem, Using the model, characteristics that have been claimed for specific case memory systems in the literature, e.g. responsiveness to a reasoner's goals or use of past experience in case assessment, are expressed formally in terms of constraints on the means by which case relations are computed, The model supports precise reasoning about the characteristics of specific systems and offers insight into the variety of options available to software or knowledge engineers seeking to reuse a case memory system, to select a case memory system shell or to develop a new system.} } @InProceedings{ z:deba92, author = {R. S. M. {de Barros} and D. J. Harper}, title = {A Method for the Specification of Relational Database Applications}, annote = {}, crossref = {z:z92}, url = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/roberto/zmeet91.ps}, pages = {261-286} } @InProceedings{ z:deba92b, author = {R. S. M. {de Barros} and D. J. Harper}, title = {Formal Development of Relational Database Applications}, editor = {D. J. Harper and M. C. Norrie}, booktitle = {Specifications of Database Systems, Glasgow 1991}, location = {Glasgow, UK, 1991}, url = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/roberto/sods.ps}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, pages = {21-43}, year = 1992, other = {Zc, a Z-like formalism, is used.} } @InProceedings{ z:deba94, author = {R. S. M. {de Barros}}, title = {Deriving Relational Database Programs from Formal Specifications}, annote = {}, crossref = {z:naft94}, url = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/roberto/fme94.ps}, pages = {703-723} } @InProceedings{ z:dehb94, author = {B. Dehbonei and F. Mejia}, title = {Formal Methods in the Railways Signalling Industry}, annote = {}, crossref = {z:naft94}, pages = {26-34} } @InProceedings{ z:deli89, author = {N. Delisle and D. Garlan}, title = {Formally Specifying Electronic Instruments}, booktitle = {Proc.\ 5th International Workshop on Software Specification and Design}, publisher = {IEEE Computer Society}, month = may, year = 1989, note = {Also published in {\em ACM SIGSOFT Software Engineering Notes}, 14(3)} } @Article{ z:deli90, author = {N. Delisle and D. Garlan}, title = {A Formal Specification of an Oscilloscope}, journal = {IEEE Software}, volume = 7, number = 5, pages = {29-36}, month = sep, year = 1990, annote = {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.} } @InProceedings{ z:deli95, author = {P. D. {de Lima Machado} and S. L. Meira}, title = {On the Use of Formal Specifications in the Design and Simulation of Artificial Neural Nets}, pages = {63-82}, annote = {}, crossref = {z:z95} } @InProceedings{ z:derr95, author = {J. Derrick and H. Bowman and M. Steen}, title = {Viewpoints and Objects}, pages = {449-468}, annote = {}, crossref = {z:z95}, url = {http://alethea.ukc.ac.uk/Dept/Computing/Research/NDS/consistency/zum.html} } @InProceedings{ z:derr95b, author = {J. Derrick and H. Bowman and M. Steen}, title = {Maintaining Cross Viewpoint Consistency using {Z}}, editor = {K. Raymond and L. Armstrong}, booktitle = {IFIP TC6 International Conference on Open Distributed Processing}, publisher = {Chapman \& Hall}, location = {Brisbane, Australia}, pages = {413-424}, isbn = {0-41271-150-8}, month = feb, year = 1995, url = {http://alethea.ukc.ac.uk/Dept/Computing/Research/NDS/consistency/icodpz.html} } @InProceedings{ z:derr96, author = {J. Derrick and E. A. Boiten and H. Bowman and M. Steen}, title = {Supporting {ODP} -- Translating {LOTOS} to {Z}}, editor = {E. Najm and J.-B. Stefani}, booktitle = {Proc.\ 1st IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems}, pages = {399-406}, publisher = {Chapman \& Hall}, location = {Paris, France, March 1996}, isbn = {0-41279-770-4}, month = mar, year = 1996, url = {http://alethea.ukc.ac.uk/Dept/Computing/Research/NDS/consistency/lotosz.html} } @InProceedings{ z:derr97, title = {Weak Refinement in {Z}}, author = {J. Derrick and E. A. Boiten and H. Bowman and M. Steen}, annote = {}, pages = {369-388}, crossref = {z:z97} } @InProceedings{ z:derr97b, author = {J. Derrick and E. A. Boiten and H. Bowman and M. Steen}, title = {Translating {LOTOS} to {O}bject-{Z}}, booktitle = {Northern Formal Methods Workshop}, series = {Electronic Workshops In Computing}, editor = {D. J. Duke and A. S. Evans}, url = {http://ewic.springer.co.uk/workshops/NFM97/}, publisher = {Springer-Verlag}, year = 1997 } @InProceedings{ z:derr98, title = {Testing Refinements by Refining Tests}, author = {J. Derrick and E. A. Boiten}, annote = {}, pages = {265-283}, crossref = {z:z98} } @InProceedings{ z:dick90, author = {A. J. J. Dick and P. J. Krause and J. Cozens}, title = {Computer Aided Transformation of {Z} into {Prolog}}, annote = {}, crossref = {z:z90}, pages = {71-85}, year = 1990 } @InProceedings{ z:diep90, author = {M. J. {van Diepen} and K. M. {van Hee}}, title = {A Formal Semantics for {Z} and the Link between {Z} and the Relational Algebra}, annote = {}, crossref = {z:bjor90}, pages = {526-551} } @InProceedings{ z:dill92, author = {A. Diller}, title = {{Z} and {Hoare} Logics}, annote = {}, crossref = {z:z92}, pages = {59-76} } @Book{ z:dill94, author = {A. Diller}, title = {{Z}: An Introduction to Formal Methods}, publisher = {John Wiley \& Sons}, year = 1994, edition = {2nd}, length = 374, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0471939730}, isbn = {0-471-93973-0}, annote = {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 {\em The Z Notation} \cite{z:spiv92} is used throughout. \par Contents: Tutorial introduction; Methods of reasoning; Case studies; Specification animation; Reference manual; Answers to exercises; Glossaries of terms and symbols; Bibliography.} } @InProceedings{ z:dill94b, author = {A. Diller and R. Docherty}, title = {{Z} and Abstract Machine Notation: A Comparison}, pages = {250-263}, annote = {}, crossref = {z:z94} } @InProceedings{ z:dinv91, author = {d'Inverno, M. and Crowcroft, J.}, title = {Design, Specification and Implementation of a Real Time Conferencing System}, pages = {1114-1125}, year = 1991, booktitle = {Proc.\ 10th Annual Joint Conference of IEEE INFOCOM'91}, address = {New York, USA} } @InProceedings{ z:dinv95, author = {M. d'Inverno and M. Priestley}, title = {Structuring Specification in {Z} to Build a Unifying Framework for Hypertext Systems}, pages = {83-102}, annote = {}, crossref = {z:z95} } @InProceedings{ z:dinv96, author = {d'Inverno, M. and Justo, G. R. and Howells, P.}, title = {A Formal Framework for Specifying Design Methodologies}, editor = {H. El-Rewini and B. D. Shriver}, booktitle = {Proc.\ 29th Annual Hawaii International Conference on System Sciences}, publisher = {IEEE Computer Society Press}, pages = {741-750}, year = 1996 } @InProceedings{ z:dinv96b, author = {d'Inverno, M. and Luck, M.}, title = {A Formal View of Social Dependence Networks}, editor = {Zhang, C. and Lukose, D.}, booktitle = {Distributed Artificial Intelligence Architecture and Modelling: Proc.\ 1st Australian Workshop on Distributed Artificial Intelligence}, series = {Lecture Notes in Artificial Intelligence}, volume = 1087, publisher = {Springer-Verlag}, pages = {115-129}, year = 1996 } @InProceedings{ z:dinv96c, author = {d'Inverno, M. and Luck, M.}, title = {Formalising the Contract Net as a Goal Directed System}, booktitle = {Agents Breaking Away: Proc.\ 7th European Workshop on Modelling Autonomous Agents in a Multi Agent World, Lecture Notes in Artificial Intelligence}, volume = 1038, editor = {{Van de Velde}, W. and Perram, J.W.}, publisher = {Springer-Verlag}, pages = {72-85}, year = 1996 } @InProceedings{ z:dinv96d, author = {d'Inverno, M. and Luck, M.}, title = {Understanding Autonomous Interaction}, booktitle = {Proc.\ 13th European Conference on Artificial Intelligence (ECAI'96)}, editor = {W. Wahlster}, publisher = {John Wiley \& Sons}, pages = {529-533}, year = 1996 } @Article{ z:dinv96e, author = {d'Inverno, M. and Justo, G. R. and Howells, P.}, title = {A Formal Framework for Specifying Design Methodologies}, journal = {Software Process: Improvement and Practice}, publisher = {John Wiley \& Sons}, pages = {181-195}, volume = 2, number = 3, year = 1996 } @InProceedings{ z:dinv97, title = {A {Z} Specification of the Soft-Link Hypertext Model}, author = {M. d'Inverno and M. J. Hu}, annote = {}, pages = {297-316}, crossref = {z:z97} } @Article{ z:dinv97b, author = {d'Inverno, M. and Priestley, M. and Luck, M.}, title = {A Formal Framework for Hypertext Systems}, journal = {IEE Proceedings -- Software Engineering}, pages = {175-184}, volume = 144, number = 3, month = jun, year = 1997 } @InProceedings{ z:dinv97c, author = {d'Inverno, M. and Luck, M.}, title = {Making and Breaking Engagements: An Operational Analysis of Agent Relationships}, booktitle = {Multi-Agent Systems Methodologies and Applications: Proc.\ 2nd Australian Workshop on Distributed Artificial Intelligence, Lecture Notes in Artificial Intelligence}, volume = 1286, editor = {Zhang, C. and Lukose, D.}, publisher = {Springer-Verlag}, pages = {48-62}, year = 1997 } @InProceedings{ z:dinv97d, author = {d'Inverno, M. and Luck, M. and Wooldridge, M.}, title = {Cooperation Structures}, booktitle = {Proc.\ 15th International Joint Conference on Artificial Intelligence}, address = {Nagoya, Japan}, pages = {600-605}, year = 1997 } @InProceedings{ z:dinv97e, author = {d'Inverno, M. and Luck, M.}, title = {Development and Application of an Formal Agent Framework}, pages = {222-231}, annote = {}, crossref = {z:hinc97} } @Article{ z:dinv97f, author = {d'Inverno, M. and Fisher, M. and Lomuscio, A. and Luck, M. and de Rijke, M. and Ryan, M. and Wooldridge, M.}, title = {Formalisms for Multi-Agent Systems}, journal = {Knowledge Engineering Review}, pages = {315-321}, volume = 12, number = 3, annote = {Includes a discussion of the appropriateness of Z for multi-agent systems.}, year = 1997 } @InProceedings{ z:dinv98, author = {d'Inverno, M. and Kinny, D. and Luck, M. and Wooldridge, M.}, title = {A Formal Specification of {dMARS}}, booktitle = {Intelligent Agents IV: Proc.\ 4th International Workshop on Agent Theories, Architectures and Languages}, editor = {Singh, M. and Rao, A. and Wooldridge, M.}, publisher = {Springer-Verlag}, series = lncs, volume = 1365, pages = {155-176}, year = 1998 } @Article{ z:dinv98b, author = {d'Inverno, M. and Luck, M.}, title = {A Formal Specification of {AgentSpeak(L)}}, journal = {Logic and Computation}, volume = 8, number = 3, year = 1998 } @InProceedings{ z:dinv98c, author = {d'Inverno, M. and Kinny, D. and Luck, M.}, title = {Interaction Protocols in {Agentis}}, booktitle = {Proc.\ 3rd International Conference on Multi-Agent Systems (ICMAS'98)}, address = {Paris, France}, year = 1998 } @Book{ z:dix91, author = {A. J. Dix}, title = {Formal Methods for Interactive Systems}, series = {Computers and People Series}, publisher = {Academic Press}, length = 369, isbn = {0-12-218315-0}, year = 1991 } @Book{ z:dix93, author = {A. J. Dix and J. Finlay and G. D. Abowd and R. Beale}, title = {Human-Computer Interaction}, publisher = {Prentice Hall International}, isbn = {0-13-458266-7 (hbk) 0-13-437211-5 (pbk)}, year = 1993 } @InProceedings{ z:doch95, author = {R. F. Docherty}, title = {Translation from {Z} to {AMN}}, pages = {205-228}, annote = {}, crossref = {z:habr95} } @Article{ z:dodg91, author = {C. J. Dodge and P. G. B. Ross and A. R. Allen and P. E. Undrill}, title = {Formal Methods in the Design of an {FFT} Accelerator for a {Transputer} based Image Processing System}, journal = {Medical and Biological Engineering and Computing}, volume = 29, other = {Supplement}, pages = 91, year = 1991 } @PhDThesis{ z:dodg93, author = {C. J. Dodge}, title = {A {Fast Fourier Transform} Accelerator for a {Transputer} System}, school = {University of Aberdeen}, address = {Department of Biomedical Physics, Foresterhill, Aberdeen AB9 2ZD, UK}, annote = {The design includes a detailed Z specification.}, year = 1993 } @Article{ z:dodg96, author = {C. J. Dodge and P. E. Undrill and A. R. Allen and P. G. B. Ross}, title = {Application of {Z} in Digital Hardware Design}, journal = {IEE Proceedings -- Computers and Digital Techniques}, volume = 143, number = 1, pages = {79-86}, year = 1996, issn = {1350-2387}, abstract = {The Z specification language is gaining wide acceptance in both academia and industry as a software development tool. Although there is now a large body of experience in using Z for software development, it is clear that the application areas of Z need not be limited to software alone. Formal design strategies could prove very beneficial in the design of hardware systems, particularly in the areas of requirements analysis and specification at an abstract level. The paper presents an experiment in using Z in the development of a hardware system, giving part of the specification as example and showing how it was used to verify certain aspects of the hardware's behaviour. The refinement process from the abstract specification statements into realised hardware and programmable logic are also shown, concluding with a discussion of the merits of an abstract specification using Z in the context of hardware design.}, keywords = {formal methods, hardware design, Z, fast fourier transform} } @InProceedings{ z:doma91, author = {V. Doma and R. Nicholl}, title = {{EZ}: A System for Automatic Prototyping of {Z} Specifications}, annote = {}, note = {}, crossref = {z:preh91}, pages = {189-203} } @InProceedings{ z:dong94, author = {J. S. Dong and R. Duke and G. A. Rose}, title = {An Object-Oriented Approach to the Semantics of Programming Languages}, booktitle = {Proc.\ 17th {Australian} Computer Science Conference ({ACSC-17})}, url = {ftp://ftp.cs.uq.oz.au/pub/TECHREPORTS/department/languageoz.ps.Z} , pages = {767-775}, month = jan, year = 1994 } @InProceedings{ z:dong94b, author = {J. S. Dong and R. Duke}, title = {An Object-Oriented Approach to the Formal Specification of {ODP} Trader}, booktitle = {Proc.\ IFIP TC6/WG6.1 International Conference on Open Distributed Processing}, location = {Berlin, Germany, 13-16 September 1993}, url = {ftp://ftp.cs.uq.oz.au/pub/TECHREPORTS/department/trader.ps.Z} , pages = {341-352}, month = sep, year = 1993 } @Article{ z:dong97, title = {An Object-Oriented Denotational Semantics of a Small Programming Language}, author = {J. S. Dong and R. Duke and G. Rose}, journal = {Object Oriented Systems}, year = 1997, volume = 4, number = 1, pages = {29-52}, issn = {0969-9767}, abstract = {A denotational semantics of a programming language specifies the meaning of the language in terms of well-defined mathematical structures. To this end, state-based formal specification notations such as VDM and Z can be used to specify denotational semantics by defining the transition from language constructs into mathematical entities. However, when using such notations, the abstract syntax, static semantics and dynamic semantics are typically defined separately using distinct formal structures. As a consequence, adding a new construct to the language usually requires modification of each of the above structures. Furthermore, this traditional denotational semantic style generally has limited modularity and reusability. This paper advocates the use of the Object-Z notation to give an object-oriented specification of programming language semantics. With this approach, programming language constructs, such as expressions and statements, are viewed as objects, with the result that the abstract syntax, static and dynamic semantics of individual language constructs become encapsulated in one class. This modularity assists readability and facilitates subsequent semantic modification with minimal disruption.}, keywords = {denotational semantics, formal methods, object orientation} } @InProceedings{ z:drap93, author = {C. Draper}, title = {Practical Experiences of {Z} and {SSADM}}, annote = {}, crossref = {z:z93}, pages = {240-251} } @Article{ z:duce94, author = {D. A. Duce and D. J. Duke and P. J. W. {ten Hagen} and G. J. Reynolds}, title = {{PREMO} -- An Initial Approach to a Formal Definition}, booktitle = {Proc.\ {EUROGRAPHICS'94}}, editor = {M. D{\ae}hlen and L. Kjelldahl}, publisher = {Blackwell Publishers}, journal = {Computer Graphics Forum}, volume = 13, number = 3, year = 1994, pages = {C-393-C-406}, annote = {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.} } @Article{ z:duce95, author = {D. A. Duce and D. J. Duke and P. J. W. {ten Hagen} and I. Herman and G. J. Reynolds}, title = {Formal Methods in the Development of {PREMO}}, journal = {Computer Standards \& Interfaces}, volume = 17, number = {5--6}, pages = {491-509}, month = sep, year = 1995, publisher = {Elsevier Science Publishers (North-Holland)} } @InProceedings{ z:duke88, author = {R. Duke and I. J. Hayes and P. King and G. A. Rose}, editor = {S. Aggarwal and K. Sabnani}, title = {Protocol Specification and Verification Using {Z}}, booktitle = {Protocol Specification, Testing, and Verification {VIII}}, publisher = {Elsevier Science Publishers (North-Holland)}, pages = {33-46}, year = 1988 } @Article{ z:duke89, author = {R. Duke and G. Smith}, title = {Temporal Logic and {Z} Specifications}, journal = {Australian Computer Journal}, volume = 21, number = 2, pages = {62-69}, month = may, year = 1989 } @InProceedings{ z:duke90, author = {D. J. Duke and R. Duke}, title = {Towards a Semantics for {Object-Z}}, annote = {}, crossref = {z:bjor90}, other = {An outline of the denotational semantics of Object-Z.}, pages = {244-261} } @InProceedings{ z:duke90b, author = {R. Duke and G. A. Rose and A. Lee}, title = {Object-oriented Protocol Specification}, editor = {L. Logrippo and R. L. Probert and H. Ural}, booktitle = {Protocol Specification, Testing, and Verification {X}}, publisher = {Elsevier Science Publishers (North-Holland)}, pages = {325-338}, year = 1990 } @InProceedings{ z:duke90d, author = {R. Duke and D. J. Duke}, title = {Aspects of Object-oriented Formal Specification}, booktitle = {Proc.\ 5th {Australian} Software Engineering Conference ({ASWEC'90})}, publisher = {IREE}, address = {Australia}, pages = {21-26}, year = 1990 } @TechReport{ z:duke91, author = {R. Duke and P. King and G. A. Rose and G. Smith}, title = {The {Object-Z} Specification Language: Version 1}, institution = {Department of Computer Science, University of Queensland}, address = {St.\ Lucia 4072, Australia}, type = {Technical Report}, number = {91-1}, url = {ftp://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr91-1.ps.Z}, month = apr, year = 1991, annote = {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 \cite{z:duke91b}.} } @InCollection{ z:duke91b, author = {R. Duke and P. King and G. A. Rose and G. Smith}, title = {The {Object-Z} Specification Language}, editor = {T. Korson and V. Vaishnavi and B. Meyer}, booktitle = {Technology of Object-Oriented Languages and Systems: {TOOLS 5}}, pages = {465-483}, publisher = {Prentice Hall}, year = 1991 } @Article{ z:duke91c, author = {D. J. Duke}, title = {Structuring {Z} Specifications}, journal = {Australian Computer Science Communications}, volume = 12, number = 1, pages = {1-10}, year = 1991, note = {Proc.\ 14th Australian Computer Science Conference} } @InProceedings{ z:duke92, author = {D. J. Duke}, title = {Enhancing the Structures of {Z} Specifications}, annote = {}, crossref = {z:z92}, pages = {329-351} } @PhDThesis{ z:duke92b, author = {D. J. Duke}, title = {Object-Oriented Formal Specification}, school = {Department of Computer Science, University of Queensland}, address = {St.\ Lucia 4072, Australia}, url = {ftp://ftp.cs.uq.oz.au/pub/Thesis/david_duke.ps.Z}, year = 1992 } @Article{ z:duke95, author = {D. J. Duke and M. D. Harrison}, title = {Event Model of Human-System Interaction}, journal = {IEE/BCS Software Engineering Journal}, volume = 10, number = 1, pages = {3-12}, month = jan, year = 1995 } @Article{ z:duke95b, author = {D. J. Duke and M. D. Harrison}, title = {Mapping User Requirements to Implementations}, journal = {IEE/BCS Software Engineering Journal}, volume = 10, number = 1, pages = {13-20}, month = jan, year = 1995 } @Article{ z:duke95c, author = {R. Duke and G. Rose and G. Smith}, title = {{Object-Z}: A Specification Language Advocated for the Description of Standards}, journal = {Computer Standards \& Interfaces}, volume = 17, number = {5--6}, pages = {511-533}, month = sep, year = 1995, publisher = {Elsevier Science Publishers (North-Holland)}, issn = {0920-5489}, abstract = {The importance of formalising the specification of standards has been recognised for a number of years. This paper advocates the use of the formal specification language Object-Z in the definition of standards. Object-Z is an extension to the Z language specifically to facilitate specification in an object- oriented style. First, the syntax and semantics of Object-Z are described informally. Then the use of Object-Z in formalising standards is demonstrated by presenting a case study based on the ODP Trader. Finally, a formal semantics is introduced that suggests an approach to the standardisation of Object-Z itself. Because standards are typically large complex systems, the extra structuring afforded by the Object-Z class construct and operation expressions enables the various hierarchical relationships and the communication between objects in a system to be succinctly specified.}, keywords = {object-orientation, formal specification, formal semantics, standards} } @InProceedings{ z:dunc96, author = {L. Dunckley and A. Smith}, title = {Improving Access of the Commercial Software Developer to Formal Methods: Integrating {MERISE} with {Z}}, annote = {}, crossref = {z:brya96} } @InProceedings{ z:dupu98, title = {Translating the {OMT} Dynamic Model into {Object-Z}}, author = {S. Dupuy and Y. Ledru and M. Chabre-Peccoud}, annote = {}, pages = {347-366}, crossref = {z:z98} } @Book{ z:edmo92, author = {D. Edmond}, title = {Information Modeling: Specification and Implementation}, publisher = {Prentice Hall}, other = {Australia}, length = 589, isbn = {0-13-457748-5}, price = {c$40 Australian}, year = 1992 } @InProceedings{ z:edmo95, author = {D. Edmond}, title = {Refining Database Systems}, pages = {25-44}, annote = {}, crossref = {z:z95} } @InProceedings{ z:elbe97, author = {J. Ebert and R. S\"uttenbach}, title = {Integration of {Z}-based Semantics of {OO}-Notations}, annote = {}, length = 5, crossref = {z:bosc97} } @InProceedings{ z:enge94, author = {M. Engel}, title = {Specifying Real-Time Systems with {Z} and the {Duration Calculus}}, pages = {282-294}, annote = {}, crossref = {z:z94} } @InProceedings{ z:evan94, author = {A. S. Evans}, title = {Visualising Concurrent {Z} Specifications}, pages = {269-281}, annote = {}, crossref = {z:z94} } @InProceedings{ z:evan94b, author = {A. S. Evans}, title = {Specifying \& Verifying Concurrent Systems Using {Z}}, annote = {}, crossref = {z:naft94}, pages = {366-400} } @InProceedings{ z:evan97, title = {An Improved Recipe for Specifying Reactive Systems in {Z}}, author = {A. S. Evans}, annote = {}, pages = {275-294}, crossref = {z:z97} } @InProceedings{ z:fenc94, author = {P. C. Fencott and A. J. Galloway and M. A. Lockyer and S. J. {O'Brien} and S. Pearson}, title = {Formalising the Semantics of {Ward/Mellor} {SA/RT} Essential Models using a Process Algebra}, annote = {}, crossref = {z:naft94}, pages = {681-702} } @Article{ z:fent88, author = {N. E. Fenton and D. Mole}, title = {A Note on the Use of {Z} for Flowgraph Transformation}, journal = {Information and Software Technology}, volume = 30, number = 7, pages = {432-437}, year = 1988 } @InProceedings{ z:ferg90, author = {E. Fergus and D. C. Ince}, title = {{Z} Specifications and Modal Logic}, editor = {P. A. V. Hall}, booktitle = {Proc.\ Software Engineering 90}, publisher = {Cambridge University Press}, location = {Brighton, UK, July 1990}, series = {British Computer Society Conference Series}, volume = 1, year = 1990 } @InProceedings{ z:fidg91, author = {C. J. Fidge}, title = {Specification and Verification of Real-Time Behaviour using {Z} and {RTL}}, editor = {J. Vytopil}, booktitle = {Formal Techniques in Real-Time and Fault-Tolerant Systems}, location = {University of Nijmegen, The Netherlands, 6--10 January 1992}, institution = {University of Queensland}, publisher = {Springer-Verlag}, series = lncs, pages = {393-410}, year = 1992 } @InProceedings{ z:fidg93, author = {C. J. Fidge}, title = {Real-Time Refinement}, annote = {}, crossref = {z:wood93}, pages = {314-331} } @InProceedings{ z:fidg94, author = {C. J. Fidge}, title = {Proof Obligations for Real-Time Refinement}, pages = {279-305}, annote = {}, crossref = {z:till94} } @InProceedings{ z:fidg94b, author = {C. J. Fidge}, title = {Adding Real Time to Formal Program Development}, annote = {}, crossref = {z:naft94}, pages = {618-638} } @InProceedings{ z:fidg96, author = {C. J. Fidge and M. Utting and P. Kearney and I. J. Hayes}, title = {Integrating Real-time Scheduling Theory and Program Refinement}, pages = {327-346}, annote = {}, crossref = {z:gaud96} } @Article{ z:finn96, author = {K. Finney}, title = {Mathematical Notation in Formal Specification: Too Difficult for the Masses?}, journal = {IEEE Transactions on Software Engineering}, volume = 22, number = 2, pages = {158-159}, month = feb, year = 1996 } @InProceedings{ z:fisc98, title = {How to Combine {Z} with a Process Algebra}, author = {C. Fischer}, annote = {}, pages = {5-23}, crossref = {z:z98} } @Proceedings{ z:fitz97, editor = {J. Fitzgerald and C. B. Jones and P. Lucas}, title = {{FME'97}: Industrial Application and Strengthened Foundations of Formal Methods}, booktitle = {FME'97: Industrial Application and Strengthened Foundations of Formal Methods}, series = lncs, volume = 1313, publisher = {Springer-Verlag}, location = {Graz, Austria, September 1997}, isbn = {3-540-63533-5}, year = 1997, organization = {Formal Methods Europe}, annote = {The 4th FME Symposium was held at Graz, Austria, 15--19 September 1997. See the Z-related paper \cite{z:boit97b}.} } @InProceedings{ z:flyn90, author = {M. Flynn and T. Hoverd and D. Brazier}, title = {{Formaliser} -- An Interactive Support Tool for {Z}}, annote = {}, crossref = {z:z90}, pages = {128-141}, year = 1990 } @Article{ z:fogg90, author = {I. Fogg and B. Hicks and A. Lister and T. Mansfield and K. Raymond}, title = {A Comparison of {LOTOS} and {Z} for specifying Distributed Systems}, journal = {Australian Computer Science Communications}, volume = 12, number = 1, pages = {88-96}, month = feb, year = 1990 } @InProceedings{ z:fowl93, author = {D. C. Fowler and P. A. Swatman and P. M. C. Swatman}, title = {Implementing {EDI} in the Public Sector: Including Formality for Enhanced Control}, booktitle = {Proc.\ 7th International Conference on Electronic Data Interchange}, location = {Bled, Slovania}, month = jun, year = 1993 } @InProceedings{ z:fran95, author = {R. B. France and M. M. Larrondo-Petrie}, title = {A Two-Dimensional View of Integrated Formal and Informal Specification Techniques}, pages = {434-448}, annote = {}, crossref = {z:z95} } @InProceedings{ z:fran96, author = {R. B. France and J. Wu and M. M. Larondo-Petrie and J.-M. Bruel}, title = {A Tale of Two Case Studies: Using Integrated Methods to Support Rigorous Requirements Specification}, annote = {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.}, crossref = {z:brya96} } @InProceedings{ z:fran97, author = {R. B. France and J.-M. Bruel}, title = {Integrated Informal Object-Oriented and Formal Modeling Techniques}, annote = {}, length = 4, crossref = {z:bosc97} } @InProceedings{ z:frie95, author = {V. Friesen}, title = {An Exercise in Hybrid System Specification Using an Extension of {Z}}, booktitle = {Proc.\ 2nd European Workshop on Real-Time and Hybrid Systems}, editor = {A. Bouajjani and O. Maler}, year = 1995, pages = {311-316} } @InProceedings{ z:frie98, title = {Object-Oriented Specification of Hybrid Systems using {UML$^h$} and {ZimOO}}, author = {V. Friesen and A. Nordwig and M. Weber}, annote = {}, pages = {328-346}, crossref = {z:z98} } @Article{ z:fuch92, author = {N. E. Fuchs}, title = {Specifications are (Preferably) Executable}, journal = {IEE/BCS Software Engineering Journal}, volume = 7, number = 5, pages = {323-334}, month = sep, year = 1992 } @TechReport{ z:gall96, author = {A. J. Galloway and H. Habrias}, title = {Integrating {NIAM}, {JSD}, {CCS} and {Z}}, institution = {Universit\'e de Nantes, Institut de Recherche en Informatique de Nantes}, address = {France}, type = {Rapport de Recherche}, number = {IRIN - 130}, year = 1996, url = {ftp://ftp.sciences.univ-nantes.fr/pub/info/Habrias/IRIN-130.ps.Z} } @TechReport{ z:gall96b, author = {A. J. Galloway and H. Habrias}, title = {Formalising the Semantics of {GRAFCET} Function Charts using {Z}}, institution = {Universit\'e de Nantes, Institut de Recherche en Informatique de Nantes}, address = {France}, type = {Rapport de Recherche}, number = {IRIN - 131}, year = 1996, url = {ftp://ftp.sciences.univ-nantes.fr/pub/info/Habrias/IRIN-131.ps.Z} } @InProceedings{ z:gard91, author = {P. H. B. Gardiner and P. J. Lupton and J. C. P. Woodcock}, title = {A Simpler Semantics for {Z}}, annote = {}, crossref = {z:z91}, pages = {3-11} } @InProceedings{ z:garl90, author = {D. Garlan and N. Delisle}, title = {Formal Specifications as Reusable Frameworks}, annote = {}, crossref = {z:bjor90}, pages = {150-163} } @Article{ z:garl90b, author = {D. Garlan}, title = {The Role of Reusable Frameworks}, journal = {ACM SIGSOFT Software Engineering Notes}, volume = 15, number = 4, editor = {M. Moriconi}, booktitle = {Proc.\ ACM SIGSOFT International Workshop on Formal Methods in Software Development}, location = {Napa, California, USA, 9--11 May 1990}, publisher = {Association for Computing Machinery}, pages = {42-44}, month = sep, year = 1990, price = {ACM members \$12.00, all others \$15.00}, isbn = {0-89791-415-5} } @InProceedings{ z:garl91, author = {D. Garlan and D. Notkin}, title = {Formalizing Design Spaces: Implicit Invocation Mechanisms}, annote = {}, note = {}, crossref = {z:preh91}, pages = {31-45} } @InProceedings{ z:garl94, author = {D. Garlan}, title = {Integrating Formal Methods into a Professional Master of Software Engineering Program}, pages = {71-85}, annote = {}, crossref = {z:z94}, other = {Invited paper} } @InCollection{ z:garl95, author = {D. Garlan and N. Delisle}, title = {Formal Specification of an Architecture for a Family of Instrumentation Systems}, crossref = {z:hinc95}, pages = {55-72}, annote = {} } @Article{ z:garl95b, author = {D. Garlan}, title = {Making Formal Methods Effective for Professional Software Engineers}, journal = {Information and Software Technology}, volume = 37, number = {5--6}, pages = {261-268}, month = {May--June}, year = 1995, annote = {Revised version of \cite{z:garl94}.} } @Proceedings{ z:gaud96, editor = {M.-C. Gaudel and J. C. P. Woodcock}, title = {{FME'96}: Industrial Benefit and Advances in Formal Methods}, booktitle = {{FME'96}: Industrial Benefit and Advances in Formal Methods}, publisher = {Springer-Verlag}, series = lncs, volume = 1051, organization = {Formal Methods Europe}, location = {Oxford, UK, 18--22 March 1996}, isbn = {3-540-60973-3}, year = 1996, annote = {The 3rd FME Symposium was held at Oxford, UK, 18--22 October 1996. The proceedings includes Z-related papers \cite{z:boit96,z:fidg96,z:kasu96,z:webe96} and B-related papers \cite{z:bica96,z:hoar96,z:wald96}.} } @Article{ z:gerh90, author = {S. L. Gerhart}, title = {Applications of Formal Methods: Developing Virtuoso Software}, journal = {IEEE Software}, volume = 7, number = 5, pages = {6-10}, month = sep, year = 1990, annote = {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 {\em IEEE Transactions on Software Engineering} and {\em IEEE Computer}. See also \cite{z:deli90,z:hall90b,z:nara90,z:spiv90b,z:wing90}.} } @InProceedings{ z:gerh93, author = {S. L. Gerhart and D. Craigen and T. J. Ralston}, title = {Observations on Industrial Practice using Formal Methods}, booktitle = {Proc.\ 15th International Conference on Software Engineering (ICSE), Baltimore, Maryland, USA}, location = {Baltimore, Maryland, USA, May 1993}, month = may, year = 1993 } @Article{ z:gerh94, author = {S. L. Gerhart and D. Craigen and T. J. Ralston}, title = {Experience with Formal Methods in Critical Systems}, journal = {IEEE Software}, volume = 11, number = 1, pages = {21-28}, month = jan, year = 1994, annote = {Several commercial and exploratory cases in which Z features heavily are briefly presented on page 24. See also \cite{z:knig94}.} } @InProceedings{ z:germ95, author = {D. M. Germ\'an and D. D. Cowan}, title = {Experiments with the {Z Interchange Format} and {SGML}}, pages = {224-233}, url = {http://csgwww.uwaterloo.ca/~dmg/research/izum95.ps.gz}, annote = {}, crossref = {z:z95} } @TechReport{ z:gilm91, author = {S. Gilmore}, title = {Correctness-Oriented Approaches to Software Development}, institution = {Department of Computer Science, University of Edinburgh}, address = {Edinburgh EH9 3JZ, UK}, length = 168, number = {ECS-LFCS-91-147 (also CST-76-91)}, price = {\pounds8 (\$16.00)}, year = 1991, annote = {This PhD thesis provides a critical evaluation of Z, VDM and algebraic specifications.}, other = {Copies available from: Dorothy McKie, Laboratory for Foundations of Computer Science, Department of Computer Science, The James Clerk Maxwell Building, The King's Buildings, University of Edinburgh, Edinburgh EH9 3JZ, UK.}, abstract = {This is a PhD thesis providing a critical evaluation of Z, VDM and algebraic specifications. It is centered around the rigorous development of a specification translator with the specifications given in Z, VDM and ASL. Several refinement techniques are used: these range from classical VDM development to an original transformational approach to implementing from a Z specification. Advantages and disadvantages of the approaches are discussed. Also, the correctness and efficiency of the completed implementation are assessed. The implementation is in an imperative programming language and is approximately 10,000 lines long.}, telephone = {+44-31-650-5175} } @InCollection{ z:gims84, author = {R. B. Gimson and C. C. Morgan}, editor = {D. A. Duce}, title = {Ease of Use Through Proper Specification}, booktitle = {Distributed Computing Systems Programme}, publisher = {Peter Peregrinus}, address = {London}, year = 1984 } @TechReport{ z:gims85, author = {R. B. Gimson and C. C. Morgan}, title = {The {Distributed Computing Software} Project}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-50}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-50.html} , length = 85, month = jul, year = 1985, isbn = {0-902928-31-7} } @TechReport{ z:gims87, author = {R. B. Gimson}, title = {The Formal Documentation of a {Block Storage Service}}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-62}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-62.html} , length = 112, month = aug, year = 1987, isbn = {0-902928-44-9} } @TechReport{ z:ginb92, author = {J. Ginbayashi}, title = {Analysis of Business Processes Specified in {Z} against an {E-R} Data Model}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-103}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-103.html} , length = 103, month = dec, year = 1992, isbn = {0-902928-81-3} } @InProceedings{ z:giov90, author = {R. {Di Giovanni} and P. L. Iachini}, title = {{HOOD} and {Z} for the Development of Complex Systems}, annote = {}, crossref = {z:bjor90}, pages = {262-289} } @InProceedings{ z:gonz98, title = {A Symbolic Representation of Transcendental Logic using {Z} Language and its Role in Knowledge Base Systems}, author = {Gonzalez, H. S.}, editor = {F. J. Cantu and R. Soto and J. Liebowitz and E. Sucar}, booktitle = {Proc.\ 4th World Congress of Expert Systems: Application of Advanced Information Technologies}, volume = {1\&2}, year = 1998, pages = {383-387}, publisher = {Scholium International Inc.}, address = {Mexico City}, month = {16--20 March}, comment = {14 Vanderventer Ave, PO Box 1519, Port Washington, NY 11050, USA}, isbn = {1-88-234522-3}, location = {Monterrey, Mexico City, Mexico, 16--20 March 1998} } @InProceedings{ z:good95, author = {H. S. Goodman}, title = {The {Z-into-Haskell} Tool-kit: An Illustrative Case Study}, pages = {374-388}, annote = {}, crossref = {z:z95} } @InProceedings{ z:good95b, author = {H. S. Goodman}, title = {From {Z} Specifications to {Haskell} Programs: A Three-pronged approach}, pages = {167-182}, annote = {}, crossref = {z:habr95} } @Article{ z:good95c, title = {Formalizing Properties of Agents}, author = {Goodwin, R.}, journal = {Journal of Logic and Computation}, year = 1995, volume = 5, number = 6, pages = {763-781}, issn = {0955-792X}, abstract = {There is a wide gulf between the formal logics used by logicians to describe agents and the informal vocabulary used by people who actually build robotic agents. In an effort to help bridge the gap, this paper applies techniques borrowed from the field of formal software methods to develop a common vocabulary. Terms useful for discussing agents are given formal definitions. A framework for describing agents, tasks and environments is developed using the Z specification language. The terms successful, capable, perceptive, predictive, interpretive, rational and sound are then defined relative to this framework. The aims of this paper are to develop a precise, common vocabulary for discussing agents and to provide a basis for rational design of agents.}, keywords = {agents, properties, formalisms, robots} } @InProceedings{ z:gotz90, author = {R. Gotzhein}, title = {Specifying Open Distributed Systems with {Z}}, annote = {}, crossref = {z:bjor90}, pages = {319-339} } @InBook{ z:gras96, author = {W. K. Grassmann and J.-P. Tremblay}, title = {The Formal Specification of Requirements in {Z}}, booktitle = {Logic and Discrete Mathematics}, chapter = 8, pages = {441-480}, publisher = {Prentice Hall}, isbn = {0-13-501206-6}, year = 1996 } @InProceedings{ z:grav90, author = {A. M. Gravell}, title = {Minimisation in Formal Specification and Design}, annote = {}, crossref = {z:z90}, pages = {32-45}, year = 1990 } @InProceedings{ z:grav91, author = {A. M. Gravell}, title = {What is a Good Formal Specification?}, annote = {}, crossref = {z:z91}, pages = {137-150} } @Article{ z:grav95, author = {A. M. Gravell and C. H. Pratten}, title = {Formal Methods and Open Systems}, journal = {Software---Concepts and Tools}, publisher = {Springer-Verlag}, volume = 16, number = 4, pages = {183-188}, year = 1995 } @Article{ z:grav96, author = {A. M. Gravell and P. Henderson}, title = {Executing Formal Specifications need not be Harmful}, journal = {IEE/BCS Software Engineering Journal}, volume = 11, number = 2, pages = {104-110}, month = mar, year = 1996 } @InProceedings{ z:grie95, author = {D. Gries}, title = {Equational Logic: A Great Pedagogical Tool for Teaching a Skill in Logic}, pages = {508-509}, annote = {}, crossref = {z:z95}, other = {Invited paper} } @InProceedings{ z:grim98, title = {Industrial Requirements for the Efficient Development of Reliable Embedded Systems}, author = {K. Grimm}, comment = {Invited speaker.}, note = {Extended abstract}, annote = {}, pages = {1-4}, crossref = {z:z98} } @InBook{ z:habr93, author = {H. Habrias}, title = {Z}, booktitle = {Introduction a la Sp\'ecification}, chapter = 10, pages = {267-290}, publisher = {Masson}, address = {Paris}, series = {M\'ethodologies du Logiciel}, isbn = {2-225-82768-0}, year = 1993 } @Proceedings{ z:habr95, editor = {H. Habrias}, title = {{Z} Twenty Years on -- What is its Future?}, booktitle = {{Z} Twenty Years on -- What is its Future?}, publisher = {IRIN (Institut de Recherche en Informatique de Nantes)}, address = {Universit\'e de Nantes, France}, location = {Nantes, France, 10-12 October 1995}, isbn = {2-225-82768-0}, year = 1995, annote = {Proceedings of the 7th International Conference on {\em Putting into Practice Methods and Tools for Information System Design}, Nantes, France, 10--12 October 1995. This conference considered the future of Z, about twenty years after a seminal paper relating to Z \cite{z:abri74}. See \cite{z:bica95b,z:bros95,z:brue95,z:chau95,z:doch95,z:good95b,% z:hall95b,z:haye95,z:ledr95,z:nguy95,z:park95,z:prat95,z:sinc95,% z:stod95,z:vale95c}.} } @InProceedings{ z:habr95b, author = {Habrias, H. and Dunne, S. and Stoddart, W. J.}, title = {From Natural Language to {Z} Specification}, booktitle = {Proc.\ Conference on Information Systems and Global Competitiveness}, year = 1995, pages = {126-145}, editor = {Labarre, J. E.}, address = {Toronto, Canada}, month = {28--30 September}, publisher = {International Association for Computer Information Systems}, location = {Toronto, Ontario, Canada, 28--30 September 1995} } @InProceedings{ z:hala90, author = {F. Halasz and M. Schwartz}, title = {The {Dexter} Hypertext Reference Model}, booktitle = {Proc.\ {NIST} Hypertext Standardization Workshop}, location = {Gaithersburg, Maryland, USA, January 1990}, address = {Gaithersburg, USA}, month = jan, year = 1990, other = {Frank Halasz is at Xerox PARC, 3333 Coyote Hill Road, Palo Alto, CA 94304, USA, e-mail \verb"halasz@xerox.com". Mayer Schwartz is at Tektronix Laboratories, P. O. Box 500, MS 50-662, Beaverton, OR 97077, USA, e-mail \verb"mayers@tekchips.labs.tek.com".} } @InProceedings{ z:hall88, author = {P. A. V. Hall}, title = {Towards Testing with respect to Formal Specification}, booktitle = {Proc.\ 2nd {IEE}/{BCS} Conference on Software Engineering}, organization = {IEE/BCS}, location = {Liverpool, UK, July 1988}, series = {Conference Publication}, number = 290, pages = {159-163}, month = jul, year = 1988 } @InProceedings{ z:hall90, author = {J. A. Hall}, title = {Using {Z} as a Specification Calculus for Object-Oriented Systems}, annote = {}, crossref = {z:bjor90}, pages = {290-318} } @Article{ z:hall90b, author = {J. A. Hall}, title = {Seven Myths of Formal Methods}, journal = {IEEE Software}, volume = 7, number = 5, pages = {11-19}, month = sep, year = 1990, annote = {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 \cite{z:bowe95c}.} } @InProceedings{ z:hall94, author = {J. A. Hall}, title = {Specifying and Interpreting Class Hierarchies in {Z}}, pages = {120-138}, annote = {}, crossref = {z:z94} } @InProceedings{ z:hall94b, author = {J. G. Hall and J. A. McDermid}, title = {Towards a {Z} Method: Axiomatic Specification in {Z}}, pages = {213-229}, annote = {}, crossref = {z:z94} } @InProceedings{ z:hall95, author = {J. A. Hall and D. L. Parnas and N. Plat and J. Rushby and C. T. Sennett}, title = {The Future of Industrial Formal Methods}, pages = {238-242}, annote = {Position statements for a panel session moderated by T.\ King.}, crossref = {z:z95} } @InProceedings{ z:hall95b, author = {J. G. Hall and J. A. McDermid and I. Toyn}, title = {Model Conjectures for {Z} Specifications}, pages = {41-51}, annote = {}, crossref = {z:habr95} } @InProceedings{ z:hall97, title = {Taking {Z} Seriously}, author = {J. A. Hall}, comment = {Invited speaker}, note = {Extended abstract}, annote = {}, pages = {89-91}, crossref = {z:z97} } @InProceedings{ z:hall97b, title = {{$\cal W$} Reconstructed}, author = {J. Hall and A. Martin}, annote = {}, pages = {116-134}, crossref = {z:z97} } @InCollection{ z:hame95, author = {U. Hamer and J. Peleska}, title = {{Z} Applied to the {A330/340 CICS} Cabin Communication System}, crossref = {z:hinc95}, pages = {253-284}, annote = {} } @InCollection{ z:hami95, author = {V. Hamilton}, title = {The Use of {Z} within a Safety-Critical Software System}, crossref = {z:hinc95}, pages = {357-374}, annote = {} } @InProceedings{ z:hamm94, author = {J. A. R. Hammond}, title = {Producing {Z} Specifications from Object-Oriented Analysis}, pages = {316-336}, annote = {}, crossref = {z:z94} } @InCollection{ z:hamm94b, author = {J. A. R. Hammond}, title = {Z}, editor = {J. J. Marciniak}, booktitle = {Encyclopedia of Software Engineering}, volume = 2, publisher = {John Wiley \& Sons}, pages = {1452-1453}, year = 1994 } @InProceedings{ z:harr92, author = {M. D. Harrison}, title = {Engineering Human-Error Tolerant Software}, annote = {}, crossref = {z:z92}, pages = {191-204} } @Book{ z:harr96, author = {A. Harry}, title = {Formal Methods Fact File: {VDM} and {Z}}, publisher = {John Wiley \& Sons}, isbn = {0-471-94006-2 (hbk) 0-471-95857-3 (pbk)}, year = 1996, annote = {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.} } @InProceedings{ z:hass94, author = {W. Hasselbring}, title = {Animation of {Object-Z} Specifications with a Set-Oriented Prototyping Language}, pages = {337-356}, annote = {}, crossref = {z:z94} } @TechReport{ z:hass94b, author = {W. Hasselbring}, title = {Prototyping Parallel Algorithms in a Set-Oriented Language}, type = {Dissertation}, institution = {Department of Computer Science, University of Dortmund}, address = {Hamburg, Germany}, publisher = {Verlag Dr.\ Kovac}, year = 1994, isbn = {3-86064-202-2}, price = {\pounds34}, length = 205, annote = {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.} } @Article{ z:haug91, author = {H. P. Haughton}, title = {Using {Z} to Model and Analyse Safety and Liveness Properties of Communication Protocols}, journal = {Information and Software Technology}, publisher = {Butterworth-Heinemann}, pages = {575-580}, volume = 33, number = 8, month = oct, year = 1991 } @Article{ z:haye85b, author = {I. J. Hayes}, title = {Applying Formal Specification to Software Development in Industry}, journal = {IEEE Transactions on Software Engineering}, volume = 11, number = 2, pages = {169-178}, month = feb, year = 1985 } @InProceedings{ z:haye86, author = {I. J. Hayes}, title = {Using Mathematics to Specify Software}, booktitle = {Proc.\ First {Australian} Software Engineering Conference}, publisher = {Institution of Engineers, Australia}, location = {Canberra, Australia, May 1986}, month = may, year = 1986 } @Article{ z:haye86b, author = {I. J. Hayes}, title = {Specification Directed Module Testing}, journal = {IEEE Transactions on Software Engineering}, volume = 12, number = 1, pages = {124-133}, month = jan, year = 1986 } @Article{ z:haye89, author = {I. J. Hayes and C. B. Jones}, title = {Specifications are not (Necessarily) Executable}, journal = {IEE/BCS Software Engineering Journal}, volume = 4, number = 6, pages = {330-338}, month = nov, year = 1989 } @InProceedings{ z:haye90b, author = {I. J. Hayes}, title = {A Generalisation of Bags in {Z}}, annote = {}, crossref = {z:z90}, pages = {113-127}, year = 1990 } @InProceedings{ z:haye91, author = {I. J. Hayes}, title = {Interpretations of {Z} Schema Operators}, annote = {}, crossref = {z:z91}, pages = {12-26} } @Article{ z:haye92b, author = {I. J. Hayes}, title = {Multi-relations in {Z}: A cross between multi-sets and binary relations}, journal = {Acta Informatica}, volume = 29, number = 1, pages = {33-62}, month = feb, year = 1992 } @Article{ z:haye92c, author = {I. J. Hayes}, title = {{VDM} and {Z}: A Comparative Case Study}, journal = {Formal Aspects of Computing}, publisher = {Springer-Verlag}, volume = 4, number = 1, pages = {76-99}, year = 1992 } @Book{ z:haye93, editor = {I. J. Hayes}, title = {Specification Case Studies}, publisher = {Prentice Hall International Series in Computer Science}, edition = {2nd}, length = 350, year = 1993, isbn = {13-832544-8}, price = {\pounds21.99 (\$37.00) paperback}, annote = {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 {\em The Z Notation: A Reference Manual} by Mike Spivey \cite{z:spiv92}. The CAVIAR chapter has been extensively changed to make use of a form of modularization. \par 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. \par The other contributors are W.~Flinn, R.~B.\ Gimson, S.~King, C.~C.\ Morgan, I.~H.\ S{\o}rensen and B.~A.\ Sufrin.} } @Article{ z:haye93c, author = {I. J. Hayes and C. B. Jones and J. E. Nicholls}, title = {Understanding the Differences Between {VDM} and {Z}}, journal = {FACS Europe}, volume = {Series I, 1}, number = 1, pages = {7-30}, month = {Autumn}, year = 1993, url = {ftp://ftp.cs.man.ac.uk/pub/TR/UMCS-93-8-1.ps.Z}, annote = {Also available as Technical Report UMCS-93-8-1, Department of Computer Science, University of Manchester, UK, 1993.} } @InProceedings{ z:haye93d, author = {I. J. Hayes and L. Wildman}, title = {Towards Libraries for {Z}}, annote = {}, crossref = {z:z93}, pages = {9-36} } @InProceedings{ z:haye95, author = {I. J. Hayes}, title = {Specification Models}, pages = {1-10}, annote = {}, crossref = {z:habr95}, other = {Invited paper} } @InProceedings{ z:he86, author = {{He Jifeng} and C. A. R. Hoare and J. W. Sanders}, title = {Data Refinement Refined}, booktitle = {Proc.\ {ESOP} 86}, editor = {B. Robinet and R. Wilhelm}, publisher = {Springer-Verlag}, other = {Berlin, Germany}, series = lncs, volume = 213, pages = {187-196}, year = 1986 } @InProceedings{ z:he94, author = {{He Jifeng} and C. A. R. Hoare and M. Fr\"anzle and M. M\"uller-Ulm and E.-R. Olderog and M. Schenke and A. P. Ravn and H. Rischel}, title = {Provably Correct Systems}, editor = {H. Langmaack and W.-P. {de Roever} and J. Vytopil}, booktitle = {Formal Techniques in Real Time and Fault Tolerant Systems}, location = {L\"ubeck, Germany, 19--23 September 1994}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/procos/FTRTFT-tutorial.ps.Z} , publisher = {Springer-Verlag}, series = lncs, volume = 863, pages = {288-335}, year = 1994 } @Book{ z:heat94, author = {D. Heath and D. Allum and L. Dunckley}, title = {Introductory Logic and Formal Methods}, publisher = {A. Waller}, address = {Henley-on-Thames, UK}, isbn = {1-872474-10-1}, price = {\pounds17.95}, year = 1994 } @InProceedings{ z:heit97, title = {Formal Methods: Panacea or Academic Poppycock?}, author = {C. Heitmeyer}, comment = {Invited speaker}, annote = {}, pages = {3-9}, crossref = {z:z97} } @InProceedings{ z:helk97, title = {Automating Test Case Generation from {Z} Specifications with {Isabelle}}, author = {S. Helke and T. Neustupny and T. Santen}, annote = {}, pages = {52-71}, crossref = {z:z97} } @InProceedings{ z:hend98, title = {A Logic for the Schema Calculus}, author = {M. C. Henson and S. Reeves}, annote = {}, pages = {172-191}, crossref = {z:z98} } @InProceedings{ z:henn96, title = {Formal Specification, Object Oriented Design, and Implementation of an Ephemeral Logger for Database Systems}, author = {Hennessey, P. and Ibrahim, M. T. and Fedorec, A. M.}, editor = {R. Wagner and H. Thoma}, booktitle = {Database and Expert System Applications}, series = lncs, publisher = {Springer-Verlag}, year = 1996, volume = 1134, pages = {333-355}, issn = {0302-9743}, abstract = {Recent attempts to relax the ACID rules of transaction processing in order to support Long-Lived Transactions (LLTs) have produced a number of systems which incorporate a meta-transactional framework to store the context of simple atomic transactions. Such a system creates problems for logger design, as a small number of very long transactions can fill the log leading to the premature termination of other transactions. Ephemeral Logging (EL) is a logging algorithm which performs generational garbage collection on the log, thus optimising disk space usage. Its claimed advantage over traditional loggers is most marked in a situation where there are a few long transactions amongst many short ones. This paper describes the formal specification of a transactional logger based on the EL algorithm, its modelling using Object-oriented design(OMT) and implementation. The application of the EL logger to new, emerging applications is also considered. At present the published performance data for this algorithm have been derived using a simulator. This report attempts to examine and scrutinise those results, and asks whether EL could be the logging method of choice in systems that support LLTs.}, keywords = {transaction processing, logging, log manager, ephemeral logging, formal specification, Z, LLT, long-lived transactions, OMT, object design, distributed database systems, log performance} } @InProceedings{ z:hepw90, author = {B. Hepworth}, title = {{ZIP}: A Unification Initiative for {Z} Standards, Methods and Tools}, annote = {}, crossref = {z:z90}, pages = {253-259}, year = 1990 } @InProceedings{ z:hepw91, author = {B. Hepworth and D. Simpson}, title = {The {ZIP} Project}, annote = {}, crossref = {z:z91}, pages = {129-133} } @InProceedings{ z:hewi97, title = {Experiences with {PiZA}, an Animator for {Z}}, author = {M. A. Hewitt and C. M. O'Halloran and C. T. Sennett}, annote = {}, pages = {37-51}, crossref = {z:z97} } @Article{ z:hinc93, author = {M. G. Hinchey}, title = {Formal Methods for System Specification: An ounce of prevention is worth a pound of cure}, journal = {IEEE Potentials Magazine}, volume = 12, number = 3, pages = {50-52}, month = oct, year = 1993 } @Book{ z:hinc95, editor = {M. G. Hinchey and J. P. Bowen}, title = {Applications of Formal Methods}, booktitle = {Applications of Formal Methods}, publisher = {Prentice Hall International Series in Computer Science}, year = 1995, url = {http://www.comlab.ox.ac.uk/archive/formal-methods/afm-book.html} , isbn = {0-13-366949-1}, price = {\pounds32.95 or \$49.95}, length = 452, annote = {A collection on industrial examples of the use of formal methods. Chapters relevant to Z include \cite{z:comb95,z:crai95,z:garl95,z:hame95,z:hami95,z:hinc95b,z:mata95}.} } @InCollection{ z:hinc95b, author = {M. G. Hinchey and J. P. Bowen}, title = {Applications of Formal Methods {FAQ}}, editor = {M. G. Hinchey and J. P. Bowen}, booktitle = {Applications of Formal Methods}, crossref = {z:hinc95}, pages = {1-15}, annote = {} } @InProceedings{ z:hinc96, author = {M. G. Hinchey}, title = {{JSD $\widehat=$ $\Delta$CSP $\oplus$ TLZ} -- A Case Study}, annote = {}, crossref = {z:brya96} } @Proceedings{ z:hinc97, editor = {M. G. Hinchey and Shaoying Liu}, title = {Formal Engineering Methods: Proc.\ 1st International Conference on Formal Engineering Methods (ICFEM'97)}, booktitle = {Formal Engineering Methods}, publisher = {IEEE Computer Society Press}, issn = {0-81-868002-4}, location = {Hiroshima, Japan, 12--14 November 1997}, address = {Hiroshima, Japan}, month = {12--14 November}, year = 1997, annote = {See Z-related papers \cite{z:dinv97e,z:scho97,z:tagu97}.} } @InProceedings{ z:hoar96, author = {J. Hoare and J. Dick and D. Neilson and I. H. S{\o}rensen}, title = {Applying the {B} Technologies to {CICS}}, pages = {74-84}, annote = {}, crossref = {z:gaud96} } @InProceedings{ z:hook96, author = {S. Hooker and M. A. Lockyer and P. C. Fencott}, title = {{CASE} Support for Methods Integration: Implementation of a Translation from a Structured to a Formal Notation}, annote = {The work presented takes the Z specification of the Semantic Function and implements it in the functional programming language, ML.}, crossref = {z:brya96} } @InProceedings{ z:horc95, author = {H.-M. H\"orcher}, title = {Improving Software Tests using {Z} Specifications}, pages = {152-166}, annote = {}, crossref = {z:z95} } @InProceedings{ z:hous91, author = {I. S. C. Houston and S. King}, title = {{CICS} Project Report: Experiences and Results from the Use of {Z} in {IBM}}, annote = {}, note = {}, crossref = {z:preh91}, pages = {588-596} } @Article{ z:hous94, author = {I. S. C. Houston and M. Josephs}, title = {Specifying Distributed {CICS} in {Z}: Accessing Local and Remote Resources (Short Communication)}, journal = {Formal Aspects of Computing}, publisher = {Springer-Verlag}, volume = 6, number = 6, pages = {569-579}, year = 1994 } @Article{ z:hous95, author = {I. S. C. Houston and M. B. Josephs}, title = {A Formal Description of the {OMG}'s {Core Object Model} and the Meaning of Compatible Extension}, journal = {Computer Standards \& Interfaces}, volume = 17, number = {5--6}, pages = {553-558}, month = sep, year = 1995, publisher = {Elsevier Science Publishers (North-Holland)}, issn = {0920-5489}, abstract = {The Object Management Group's Core Object Model provides a standard type structure that must be supported by compliant object-oriented systems (such as IBM's SOM Object Request Broker) and languages (such as C++). The standard is expressed in prose and punctuated by several small examples. The standard also attempts to convey the idea of compatible extensions to the model. The objective of the work reported here was to understand and to communicate the essence of the above standard by use of a formal description technique, the Z notation. In so doing, the meaning of compatibility was clarified. These efforts have been well-received by authors of the original standard.}, keywords = {object-oriented technology, portability, interoperability, object model, compatible extension, formal description, Z notation} } @InProceedings{ z:hugh95, author = {A. P. Hughes and A. A. Donnelly}, title = {An Algebraic Proof in {VDM$^{\clubsuit}$}}, pages = {114-133}, annote = {}, crossref = {z:z95} } @Article{ z:hutc90, author = {A. D. Hutcheon and A. J. Wellings}, title = {Specifying Restrictions on Imperative Programming Languages for use in a Distributed Embedded Environment}, journal = {IEE/BCS Software Engineering Journal}, pages = {93-104}, volume = 5, number = 2, month = mar, year = 1990, abstract = {The authors present a programming language-independent specification of how imperative programming languages can be handled in a distributed environment. These restrictions ensure that processes executing on one machine do not have access to the memory space of processes executing on another.} } @InProceedings{ z:iach91, author = {P. L. Iachini}, title = {Operation Schema Iterations}, annote = {}, crossref = {z:z91}, pages = {50-57} } @Book{ z:impe91, author = {M. Imperato}, title = {An Introduction to {Z}}, publisher = {Chartwell-Bratt}, isbn = {0-86238-289-0}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0862382890}, price = {\pounds9.95, \pound11.95 if delivered outside UK}, length = 190, year = 1991, annote = {Contents: Introduction; Set theory; Logic; Building Z specifications; Relations; Functions; Sequences; Bags; Advanced Z; Case study: a simple banking system.} } @InCollection{ z:ince90, author = {D. C. Ince}, editor = {D. C. Ince and D. Andrews}, title = {{Z} and System Specification}, booktitle = {The Software Life Cycle}, publisher = {Butterworths}, price = {\pounds50}, isbn = {0-408-03741-5}, pages = {260-277}, chapter = 12, year = 1990, other = {In section 3 on {\em Software Engineering and Mathematics}} } @Book{ z:ince93, author = {D. C. Ince}, title = {An Introduction to Discrete Mathematics, Formal System Specification and {Z}}, publisher = {Oxford University Press}, edition = {2nd}, series = {Oxford Applied Mathematics and Computing Science Series}, year = 1993, length = 296, isbn = {0-19-853837-5 or 0-19-853836-7 (pbk)}, price = {\pounds30.00 (hbk) \pounds15.00 (pbk)}, other = {1st edition, 1988} } @InCollection{ z:inmo88, author = {{INMOS Limited.}}, title = {Specification of instruction set \& {Specification} of floating point unit instructions}, booktitle = {{Transputer} Instruction Set -- A compiler writer's guide}, publisher = {Prentice Hall}, pages = {127-161}, year = 1988, isbn = {0-13-929100-8}, length = 167, price = {\pounds19.95 paperback}, telephone = {+44-454-616616, fax: +44-454-617910}, other = {Inmos document number: 72 TRN 199 05. Produced by Inmos Ltd, 1000 Aztec West, Almondsbury, Bristol BS12 4SQ, UK.}, annote = {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.} } @TechReport{ z:iso97, author = {ISO/IEC}, type = {International Standard}, institution = {International Standards Organization}, number = {ISO/IEC DIS 10118-3}, title = {IT -- Security Techniques -- Hash-Functions -- Part 3: Dedicated Hash-Functions}, url = {http://www.iso.ch/cate/d25428.html}, year = 1997, annote = {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.}, abstract = {NPL developed the Z specifications of all the hash functions in the standard while the standard was being developed. This process we believe has produced a very clear and unambiguous standard. The Z specifications have been syntax checked and type checked using commercially available tools. They have also been prototyped in Prolog using a Prolog library developed for Z.}, comment = {To our knowledge this is the first published ISO standard which contains a complete specification in Z. The book {\em Turing's Legacy: A history of computing at the National Physical Laboratory 1945--1995} by Dr.\ D.\ Yates (pub.\ Science Museum, London, 1997) will be given to the first person who can give details of an earlier example.}, other = {Graham Parkin}, email = {Graeme.Parkin@npl.co.uk} } @Article{ z:jack90, author = {J. Jacky}, title = {Formal Specifications for a Clinical Cyclotron Control System}, journal = {ACM SIGSOFT Software Engineering Notes}, volume = 15, number = 4, editor = {M. Moriconi}, booktitle = {Proc.\ ACM SIGSOFT International Workshop on Formal Methods in Software Development}, location = {Napa, California, USA, 9--11 May 1990}, publisher = {Association for Computing Machinery}, pages = {45-54}, month = sep, year = 1990, price = {ACM members \$12.00, all others \$15.00}, isbn = {0-89791-415-5} } @Article{ z:jack92, author = {A. Jack}, title = {It's hard to explain, but {Z} is much clearer than {English}}, journal = {Financial Times}, pages = 22, month = {21 April}, year = 1992 } @InProceedings{ z:jack93, author = {J. Jacky}, title = {Specifying a Safety-Critical Control System in {Z}}, other = {Revised version in \cite{z:jack95}.}, crossref = {z:wood93}, pages = {388-402} } @InProceedings{ z:jack93b, author = {J. Jacky}, title = {Formal Specification and Development of Control System Input/Output}, annote = {}, crossref = {z:z93}, pages = {95-108} } @InProceedings{ z:jack94b, author = {D. Jackson}, title = {Abstract Model Checking of Infinite Specifications}, annote = {}, crossref = {z:naft94}, pages = {519-531} } @Article{ z:jack95, author = {J. Jacky}, title = {Specifying a Safety-Critical Control System in {Z}}, journal = {IEEE Transactions on Software Engineering}, volume = 21, number = 2, pages = {99-106}, month = feb, year = 1995, annote = {Revised version of \cite{z:jack93}.}, issn = {0098-5589}, abstract = {This paper presents a formal specification in the Z notation for a safety-critical control system. It describes a particular medical device but is quite generic and should be widely applicable. The specification emphasizes safety interlocking and other discontinuous features that are not considered in classical control theory. A method for calculating interlock conditions for particular operations from system safety assertions is proposed; it is similar to ordinary Z precondition calculation, but usually results in stronger preconditions. The specification is presented as a partially complete framework that can be edited and filled in with the specific features of a particular control system. Our system is large but the specification is concise. It is built up from components, subsystems, conditions and modes that are developed separately, but also accounts for behaviors that emerge at the system level. The specification illustrates several useful idioms of the Z notation, and demonstrates that an object- oriented specification style can be expressed in ordinary Z.}, keywords = {software requirements, formal specification, process control, safety, medical applications, radiation therapy, cyclotron, Z} } @Article{ z:jack95b, author = {D. Jackson}, title = {Structuring {Z} Specifications with Views}, journal = {ACM Transactions on Software Engineering and Methodology (TOSEM)}, volume = 4, number = 4, pages = {365-389}, month = oct, year = 1995 } @InProceedings{ z:jack95c, author = {J. Jacky and J. Unger}, title = {From {Z} to Code: A Graphical User Interface for a Radiation Therapy Machine}, pages = {315-333}, annote = {}, crossref = {z:z95} } @Article{ z:jack96, author = {D. Jackson and C. A. Damon}, title = {Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector}, journal = {IEEE Transactions on Software Engineering}, volume = 22, number = 7, pages = {484-495}, month = jul, year = 1996, annote = {Nitpick, a specification checker, is applied to the design of a style mechanism for a word processor, using a subset of Z.}, other = {Previously appeared in S.\ J.\ Zeil (editor) {\em Proc.\ 1996 International Symposium on Software testing and Analysis (ISSTA)}, San Diego, California, USA, 8--10 January 1996, {\em ACM Software Engineering Notes}, 21(3):239--249, May 1996.}, issn = {0098-5589}, abstract = {We demonstrate how Nitpick, a specification checker, can be applied to the design of a style mechanism for a word processor. The design is cast, along with some expected properties, in a subset of Z. Nitpick checks a property by enumerating all possible cases within some finite bounds, displaying as a counterexample the first case for which the property fails to hold. Unlike animation or execution tools, Nitpick does not require state transitions to be expressed constructively, and unlike theorem provers, Nitpick operates completely automatically without user intervention. Using a variety of reduction mechanisms, it can cover an enormous number of cases in a reasonable time, so that subtle flaws can be rapidly detected.}, keywords = {specifications, systems, abstract modeling, software design, formal specification, Z notation, model checking, exhaustive testing} } @Article{ z:jack96b, author = {D. Jackson and M. Jackson}, title = {Problem Decomposition for Reuse}, journal = {IEE/BCS Software Engineering Journal}, volume = 11, number = 1, pages = {19-30}, month = jan, year = 1996, annote = {An approach to software development based on the idea of {\em problem frames} and of structuring Z specifications as {\em views}.} } @Book{ z:jack97, author = {J. Jacky}, title = {The Way of {Z}: Practical Programming with Formal Methods}, publisher = {Cambridge University Press}, year = 1997, length = 350, isbn = {0-521-55041-6 (hbk) 0-521-55976-6 (pbk)}, url = {http://www.radonc.washington.edu/prostaff/jon/z-book/}, other = {Contents: Why Z; Introducing Z; Elements of Z; Studies in Z; Programming with Z.} } @InProceedings{ z:jack97b, title = {Experience with {Z} Developing a Control Program for a Radiation Therapy Machine}, author = {J. Jacky and J. Unger and M. Patrick and R. Risler}, comment = {Best paper winner.}, annote = {}, pages = {317-328}, crossref = {z:z97} } @InProceedings{ z:jack98, title = {Modelling a Real-Time Program in {Z}}, author = {J. Jacky}, annote = {}, pages = {136-153}, crossref = {z:z98} } @InProceedings{ z:jaco91, author = {J. Jacob}, title = {The Varieties of Refinements}, editor = {J. M. Morris and R. C. Shaw}, pages = {441-455}, annote = {}, crossref = {z:morr91} } @InProceedings{ z:john87, author = {P. Johnson}, title = {Using {Z} to specify {CICS}}, booktitle = {Proc.\ Software Engineering anniversary meeting ({SEAS})}, other = {SEA}, year = 1987, pages = 303 } @InProceedings{ z:john90, author = {M. Johnson and P. Sanders}, title = {From {Z} Specifications to Functional Implementations}, annote = {}, crossref = {z:z90}, pages = {86-112}, year = 1990 } @Article{ z:john95, author = {C. W. Johnson}, title = {Using {Z} to Support the Design of Interactive Safety-critical Systems}, journal = {IEE/BCS Software Engineering Journal}, volume = 10, number = 2, pages = {49-60}, month = mar, year = 1995 } @InProceedings{ z:john96, author = {D. R. Johnson and H. Kilov}, title = {Can a Flat Notation be used to Specify an {OO} System: using {Z} to describe {RM-ODP} Constraints}, editor = {E. Najm and J.-B. Stefani}, booktitle = {Proc.\ 1st IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems}, pages = {391-398}, location = {Paris, France, March 1996}, publisher = {Chapman \& Hall}, isbn = {0-41279-770-4}, month = mar, year = 1996 } @Article{ z:john96b, title = {Literate Specification: Using Design Rationale to Support Formal Methods in the Development of Human-Machine Interfaces}, author = {Johnson, C. W.}, journal = {Human-Computer Interaction}, year = 1996, volume = 11, number = 4, pages = {291-320}, issn = {0737-0024}, abstract = {The design of safety-critical user interfaces is typically very different from that of many other applications. Reactor control systems and aircraft cockpits are complex and dynamic, open to input from many different users and devices. A number of formal notations, including Z and temporal logic, have been developed to address these problems. They provide precise and concise means of representing a potential design before designers incur the expense of implementation. Consequently, government bodies and commercial organizations have recommended that these techniques be used when tendering for their contracts. However, there are a number of limitations that restrict the use of mathematical specifications for interface development in large scale projects. In particular, formal notations cannot easily be used to coordinate the activities of human factors and systems engineering teams. This creates particular difficulties if some group members have only a limited understanding of discrete mathematics. A further problem is that the development of a safety-critical application may take many months, or even years, to complete. This creates difficulties because abstract mathematical specifications cannot be used easily by new members of a development team to understand past design decisions. To avoid these limitations I have developed a literate approach to interface specification. This technique uses a formal development language and a semiformal design rationale to support the design of safety-critical user interfaces.}, keywords = {safety-critical systems} } @InProceedings{ z:john97, author = {D. R. Johnson and H. Kilov}, title = {An Approach to an {RM-ODP} Toolkit in {Z}}, editor = {G. T. Leavens and M. Sitaraman}, booktitle = {Proc.\ Foundations of Component-based Systems Workshop}, address = {Zurich, Switzerland}, month = {26 September}, year = 1997, organization = {European Software Engineering Conference}, url = {http://www.cs.iastate.edu/~leavens/FoCBS/johnson.html} } @InProceedings{ z:jone91, author = {C. B. Jones}, title = {Interference Revisited}, annote = {}, crossref = {z:z91}, pages = {58-73} } @Article{ z:jone92, author = {R. B. Jones}, title = {{ICL ProofPower}}, journal = {BCS-FACS FACTS}, volume = {Series III, 1}, number = 1, pages = {10-13}, month = {Winter}, year = 1992 } @Proceedings{ z:jone92b, editor = {C. B. Jones and R. C. Shaw and T. Denvir}, title = {5th Refinement Workshop}, booktitle = {5th Refinement Workshop}, other = {BCS-FACS}, publisher = {Springer-Verlag}, series = {Workshop in Computing}, location = {London, UK, 8--10 January 1992}, isbn = {3-540-19752-4}, year = 1992, url = {http://www.dcs.gla.ac.uk/springer-verlag/15.html}, annote = {The workshop was held at Lloyd's Register, London, UK, 8--10 January 1992. See \cite{z:senn92}.} } @InProceedings{ z:jord91, author = {D. Jordan and J. A. McDermid and I. Toyn}, title = {{CADiZ} -- Computer Aided Design in {Z}}, annote = {}, crossref = {z:z91}, pages = {93-104}, other = {See also \cite{z:toyn90}.} } @Article{ z:jose88, author = {M. B. Josephs}, title = {The Data Refinement Calculator for {Z} Specifications}, journal = {Information Processing Letters}, volume = 27, number = 1, pages = {29-33}, year = 1988 } @Article{ z:jose88b, author = {M. B. Josephs}, title = {A State-Based Approach to Communicating Processes}, journal = {Distributed Computing}, publisher = {Springer-Verlag}, volume = 3, pages = {9-18}, year = 1988, annote = {A theoretical paper on combining features of CSP and Z.} } @InProceedings{ z:kasu96, author = {V. Kasurinen and K. Sere}, title = {Integrating Action Systems and {Z} in a Medical System Specification}, pages = {105-119}, annote = {}, crossref = {z:gaud96} } @InProceedings{ z:kasu96b, author = {V. Kasurinen and K. Sere}, title = {Data Modelling in {ZIM}}, annote = {}, crossref = {z:brya96} } @Proceedings{ z:kats93, editor = {T. Katsolakos}, title = {Proc.\ 1993 Software Engineering Standards Symposium (SESS'93)}, booktitle = {Proc.\ 1993 Software Engineering Standards Symposium}, publisher = {IEEE Computer Society Press}, location = {Brighton, UK, 30 August -- 3 September}, address = {Brighton, UK}, month = {30 August -- 3 September}, year = 1993, annote = {See Z-related papers \cite{z:aujl93,z:bowe93h,z:lano93b}.} } @InProceedings{ z:kilo93, author = {H. Kilov}, title = {Information Modeling and {Object Z}: Specifying Generic Reusable Associations}, editor = {O. Etzion and A. Segev}, booktitle = {Proc.\ NGITS-93 (Next Generation Information Technology and Systems)}, location = {Haifa, Israel, 28--30 June 1993}, pages = {182-191}, month = jun, year = 1993, other = {Different kinds of generic relationships (e.g., Dependency, Symmetric Relationship, Composition) have been specified (using invariants and pre- and postconditions for operations) in extended Object-Z.} } @InProceedings{ z:kilo93b, author = {H. Kilov and J. Ross}, title = {Declarative Specifications of Collective Behavior: Generic Reusable Frameworks}, editor = {H. Kilov and W. Harvey}, booktitle = {Proc.\ Workshop on Specification of Behavioral Semantics in Object-Oriented Information Modeling}, location = {Washington DC, USA, 26 September 1993}, organization = {OOPSLA}, other = {Institute for Information Management and Department of Computer and Information Systems, Robert Morris College, Coraopolos and Pittsburgh, Pennsylvania, USA}, address = {Washington DC, USA}, pages = {71-75}, date = {26 September}, year = 1993 } @InCollection{ z:kilo94, author = {H. Kilov and J. Ross}, title = {{Appendix A}: A More Formal Approach}, annote = {}, pages = {199-207}, other = {Uses Object-Z}, crossref = {z:kilo94b} } @Book{ z:kilo94b, author = {H. Kilov and J. Ross}, title = {Information Modeling: An Object-Oriented Approach}, booktitle = {Information Modeling: An Object-Oriented Approach}, publisher = {Prentice Hall}, series = {Object-Oriented Series}, isbn = {0-13-083033-X}, year = 1994 } @TechReport{ z:king88, author = {S. King and I. H. S{\o}rensen and J. C. P. Woodcock}, title = {{Z}: Grammar and Concrete and Abstract Syntaxes}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-68}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-68.html} , length = 48, year = 1988, isbn = {0-902928-50-3} } @InProceedings{ z:king89, author = {S. King and I. H. S{\o}rensen}, title = {Specification and Design of a Library System}, annote = {}, crossref = {z:mcde89} } @InProceedings{ z:king90b, author = {S. King}, title = {{Z} and the Refinement Calculus}, crossref = {z:bjor90}, pages = {164-188}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-79.html} , annote = {Also published as Technical Monograph PRG-79, Oxford University Computing Laboratory, UK, February 1990.} } @Unpublished{ z:king90d, author = {P. King}, title = {Printing {Z} and {Object-Z} {\LaTeX} Documents}, note = {Department of Computer Science, University of Queensland}, address = {St.\ Lucia 4072, Australia}, length = 12, month = may, year = 1990, url = {http://svrc.it.uq.edu.au/Object-Z/pages/latex.html ftp://ftp.comlab.ox.ac.uk/pub/Zforum/oz.ps.Z}, annote = {A description of a Z style option `\verb"oz.sty"', an extended version of Mike Spivey's original `\verb"zed.sty"' \cite{z:spiv90d}, for use with the \LaTeX\ document preparation system \cite{z:lamp93}. It is particularly useful for printing Object-Z documents \cite{z:carr90,z:duke90}.} } @InProceedings{ z:knig93, author = {J. C. Knight and D. M. Kienzle}, title = {Preliminary Experience Using {Z} to Specify a Safety-Critical System}, annote = {}, crossref = {z:z93}, pages = {109-118} } @Article{ z:knig94, author = {J. C. Knight and B. Littlewood}, title = {Critical Task of Writing Dependable Software}, journal = {IEEE Software}, volume = 11, number = 1, pages = {16-20}, month = jan, year = 1994, annote = {Guest editors' introduction to a special issue of {\em IEEE Software} on {\em Safety-Critical Systems}. A short section on formal methods mentions several Z books on page 18. See also \cite{z:gerh94}.} } @InProceedings{ z:knig97, title = {Preliminary Evaluation of a Formal Approach to User Interface Specification}, author = {J. C. Knight and S. S. Brilliant}, annote = {}, pages = {329-346}, crossref = {z:z97} } @InProceedings{ z:knot92, author = {R. D. Knott and P. J. Krause}, title = {The Implementation of {Z} Specifications using Program Transformation Systems: The {SuZan} Project}, editor = {C. Rattray and R. G. Clark}, booktitle = {The Unified Computation Laboratory}, series = {IMA Conference Series}, publisher = {Clarendon Press}, address = {Oxford, UK}, volume = 35, pages = {207-220}, year = 1992 } @InProceedings{ z:kraa95, author = {I. Kraan and P. Baumann}, title = {Implementing {Z} in {Isabelle}}, pages = {355-373}, annote = {}, crossref = {z:z95} } @InProceedings{ z:kraa97, title = {Using the Rippling Heuristic in Set Membership Proofs}, author = {I. Kraan}, annote = {}, pages = {135-147}, crossref = {z:z97} } @Book{ z:lamp93, author = {L. Lamport}, title = {\LaTeX\ User's Guide \& Reference Manual: A document preparation system}, publisher = {Addison-Wesley Publishing Company}, comment = {Reading, Massachusetts}, edition = {2nd}, isbn = {0-201-529831}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0201529831}, length = 242, year = 1993, other = {1st edition, 1986, ISBN 0-201-15790-X}, annote = {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 \verb"fuzz.sty" \cite{z:spiv92b}, \verb"zed.sty" \cite{z:spiv90d} and \verb"oz.sty" \cite{z:king90d}.} } @InProceedings{ z:lamp94, author = {L. Lamport}, title = {{TLZ}}, pages = {267-268}, annote = {}, crossref = {z:z94}, other = {Invited paper}, note = {Abstract} } @InProceedings{ z:lano90, author = {K. C. Lano and P. T. Breuer}, title = {From Programs to {Z} Specifications}, annote = {}, crossref = {z:z90}, pages = {46-70}, year = 1990 } @InProceedings{ z:lano91, author = {K. C. Lano}, title = {{Z$^{++}$}, An Object-orientated Extension to {Z}}, annote = {}, crossref = {z:z91}, pages = {151-172} } @Manual{ z:lano92, author = {K. C. Lano and H. P. Haughton}, title = {The {Z$^{++}$} Manual}, organization = {Lloyd's Register of Shipping}, address = {29 Wellesley Road, Croydon CRO 2AJ, UK}, year = 1992 } @InProceedings{ z:lano92b, author = {K. C. Lano and H. P. Haughton}, title = {Reasoning and Refinement in Object-Oriented Specification Languages}, editor = {O. L. Madsen}, booktitle = {{ECOOP '92}: {European} Conference on Object-Oriented Programming}, publisher = {Springer-Verlag}, series = lncs, volume = 615, pages = {78-97}, location = {Utrecht, The Netherlands, June/July 1992}, year = 1992 } @InProceedings{ z:lano92c, author = {K. C. Lano and H. P. Haughton}, title = {An Algebraic Semantics for the Specification Language {Z$^{++}$}}, booktitle = {Proc.\ Algebraic Methodology and Software Technology Conference (AMAST '91)}, publisher = {Springer-Verlag}, location = {Iowa, USA, May 1991}, year = 1992 } @Article{ z:lano93, author = {K. C. Lano and P. T. Breuer and H. P. Haughton}, title = {Reverse Engineering {COBOL} via Formal Methods}, journal = {Software Maintenance: Research and Practice}, volume = 5, pages = {13-35}, year = 1993, annote = {Also published in a shortened form as Chapter 16 in \cite{z:vanz93}.} } @InProceedings{ z:lano93b, author = {K. C. Lano and H. P. Haughton}, title = {Standards and Techniques for Object-Oriented Formal Specification}, pages = {237-246}, annote = {}, crossref = {z:kats93} } @InProceedings{ z:lano93c, author = {K. C. Lano and H. P. Haughton}, title = {Reuse and Adaptation of {Z} Specifications}, annote = {}, crossref = {z:z93}, pages = {62-90} } @Book{ z:lano93d, editor = {K. C. Lano and H. P. Haughton}, title = {Object Oriented Specification Case Studies}, publisher = {Prentice Hall International}, series = {Object Oriented Series}, year = 1993, annote = {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: \begin{quote} 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. \end{quote} 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.}, length = 240, price = {c\pounds25 UK} } @Book{ z:lano93e, author = {K. C. Lano and H. P. Haughton}, title = {Reverse Engineering and Software Maintenance: A Practical Approach}, publisher = {McGraw Hill}, series = {International Series in Software Engineering}, isbn = {0-07-707897-7}, price = {\pounds29.95}, year = 1993 } @InProceedings{ z:lano94, author = {K. C. Lano}, title = {Refinement in Object-Oriented Specification Languages}, pages = {236-259}, annote = {}, crossref = {z:till94} } @Article{ z:lano95, author = {K. C. Lano and H. P. Haughton}, title = {Formal Development in {B} {Abstract Machine Notation}}, journal = {Information and Software Technology}, volume = 37, number = {5--6}, pages = {303-316}, month = {May--June}, year = 1995 } @InProceedings{ z:lano96, author = {K. C. Lano and S. Goldsack}, title = {Integrated Formal and Object-Oriented Methods: The {VDM$^{++}$} Approach}, annote = {Structure Diagrams are formalized in terms of TLZ \cite{z:lamp94}, 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.}, crossref = {z:brya96} } @InProceedings{ z:lano97, title = {Integrating {VDM++} and Real-Time System Design}, author = {K. C. Lano and S. Goldsack and J. Bicarregui and S. Kent}, annote = {}, pages = {188-219}, crossref = {z:z97} } @InProceedings{ z:lano97b, title = {Specifying Reactive Systems in {B AMN}}, author = {K. C. Lano}, annote = {}, pages = {242-274}, crossref = {z:z97} } @InProceedings{ z:lano98, title = {Compositional Specification of Controllers for Batch Process Operations}, author = {K. C. Lano and P. Kan and A. Sanchez}, annote = {}, pages = {250-264}, crossref = {z:z98} } @Article{ z:layc92, author = {G. Laycock}, title = {Formal Specification and Testing: A Case Study}, journal = {Software Testing, Verification and Reliability}, volume = 2, number = 1, pages = {7-23}, month = may, year = 1992, other = {Constructing test sets from a Z specification.} } @InProceedings{ z:ledr95, author = {Y. Ledru and Y. Chiaramella}, title = {Integrating and Teaching {Z} and {CSP}}, pages = {131-147}, annote = {}, crossref = {z:habr95} } @Article{ z:lee98, title = {A Rule-Based Approach to Producing {Z} Specifications from {Jackson System Development}}, author = {Lee, J. and Pan, J. I.}, journal = {International Journal of Intelligent Systems}, year = 1998, volume = 13, number = 7, pages = {587-611}, issn = {0884-8173}, abstract = {In this paper, we propose a rule-based approach (called JSDZ) to producing Z specifications from Jackson system development (JSD) specifications automatically. In JSDZ, JSP is to serve as the structuring mechanism to help the analysis of problem domains, and Z is to express the formal specifications of JSD artifacts. Several criteria are identified for comparing specifications generated from JSDZ and Z. The bringing together of diagrammatical and text elements of JSD specifications in Z notations offers two major benefits. First, JSD can be seen both as a structuring mechanism that helps in deriving Z specifications, and as a preliminary that assists in ascertaining the clients requirements. Second, Z specifications make it easier to identify omissions or errors.}, keywords = {diagrams} } @InProceedings{ z:leve98, title = {Designing a Requirements Specification Language for Reactive Systems}, author = {N. Leveson}, comment = {Invited speaker.}, note = {Abstract}, annote = {}, pages = 135, crossref = {z:z98} } @Book{ z:ligh91, author = {D. Lightfoot}, title = {Formal Specification using {Z}}, publisher = {Macmillan}, isbn = {0-333-54408-0}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0333544080}, year = 1991, annote = {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.} } @InProceedings{ z:lind94, author = {P. A. Lindsay}, title = {On Transferring {VDM} Verification Techniques to {Z}}, crossref = {z:naft94}, url = {ftp://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr94-10.ps.Z}, annote = {Also available as Technical Report 94-10, Department of Computer Science, University of Queensland, Australia, 1994.}, pages = {190-213} } @InProceedings{ z:lisk95, author = {B. Liskov and J. M. Wing}, title = {Specifications and their Use in Defining Subtypes}, pages = {246-263}, annote = {}, crossref = {z:z95}, other = {Invited paper} } @Article{ z:lond89, author = {R. L. London and K. R. Milsted}, title = {Specifying Reusable Components Using {Z}: Realistic Sets and Dictionaries}, journal = {ACM SIGSOFT Software Engineering Notes}, volume = 14, number = 3, pages = {120-127}, month = may, year = 1989, other = {Presented at the {\em 5th International Workshop on Software Specification and Design}, Pittsburgh, Pennsylvania, 19--20 May 1989. A longer version entitled {\em Specifying and Verifying Reusable Components Using {Z}: Sets and Dictionaries} appeared as Technical Report CR-88-10, Tektronix Laboratories, P. O.~Box 500, MS 50-662, Beaverton, Oregon 97077, USA, October, 1988.} } @InProceedings{ z:love93, author = {M. Love}, title = {Animating {Z} Specifications in {SQL*Forms3.0}}, annote = {}, crossref = {z:z93}, pages = {294-306} } @InProceedings{ z:luck95, author = {M. Luck and M. d'Inverno}, title = {Structuring a {Z} Specification to Provide a Formal Framework for Autonomous Agent Systems}, pages = {47-62}, annote = {}, crossref = {z:z95} } @InProceedings{ z:luck95b, author = {Luck, M. and d'Inverno, M.}, title = {A Formal Framework for Agency and Autonomy}, booktitle = {Proc.\ 1st International Conference on Multi-Agent Systems}, publisher = {AAAI Press / MIT Press}, pages = {254-260}, year = 1995 } @InProceedings{ z:luck96, author = {Luck, M. and d'Inverno, M.}, title = {Engagement and Cooperation in Motivated Agent Modelling}, editor = {Zhang, C. and Lukose, D.}, booktitle = {Distributed Artificial Intelligence Architecture and Modelling: Proc.\ 1st Australian Workshop on Distributed Artificial Intelligence}, series = {Lecture Notes in Artificial Intelligence}, volume = 1087, publisher = {Springer-Verlag}, pages = {70-84}, year = 1996 } @InProceedings{ z:luck97, author = {Luck, M. and Griffiths, N. and d'Inverno, M.}, title = {From Agent Theory to Agent Construction: A Case Study}, booktitle = {Intelligent Agents III: Proc.\ 3rd International Workshop on Agent Theories, Architectures and Languages, Lecture Notes in Artificial Intelligence, 1193}, publisher = {Springer-Verlag}, pages = {49-63}, editor = {M\"uller, J. P. and Wooldridge, M. and Jennings, N.}, year = 1997 } @InProceedings{ z:lupt91, author = {P. J. Lupton}, title = {Promoting Forward Simulation}, annote = {}, crossref = {z:z91}, pages = {27-49} } @InProceedings{ z:luth98, title = {HOL-{Z} in the {UniForM}-Workbench -- A Case Study in Tool Integration for {Z}}, author = {C. L\"uth and E. W. Karlsen and Kolyang and S. Westmeier and B. Wolff}, annote = {}, pages = {116-134}, crossref = {z:z98} } @TechReport{ z:macd91, author = {R. Macdonald}, title = {{Z} Usage and Abusage}, institution = {RSRE, Ministry of Defence}, address = {Malvern, Worcestershire, UK}, type = {Report}, number = {no.\ 91003}, month = feb, year = 1991, annote = {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.}, abstract = {Training courses for Z teach the notation and a number of commonly used techniques for manipulating it. Experience of writing Z specifications and reading those of others leads to the development of other techniques, many of which are passed around informally between Z practitioners, but which are less likely to be written down. 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. The paper assumes a familiarity with the Z notation and the modelling of operations using the state-machine style, including error-handling.} } @InProceedings{ z:macd95, author = {A. MacDonald and D. Carrington}, title = {Structuring {Z} Specifications: Some Choices}, pages = {203-223}, annote = {}, crossref = {z:z95} } @InProceedings{ z:maho91b, author = {B. P. Mahony and I. J. Hayes}, title = {A Case-Study in Timed Refinement: A Central Heater}, pages = {138-149}, annote = {}, crossref = {z:morr91} } @Article{ z:maho92, author = {B. P. Mahony and I. J. Hayes}, title = {A Case-Study in Timed Refinement: A Mine Pump}, journal = {IEEE Transactions on Software Engineering}, volume = 18, number = 9, pages = {817-826}, month = sep, year = 1992 } @InProceedings{ z:maho98, title = {Adding Timed Concurrent Processes to {Object-Z}: A Case Study in {TCOZ}}, author = {B. Mahony and J. S. Dong}, annote = {}, pages = {308-327}, crossref = {z:z98} } @Article{ z:mand95, author = {K. C. Mander and F. Polack}, title = {Rigorous Specification using Structured Systems Analysis and {Z}}, journal = {Information and Software Technology}, volume = 37, number = {5--6}, pages = {285-291}, month = {May--June}, year = 1995, annote = {Revised version of \cite{z:pola94}.} } @InProceedings{ z:mart93, author = {A. Martin}, title = {Encoding {W}: A Logic for {Z} in {2OBJ}}, annote = {}, crossref = {z:wood93}, pages = {462-481} } @PhDThesis{ z:mart95, author = {A. Martin}, title = {Machine-Assisted Theorem-Proving for Software Engineering}, school = oucl, address = oxford, type = {{DPhil} thesis}, year = 1995 } @InProceedings{ z:mata94, author = {P. Mataga and P. Zave}, title = {Formal Specification of Telephone Features}, pages = {29-50}, annote = {}, crossref = {z:z94} } @InCollection{ z:mata95, author = {P. Mataga and P. Zave}, title = {Multiparadigm Specification of an {AT\&T} Switching System}, crossref = {z:hinc95}, pages = {375-398}, annote = {} } @Article{ z:mata95b, author = {P. Mataga and P. Zave}, title = {Using {Z} to Specify Telephone Features}, journal = {Information and Software Technology}, volume = 37, number = {5--6}, pages = {277-283}, month = {May--June}, year = 1995, annote = {Revised version of \cite{z:mata94}.}, issn = {0950-5849}, abstract = {This paper gives a very brief overview of a formal specification of the behaviour of a set of about 10 realistic features for ISDN telephones, The full specification employs a multiparadigm technique in which partial specifications in different languages are composed, but the focus here is on the use of the Z notation to specify call processing and subscriber database aspects of telephone features, Our experiences with the approach, and with Z in particular, are discussed.}, keywords = {formal specification, Z notation, telephony, feature interaction} } @InProceedings{ z:maun93, author = {I. Maung and J. R. Howse}, title = {Introducing {Hyper-Z} -- A New Approach to Object Orientation in {Z}}, annote = {}, crossref = {z:z93}, pages = {149-165} } @InProceedings{ z:may87, author = {M. D. May and D. E. Shepherd}, title = {Verification of the {IMS T800} Microprocessor}, booktitle = {Proc.\ Electronic Design Automation}, pages = {605-615}, address = {London, UK}, month = sep, year = 1987 } @InCollection{ z:may90, author = {M. D. May}, title = {Use of Formal Methods by a Silicon Manufacturer}, editor = {C. A. R. Hoare}, booktitle = {Developments in Concurrency and Communication}, publisher = {Addison-Wesley Publishing Company}, series = {University of Texas at Austin Year of Programming Series}, chapter = 4, pages = {107-129}, year = 1990 } @InCollection{ z:may92, author = {M. D. May and G. Barrett and D. E. Shepherd}, editor = {C. A. R. Hoare and M. J. C. Gordon}, title = {Designing Chips that Work}, booktitle = {Mechanized Reasoning and Hardware Design}, publisher = {Prentice Hall International Series in Computer Science}, pages = {3-19}, year = 1992 } @Proceedings{ z:mcde89, editor = {J. A. McDermid}, title = {The Theory and Practice of Refinement: Approaches to the Formal Development of Large-Scale Software Systems}, booktitle = {The Theory and Practice of Refinement: Approaches to the Formal Development of Large-Scale Software Systems}, publisher = {Butterworth Scientific}, year = 1989, location = {University of York, UK, 7--8 January 1988}, annote = {This book contains papers from the 1st Refinement Workshop held at the University of York, UK, 7--8 January 1988. Z-related papers include \cite{z:king89,z:neil89}.} } @Article{ z:mcde89b, author = {J. A. McDermid}, editor = {J. A. McDermid}, title = {Special section on {Z}}, journal = {IEE/BCS Software Engineering Journal}, volume = 4, number = 1, pages = {25-72}, month = jan, year = 1989, annote = {A special issue on Z, introduced and edited by Prof.\ J. A.\ McDermid. See also \cite{z:bowe89b,z:cohe89,z:spiv89b,z:wood89d}.} } @InCollection{ z:mcde93, author = {J. A. McDermid}, title = {Formal Methods: Use and Relevance for the Development of Safety Critical Systems}, editor = {P. A. Bennett}, booktitle = {Safety Aspects of Computer Control}, publisher = {Butterworth-Heinemann}, address = {Oxford, UK}, isbn = {0-7506-1102-2}, annote = {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.}, year = 1993 } @TechReport{ z:mcmo89, author = {M. A. McMorran and J. E. Nicholls}, title = {{Z} User Manual}, institution = {IBM United Kingdom Laboratories Ltd}, address = {Hursley Park, Winchester, Hampshire SO21 2JN, UK}, type = {Technical Report}, number = {TR12.274}, edition = {Version 1.0}, month = jul, year = 1989 } @Book{ z:mcmo93, author = {M. A. McMorran and S. Powell}, title = {{Z} Guide for Beginners}, publisher = {Blackwell Scientific}, isbn = {0632031174}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0632031174}, year = 1993 } @InProceedings{ z:meir91, author = {S. L. Meira and A. L. C. Cavalcanti}, title = {Modular Object-oriented {Z} Specifications}, annote = {}, crossref = {z:z91}, pages = {173-192} } @Article{ z:meye85, author = {B. Meyer}, title = {On Formalism in Specifications}, journal = {IEEE Software}, volume = 2, number = 1, pages = {6-26}, month = jan, year = 1985 } @InProceedings{ z:mikk95, author = {E. Mikk}, title = {Compilation of {Z} Specifications into {C} for Automatic Test Result Evaluation}, pages = {167-180}, annote = {}, crossref = {z:z95} } @InProceedings{ z:miku95, author = {L. Miku\v{s}iak and V. Vojtek and J. Hasaralejko and J. Hanzelov\'a}, title = {{Z} Browser -- Tool for Visualization of {Z} Specifications}, pages = {510-523}, annote = {}, crossref = {z:z95} } @InProceedings{ z:miku97, author = {L. Miku\v{s}iak and M. Adamy and T. Seidmann}, title = {Publishing Formal Specifications in {Z} Notation on the {WWW}}, editor = {M. Bidoit and M. Dauchet}, booktitle = {TAPSOFT'97: Theory and Practice of Software Development}, publisher = {Springer-Verlag}, volume = 1214, series = lncs, pages = {871-874}, location = {Lille, France}, year = 1997 } @InProceedings{ z:mink95, author = {C. Minkowitz and D. Rann and J. H. Turner}, title = {A {C++} Library for Implementing Specifications}, crossref = {z:wift95}, pages = {61-75} } @Article{ z:misi92, author = {V. B. Mi\v{s}i\'c and D. Vela\v{s}evi\'c and B. Lazarevi\'c}, title = {Formal Specification of a Data Dictionary for an Extended {ER} Data Model}, journal = {The Computer Journal}, volume = 35, number = 6, pages = {611-622}, month = dec, year = 1992 } @InProceedings{ z:misi97, author = {V. B. Mi\v{s}i\'c and S. Moser}, title = {Formal Approach to Metamodeling: A Generic Object-Oriented Perspective}, editor = {D. W. Embley and R. C. Goldstein}, booktitle = {Proc.\ 16th Conference on Conceptual Modeling (ER'97)}, month = nov, year = 1997, pages = {243-256}, address = {Los Angeles, USA}, abstract = {Formal methods and metamodeling are promising ways to cope with the ever increasing size and complexity of modern software systems: the former should provide the means to write precise, unambiguous, and provably consistent descriptions of system properties, while the latter should lead to a better understanding of the software development process through metamodeling the descriptions produced in the course of the software development process. In this paper, we propose to use both formal methods and metamodeling, in order to combine their advantages. A generic metamodel of object-oriented systems is presented and specified, using the Z formal notation. Other known models may easily be mapped to our model, as demonstrated on the OMG core object model. The formal notation facilitates the specification of various constraints and consistency checks, a number of which are shown in detail.} } @Article{ z:misi97b, author = {V. B. Mi\v{s}i\'c and D. Vela\v{s}evi\'c}, title = {Formal Specifications in Software Development: An Overview}, journal = {Yugoslav Journal for Operations Research}, volume = 7, year = 1997, pages = {79-96}, month = jan, number = 1, abstract = {Formal methods find increasing usage for system and software specification. In this paper, we discuss some benefits resulting from the use of such methods, together with some properties shared by most of them. Some possible criteria for classification are also presented, and a tabular overview is given of some of the most well-known methods. A number of known formal methods are reviewed, and their similarities and differences discussed.} } @InProceedings{ z:misi97c, author = {V. B. Mi\v{s}i\'c and S. Moser}, title = {From Formal Metamodels to Metrics: An Object-Oriented Approach}, booktitle = {Proc.\ 24th Conference on Technology of Object-Oriented Languages and Systems (TOOLS Asia)}, editor = {Chen, J. and Li, M. and Mingins, C. and Meyer, B.}, month = sep, year = 1997, pages = {413-422}, address = {Beijing, China}, abstract = {Classical system development techniques often cannot cope with the ever increasing size and complexity of modern software systems. Promising ways to overcome this are formal methods and metamodels: the former should provide the means to write precise, unambiguous, and provably consistent descriptions of system properties, while the latter should lead to a better understanding of the software development process through modeling the process itself. In this paper, we propose to use both formal methods and metamodeling, in order to combine their advantages. A generic metamodel of object-oriented systems is presented, and specified using the Z formal notation. The metamodel is applied towards derivation of complexity metrics, including the well-known Function Point metric, as well as a recently introduced generic measure -- the System Meter. Both applications demonstrate the genericity of the approach.} } @Article{ z:mitc94, title = {Structuring Formal Specifications: A Lesson Relearned}, author = {Mitchell, R. and Loomes, M. and Howse, J.}, journal = {Microprocessors and Microsystems}, year = 1994, volume = 18, number = 10, pages = {593-599}, issn = {0141-9331}, abstract = {Specifications written in the formal specification language Z often make use of a form of decomposition that is novel to programmers. A published Z specification is rewritten using the form of decomposition familiar to programmers. Whenever decomposition is used, there must be some strategy for deciding what is to go in one component and what is to go in another. At the highest level, the strategy underlying the rewritten specification is the well-known strategy of separating user interface issues from deeper system functionality issues. The effectiveness of the strategy is put to a simple test by showing how a modification to the interface can be supported by a modification to only part of the specification. The conclusions drawn are that care over decomposition is important in specifications, just as it is in programs, and that lessons learned from programming about effective decomposition strategies can be applicable at the specification level, too. In particular, the lesson relearned is that it is important to separate information about a system's functionality from information about how this functionality is presented to users.}, keywords = {formal specification, decomposition, modifiability} } @InProceedings{ z:moff91, author = {J. D. Moffett and M. S. Sloman}, title = {A Case Study Representing a Model: To {Z} or not to {Z}?}, annote = {}, crossref = {z:z91}, pages = {254-268} } @Article{ z:mona89, author = {B. Q. Monahan}, title = {Book Review}, journal = {Formal Aspects of Computing}, publisher = {Springer-Verlag}, volume = 1, number = 1, pages = {137-142}, month = {January--March}, year = 1989, annote = {A review of {\em Understanding z: A Specification Language and Its Formal Semantics} by Mike Spivey \cite{z:spiv88b}.} } @InCollection{ z:mona91, author = {B. Q. Monahan and R. C. Shaw}, editor = {J. A. McDermid}, title = {Model-based Specifications}, booktitle = {Software Engineer's Reference Book}, publisher = {Butterworth-Heinemann}, address = {Oxford, UK}, isbn = {0-7506-1014-9}, chapter = 21, year = 1991, price = {\pounds125}, annote = {This chapter contains a case study in Z, followed by a discussion of the respective trade-offs in specification between Z and VDM.} } @Article{ z:morg84, author = {C. C. Morgan and B. A. Sufrin}, title = {Specification of the {Unix} Filing System}, journal = {IEEE Transactions on Software Engineering}, volume = 10, number = 2, pages = {128-142}, month = mar, year = 1984 } @Article{ z:morg87c, author = {C. C. Morgan and K. A. Robinson}, title = {Specification Statements and Refinement}, journal = {IBM Journal of Research and Development}, volume = 31, number = 5, month = sep, year = 1987, other = {Also reprinted in \cite{z:morg88e}.} } @Article{ z:morg88b, author = {C. C. Morgan}, title = {Data Refinement using Miracles}, journal = {Information Processing Letters}, volume = 26, number = 5, pages = {243-246}, month = jan, year = 1988, other = {Also reprinted in \cite{z:morg88e}.} } @Article{ z:morg88c, author = {C. C. Morgan}, title = {The Specification Statement}, journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}, volume = 10, number = 3, month = jul, year = 1988, other = {Also reprinted in \cite{z:morg88e}.} } @Article{ z:morg88d, author = {C. C. Morgan}, title = {Procedures, Parameters, and Abstraction: Separate Concerns}, journal = {Science of Computer Programming}, volume = 11, number = 1, month = oct, year = 1988, other = {Also reprinted in \cite{z:morg88e}.} } @InProceedings{ z:morg89c, author = {C. C. Morgan}, title = {Types and Invariants in the Refinement Calculus}, booktitle = {Proc.\ Mathematics of Program Construction Conference}, address = {Twente, The Netherlands}, location = {Twente, The Netherlands, June 1989}, month = jun, year = 1989 } @TechReport{ z:morg89d, author = {C. C. Morgan and J. W. Sanders}, title = {Laws of the Logical Calculi}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-78}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-78.html} , length = 17, month = sep, year = 1989, isbn = {0-902928-58-9}, annote = {This document records some important laws of classical predicate logic. It is designed as a reservoir to be tapped by {\em users} of logic, in system development.} } @InProceedings{ z:morg90b, author = {C. C. Morgan and J. C. P. Woodcock}, editor = {D. Craigen and K. Summerskill}, title = {What is a Specification?}, booktitle = {Formal Methods for Trustworthy Computer Systems (FM89)}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, isbn = {3-540-19635-8}, chapter = {4.2}, pages = {38-43}, year = 1990, location = {Halifax, Canada, 23--27 July 1989}, other = {Report from FM89: A workshop on the assessment of formal methods for trustworthy computer systems. In chapter 4, `Formal Methods'.} } @Proceedings{ z:morg91, editor = {C. C. Morgan and J. C. P. Woodcock}, title = {3rd Refinement Workshop}, booktitle = {3rd Refinement Workshop}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, other = {BCS-FACS}, isbn = {3-540-19624-2}, url = {http://www.dcs.gla.ac.uk/springer-verlag/48.html}, pages = {151-184}, year = 1991, location = {IBM, Hursley Park, UK, 9--11 January 1990}, annote = {The workshop was held at the IBM Laboratories, Hursley Park, UK, 9--11 January 1990. See \cite{z:senn91}.} } @Book{ z:morg94, editor = {C. C. Morgan and T. Vickers}, title = {On the Refinement Calculus}, publisher = {Springer-Verlag}, series = {Formal Approaches to Computing and Information Technology series (FACIT)}, length = 168, price = {\pounds25 UK}, isbn = {3-540-19809-1}, year = 1994, annote = {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.} } @Book{ z:morg94b, author = {C. C. Morgan}, title = {Programming from Specifications}, publisher = {Prentice Hall International Series in Computer Science}, edition = {2nd}, isbn = {13-12332274-6}, length = 320, year = 1994, annote = {This book presents a rigorous treatment of most elementary program development techniques, including iteration, recursion, procedures, parameters, modules and data refinement.} } @Proceedings{ z:morr91, editor = {J. M. Morris and R. C. Shaw}, title = {4th Refinement Workshop}, booktitle = {4th Refinement Workshop}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, other = {BCS-FACS}, isbn = {3-540-19657-9}, year = 1991, location = {Cambridge, UK, 9--11 January 1991}, url = {http://www.dcs.gla.ac.uk/springer-verlag/49.html}, annote = {The workshop was held at Cambridge, UK, 9--11 January 1991. For Z related papers, see \cite{z:bail91,z:jaco91,z:maho91b,z:wood91b,z:wood91c,z:whys91}.} } @Article{ z:morr98, title = {A Toolset to Support the Construction and Animation of Formal Specifications}, author = {Morrey, I. and Siddiqi, J. and Hibberd, R. and Buckberry, G.}, journal = {Journal of Systems and Software}, year = 1998, volume = 41, number = 3, pages = {147-160}, issn = {0164-1212}, abstract = {Model-based specification languages, in particular Z, have been widely used to provide a precise and unambiguous statement of the proposed system as perceived by the developer. However, for many complex specifications, developers cannot themselves be sure about the ``intended behaviour'' of the specification constructed. This paper reports on an approach and toolset that enables a developer to construct a Z specification using the wiZe editor, demonstrate its properties by transforming it into an executable form using the ZAL animation system, and explore its adequacy by animating a variety of scenarios. The application of the approach and toolset is demonstrated on a specification of a telephone network to illustrate that specification validation could be carried our incrementally during development through investigative scenarios to assess the adequacy of the specification. II is claimed that this interaction, when used in peer review or by the individual developer, can provide enhanced accessibility, a better understood and possibly an improved specification.}, keywords = {Haskell, formal specification, rapid prototyping, animation, validation} } @InProceedings{ z:mose97, author = {S. Moser and V. B. Mi\v{s}i\'c}, title = {Measuring Class Coupling and Cohesion: A Formal Metamodel Approach}, booktitle = {Proc.\ 4th Asia Pacific Software Engineering Conference APSEC'97}, month = dec, year = 1997, address = {Hong Kong}, abstract = {Metamodeling, object-orientation and formal methods are three promising ways to cope with the increasing size and complexity of today's software systems. Furthermore, effective control of development projects requires the use of versatile metrics for software size and complexity. In this paper, we present a generic formal object-oriented metamodel (GM), specifically tailored for modeling object-oriented software systems, and use it as the foundation for defining two basic measures of structural quality: coupling and cohesion. Even though these two notions are generic, we restrict ourselves to defining them at the class level, which is probably the most useful for object-oriented systems. The metrics have a generic formal definition, which makes them simple, intuitive, and amenable to automated measurement.} } @InProceedings{ z:murr98, title = {Formal Derivation of Finite State Machines for Class Testing}, author = {L. Murray and D. Carrington and I. MacColl and J. McDonald and P. Strooper}, annote = {}, pages = {42-59}, crossref = {z:z98} } @Proceedings{ z:naft94, editor = {M. Naftalin and T. Denvir and M. Bertran}, title = {{FME'94}: Industrial Benefit of Formal Methods}, booktitle = {{FME'94}: Industrial Benefit of Formal Methods}, publisher = {Springer-Verlag}, series = lncs, volume = 873, organization = {Formal Methods Europe}, location = {Barcelona, Spain, 24--28 October 1994}, isbn = {3-540-58555-9}, year = 1994, annote = {The 2nd FME Symposium was held at Barcelona, Spain, 24--28 October 1994. Z-related papers include \cite{z:bowe94e,z:cord94,z:deba94,z:evan94b,z:fenc94,z:fidg94b,% z:jack94b,z:lind94,z:ohal94}. B-related papers include \cite{z:dehb94,z:ritc94,z:stor94}.} } @Article{ z:nara90, author = {K. T. Narayana and S. Dharap}, title = {Formal Specification of a Look Manager}, journal = {IEEE Transactions on Software Engineering}, volume = 16, number = 9, pages = {1089-1103}, month = sep, year = 1990, annote = {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.} } @Article{ z:nara90b, author = {K. T. Narayana and S. Dharap}, title = {Invariant Properties in a Dialog System}, journal = {ACM SIGSOFT Software Engineering Notes}, volume = 15, number = 4, editor = {M. Moriconi}, booktitle = {Proc.\ {ACM SIGSOFT} International Workshop on Formal Methods in Software Development}, location = {Napa, California, USA, 9--11 May 1990}, publisher = {Association for Computing Machinery}, pages = {67-79}, month = sep, year = 1990, isbn = {0-89791-415-5}, abstract = {It is possible to specify both liveness and safety properties using Z. In a temporal logic, formulas of the logic are given interpretation on a domain of admissible computations. For a given specification the set of admissible computations constitute the model. Using Z one constructs the admissible computations i.e., the model. Using temporal logic one specifies the properties. Thus temporal logic is higher level than Z for specifying concurrency. More importantly, because model construction in Z (to a great extent) obscures the niceties of Z schema calculus, it is not advisable to use Z for concurrency specification. Actually the use of Z for concurrency description has been reported in this paper.} } @InProceedings{ z:nash90, author = {T. C. Nash}, title = {Using {Z} to Describe Large Systems}, annote = {}, crossref = {z:z90}, pages = {150-178}, year = 1990 } @Article{ z:nehl94, author = {Ph. W. Nehlig and D. A. Duce}, title = {{GKS-9x}: The Design Output Primitive, an Approach to Specification}, booktitle = {Proc.\ {EUROGRAPHICS'94}}, editor = {M. D{\ae}hlen and L. Kjelldahl}, publisher = {Blackwell Publishers}, journal = {Computer Graphics Forum}, volume = 13, number = 3, year = 1994, pages = {C-381-C-392} } @InProceedings{ z:neil89, author = {D. S. Neilson}, title = {Hierarchical Refinement of a {Z} Specification}, annote = {}, crossref = {z:mcde89} } @TechReport{ z:neil90, author = {D. S. Neilson}, title = {From {Z} to {C}: Illustration of a Rigorous Development Method}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-101}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-101.html} , year = 1990, isbn = {0-902928-78-3} } @InProceedings{ z:neil91, author = {D. S. Neilson}, title = {Machine Support for {Z}: The {zedB} Tool}, annote = {}, crossref = {z:z91}, pages = {105-128} } @InProceedings{ z:neil92, author = {D. S. Neilson and D. Prasad}, title = {zed{B}: A Proof Tool for {Z} Built on {B}}, annote = {}, crossref = {z:z92}, pages = {243-258} } @Article{ z:neil98, title = {Lessons from using {Z} to Specify a Software Tool}, author = {Neil, M. and Ostrolenk, G. and Tobin, M. and Southworth, M.}, journal = {IEEE Transactions on Software Engineering}, year = 1998, volume = 24, number = 1, pages = {15-23}, issn = {0098-5589}, abstract = {The authors were recently involved in the development of a COBOL parser, specified formally in Z. The type of problem tackled was well suited to a formal language. The specification process was part of a life-cycle characterized by the front- loading of effort in the specification stage and the inclusion of a statistical testing stage. The specification was found to be error dense and difficult to comprehend. The Z was used to specify inappropriate procedural rather than declarative detail. Modularity and style problems in the Z specification made it difficult to review. In this sense, the application of formal methods was not successful. Despite these problems the estimated fault density for the product was 1.3 faults per KLOC, before delivery, which compares favorably with IBM's Cleanroom method. This was achieved, despite the low quality of the Z specification, through meticulous and effort-intensive reviews. However, because the faults were in critical locations, the reliability of the product was assessed to be unacceptably low. This demonstrates the necessity of assessing reliability as well as ``correctness'' during system testing. Overall, the experiences reported in this paper suggest a range of important lessons for anyone contemplating the practical application of formal methods.}, keywords = {formal methods, statistical testing, practical experience, reliability, fault density} } @InProceedings{ z:nguy95, author = {K. Nguyen and R. Duke}, title = {A Formal Analysis Method for Conceptual Modelling of Information Systems}, pages = {93-110}, annote = {}, crossref = {z:habr95} } @Article{ z:nich87, author = {J. E. Nicholls}, title = {Working with Formal Methods}, journal = {Journal of Information Technology}, volume = 2, number = 2, pages = {67-71}, month = jun, year = 1987, other = {Based on a talk given at a one-day conference at Imperial College, London, UK.} } @TechReport{ z:nich89, author = {J. E. Nicholls and others}, editor = {J. E. Nicholls}, title = {{Z} in the Development Process}, institution = oucl, address = oxford, type = {Technical Report}, number = {PRG-TR-1-89}, length = 54, month = jun, year = 1989, annote = {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.} } @InProceedings{ z:nich91, author = {J. E. Nicholls}, title = {A Survey of {Z} Courses in the {UK}}, booktitle = {{Z} User Workshop, {Oxford} 1990}, annote = {}, crossref = {z:z91}, pages = {343-350} } @InProceedings{ z:nich92, author = {J. E. Nicholls}, title = {Domains of Application for Formal Methods}, booktitle = {{Z} User Workshop, {York} 1991}, annote = {}, crossref = {z:z92}, pages = {145-156} } @InProceedings{ z:nich93, author = {J. E. Nicholls}, title = {Plain Guide to the {Z} Base Standard}, annote = {}, crossref = {z:z93}, pages = {52-61} } @Article{ z:nix88, author = {C. J. Nix and B. P. Collins}, title = {The use of Software Engineering, including the {Z} Notation, in the Development of {CICS}}, journal = {Quality Assurance}, volume = 14, number = 3, pages = {103-110}, month = sep, year = 1988 } @InProceedings{ z:norc91, author = {A. Norcliffe and S. H. Valentine}, title = {A Video-based Training Course in Reading {Z} Specifications}, annote = {}, crossref = {z:z91}, pages = {337-342} } @Book{ z:norc91b, author = {A. Norcliffe and G. Slater}, title = {Mathematics for Software Construction}, publisher = {Ellis Horwood}, series = {Series in Mathematics and its Applications}, isbn = {0-13-563370-2 and 0-13-563388-5}, price = {\pounds25 (Library ed.) and \pounds 13.95 (Student paperback ed.)}, year = 1991, annote = {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.} } @Misc{ z:norc92, author = {A. Norcliffe and S. Valentine}, title = {{Z} Readers Video Course}, howpublished = {PAVIC Publications}, note = {Sheffield Hallam University, 33 Collegiate Crescent, Sheffield S10 2BP, UK}, year = 1992, organization = {Sheffield Hallam University}, annote = {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.}, price = {\pounds995 UK non-education, \pounds495 UK for education. (Multiple copy prices reflect the cost of making additional copies only and are not significantly more expensive.)}, other = {The course is aimed software engineers in industry who wish to take a look at formal methods. It is specifically designed to give skills in {\em reading} Z specifications. The material is also suitable for use in academic institutions where students are to be introduced to Z. \par There are 5 video tapes, each about 1 hour long. The tapes contain material on supporting mathematics followed by a tutorial specification showing the mathematics in action. Each part of the course is accompanied by a booklet containing the specifications discussed on the tapes with annotations. The contents is as follows: \begin{description} \item[1] An introduction to sets. Specifying a (very) simple Security System. \item[2] Functions. Specifying a simple Banking System. \item[3] Sequences. Modelling queues at a petrol filling station. \item[4] Relations. Specifying an e-mail system. \item[5] A review of the Z mathematical tool kit. Three further written specifications to practice reading skills: Modelling Family Relationships; Specifying a Lift (elevator) System; Railway Signalling. \end{description} Formats: VHS(PAL) for UK, Europe, Australia, etc.; VHS(NTSC) for American continent; SECAM for France \& Russia). Other formats could be made available on request. Further details, including free preview material, are also available. For information, please contact: Anthony Meehan, School of Engineering Information Technology, Sheffield Hallam University, Pond Street, Sheffield S1 1WB, UK.} } @InProceedings{ z:norm93, author = {G. Normington}, title = {{Cleanroom} and {Z}}, annote = {}, crossref = {z:z93}, pages = {281-293} } @InProceedings{ z:oakl90, author = {B. Oakley}, title = {The State of Use of Formal Methods}, crossref = {z:z90}, pages = {1-5}, year = 1990, annote = {A record of the opening address at ZUM'89.} } @InProceedings{ z:ohal94, author = {C. {O' Halloran}}, title = {Evaluation Semantics in {Z}}, annote = {}, crossref = {z:naft94}, pages = {502-518} } @InProceedings{ z:olde98, title = {Combining Specification Techniques for Processes, Data and Time}, author = {E.-R. Olderog}, comment = {Invited speaker.}, note = {Abstract}, annote = {}, pages = 192, crossref = {z:z98} } @InProceedings{ z:paig98, title = {Comparing Extended {Z} with a Heterogeneous Notation for Reasoning about Time and Space}, author = {R. Paige}, annote = {}, pages = {214-232}, crossref = {z:z98} } @TechReport{ z:park91, author = {C. E. Parker}, title = {{Z} Tools Catalogue}, institution = {British Aerospace, Software Technology Department}, address = {Warton PR4 1AX, UK}, type = {ZIP project report}, number = {ZIP/BAe/90/020}, month = may, year = 1991 } @InProceedings{ z:park95, author = {H. Parker and F. Polack and K. C. Mander}, title = {The Industrial Trial of {SAZ}: Reflections on the Use of an Integrated Specification Method}, pages = {111-129}, annote = {}, crossref = {z:habr95} } @InProceedings{ z:parn95, author = {D. L. Parnas}, title = {Language-Free Mathematical Models for Software Design}, pages = {3-4}, annote = {}, crossref = {z:z95}, note = {Extended abstract}, other = {Invited paper} } @InProceedings{ z:parn95b, author = {D. L. Parnas}, title = {Teaching Programming as Engineering}, pages = {471-481}, annote = {}, crossref = {z:z95}, other = {Invited paper} } @InProceedings{ z:phil90, author = {M. Phillips}, title = {{CICS/ESA} 3.1 Experiences}, crossref = {z:z90}, pages = {179-185}, year = 1990, annote = {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 {\em total development cost} of the release, based on the reduction of programmer days fixing problems.} } @Article{ z:pill90, author = {M. Pilling and A. Burns and K. Raymond}, title = {Formal Specifications and Proofs of Inheritance Protocols for Real-time Scheduling}, journal = {IEE/BCS Software Engineering Journal}, volume = 5, number = 5, pages = {263-279}, month = sep, year = 1990 } @InProceedings{ z:pola92, author = {F. Polack and M. Whiston and P. Hitchcock}, title = {Structured Analysis -- A Draft Method for Writing {Z} Specifications}, annote = {}, crossref = {z:z92}, pages = {261-286} } @InProceedings{ z:pola93, author = {F. Polack and M. Whiston and K. C. Mander}, title = {The {SAZ} Project: Integrating {SSADM} and {Z}}, annote = {}, crossref = {z:wood93}, pages = {541-557}, abstract = {This paper investigates the rationale for integrating a structured systems analysis method (SSADM version 4) and a formal notation (Z). It describes the integrated specification, and discusses the advantages and disadvantages of formal specification and development for information systems.} } @InProceedings{ z:pola94, author = {F. Polack and K. C. Mander}, title = {Software Quality Assurance using the {SAZ} Method}, pages = {230-249}, annote = {}, crossref = {z:z94} } @InProceedings{ z:pott87, author = {B. F. Potter and D. Till}, title = {The Specification in {Z} of Gateway Functions within a Communications Network}, booktitle = {Proc.\ {IFIP} {WG}10.3 Conference on Distributed Processing}, publisher = {Elsevier Science Publishers (North-Holland)}, url = {http://www.cs.city.ac.uk/bibliography/cs/database?TCU/CS/1987/30} , url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0134787021}, isbn = {0134787021}, month = oct, year = 1987 } @Book{ z:pott96, author = {B. F. Potter and J. E. Sinclair and D. Till}, title = {An Introduction to Formal Specification and {Z}}, publisher = {Prentice Hall International Series in Computer Science}, year = 1996, edition = {2nd}, length = 434, isbn = {0-13-242207-7}, annote = {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.} } @InProceedings{ z:prat95, author = {C. H. Pratten}, title = {An Introduction to Proving {AMN} Specifications with {PVS} and the {AMN-PROOF} Tool}, pages = {149-165}, annote = {}, crossref = {z:habr95} } @Proceedings{ z:preh91, editor = {S. Prehn and W. J. Toetenel}, title = {{VDM'91}: Formal Software Development Methods}, booktitle = {{VDM'91}: Formal Software Development Methods}, publisher = {Springer-Verlag}, series = lncs, volume = 551, location = {Noordwijkerhout, The Netherlands, 21--25 October 1991}, year = 1991, note = {Volume 1: Conference Contributions}, other = {4th VDM-Europe Symposium}, annote = {The 4th VDM-Europe Symposium was held at Noordwijkerhout, The Netherlands, 21--25 October 1991. Papers with relevance to Z include \cite{z:arth91,z:benv91,z:crai91,z:doma91,z:garl91,z:hous91,% z:vanh91,z:wing91,z:zave91}. See also \cite{z:preh91b}.} } @Proceedings{ z:preh91b, editor = {S. Prehn and W. J. Toetenel}, title = {{VDM'91}: Formal Software Development Methods}, booktitle = {{VDM'91}: Formal Software Development Methods}, publisher = {Springer-Verlag}, series = lncs, volume = 552, location = {Noordwijkerhout, The Netherlands, 21--25 October 1991}, year = 1991, note = {Volume 2: Tutorials}, other = {4th VDM-Europe Symposium}, annote = {Papers with relevance to Z include \cite{z:abri91,z:wood91}. See also \cite{z:preh91}.} } @InProceedings{ z:rafs93, author = {G.-H. B. Rafsanjani and S. J. Colwill}, title = {From {Object-Z} to {C$^{++}$}: A Structural Mapping}, annote = {}, crossref = {z:z93}, pages = {166-179} } @InProceedings{ z:rand91, author = {G. P. Randell}, title = {Data Flow Diagrams and {Z}}, annote = {}, crossref = {z:z91}, pages = {216-227} } @Book{ z:rann94, author = {D. Rann and J. Turner and J. Whitworth}, title = {{Z}: A Beginner's Guide}, publisher = {Chapman \& Hall}, address = {London}, isbn = {0-412-55660-X}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?041255660X}, price = {\pounds16.99, paperback}, length = 190, other = {School of Computing, Staffordshire University, UK}, year = 1994 } @Book{ z:ratc94, author = {B. Ratcliff}, title = {Introducing Specification Using {Z}: A Practical Case Study Approach}, publisher = {McGraw-Hill}, series = {International Series in Software Engineering}, isbn = {0077079655}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0077079655}, year = 1994, other = {Inspection copies available from: Alistair Cameron, Marketing Co-ordinator, McGraw-Hill Book Co.\ Ltd, Shoppenhangers Road, Maidenhead, Berkshire SL6 2QL, UK} } @InProceedings{ z:ravn90, author = {A. P. Ravn and H. Rischel and V. Stavridou}, title = {Provably Correct Safety Critical Software}, booktitle = {Proc.\ {IFAC} Safety of Computer Controlled Systems 1990 ({SAFECOMP'90})}, publisher = {Pergamon Press}, comment = {Also available as Technical Report CSD-TR-625, Department of Computer Science, Royal Holloway, University of London, Egham, Surrey TW20 0EX, UK.}, year = 1990 } @InProceedings{ z:raws93, author = {M. Rawson}, title = {{OOPSLA'93}: Workshop on Formal Specification of Object-Oriented Systems -- Position Paper}, editor = {H. Kilov and W. Harvey}, booktitle = {Proc.\ Workshop on Specification of Behavioral Semantics in Object-Oriented Information Modeling}, location = {Washington DC, USA, 26 September 1993}, address = {Washington DC, USA}, organization = {OOPSLA}, comment = {Institute for Information Management and Department of Computer and Information Systems, Robert Morris College, Coraopolos and Pittsburgh, Pennsylvania, USA}, pages = {125-135}, date = {26 September}, year = 1993 } @InProceedings{ z:raws96, author = {M. Rawson and P. Allen}, title = {Synthesis -- An Integrated, Object-Oriented Method and Tool for Requirements Specification in {Z}}, annote = {}, crossref = {z:brya96} } @InProceedings{ z:read91, author = {T. J. Read}, title = {Formal specification of reusable {Ada} software packages}, editor = {A. Burns}, booktitle = {Proc.\ Towards Ada 9X Conference}, pages = {98-117}, year = 1991 } @InProceedings{ z:reed88, author = {J. N. Reed}, title = {Semantics-Based Tools for a Specification Support Environment}, booktitle = {Mathematical Foundations of Programming Language Semantics}, publisher = {Springer-Verlag}, other = {Berlin, Germany}, series = lncs, volume = 298, year = 1988, other = {Presented at the 3rd Workshop on Mathematical Foundations of Programming Language Semantics, 1987.} } @TechReport{ z:reed90, author = {J. N. Reed and J. E. Sinclair}, title = {An Algorithm for Type-Checking {Z}: A {Z} Specification}, institution = oucl, address = oxford, type = {Technical Monograph}, number = {PRG-81}, url = {http://www.comlab.ox.ac.uk/oucl/publications/monos/PRG-81.html} , month = mar, year = 1990, isbn = {0-902928-60-0}, length = 35 } @InProceedings{ z:reil95, author = {C. Reilly}, title = {Exploring Specifications with {Mathematica}}, pages = {408-420}, annote = {}, crossref = {z:z95} } @InProceedings{ z:reiz94, author = {N. R. Reizer and G. D. Abowd and B. C. Meyers and P. R. H. Place}, title = {Using Formal Methods for Requirements Specification of a Proposed {POSIX} Standard}, booktitle = {Proc.\ IEEE International Conference on Requirements Engineering (ICRE'94)}, month = apr, year = 1994, url = {ftp://ftp.sei.cmu.edu/pub/gda/papers/icre94.ps.Z} } @InProceedings{ z:reyn91, author = {G. J. Reynolds}, title = {Yet Another Approach to the Formal Specification of a Configurable Graphics System}, booktitle = {Proc.\ Eurographics Association Formal Methods in Computer Graphics}, location = {Marina di Carrara, Italy, June 1991}, month = jun, year = 1991, other = {Describes an approach to the formal specification of computer graphics systems, using Object-Z.} } @InProceedings{ z:ritc94, author = {B. Ritchie and J. Bicarregui and H. P. Haughton}, title = {Experiences in Using the Abstract Machine Notation in a {GKS} Case Study}, annote = {}, crossref = {z:naft94}, pages = {93-104} } @Book{ z:rlg92, author = {{RAISE Language Group}}, title = {The {RAISE} Specification Language}, publisher = {Prentice Hall International}, series = {BCS Practitioner Series}, year = 1992 } @InProceedings{ z:robi87, author = {K. A. Robinson}, title = {Refining {Z} Specifications to Programs}, booktitle = {Proc.\ {Australian} Software Engineering Conference}, location = {Australia, 1987}, pages = {87-97}, year = 1987 } @InProceedings{ z:rose86, author = {G. A. Rose and P. Robinson}, title = {A Case Study in Formal Specifications}, booktitle = {Proc.\ First {Australian} Software Engineering Conference}, month = may, year = 1986 } @InCollection{ z:rose92, author = {G. A. Rose}, title = {{Object-Z}}, annote = {}, crossref = {z:step92c}, pages = {59-77} } @InProceedings{ z:rudd93, author = {A. R. Ruddle}, title = {Formal Methods in the Specification of Real-Time, Safety-Critical Control Systems}, annote = {}, crossref = {z:z93}, pages = {131-146} } @InProceedings{ z:rudk92, author = {P. Rudkin}, editor = {J. {de Meer}}, title = {Modelling Information Objects in {Z}}, booktitle = {Proc.\ International Workshop on {ODP}}, location = {Berlin, October 1991}, publisher = {Elsevier Science Publishers (North-Holland)}, year = 1992 } @InProceedings{ z:rush95, author = {J. Rushby}, title = {Mechanizing Formal Methods: Challenges and Opportunities}, pages = {105-113}, annote = {}, crossref = {z:z95}, other = {Invited paper} } @InProceedings{ z:saal92, author = {M. Saaltink}, title = {{Z} and {Eves}}, annote = {}, crossref = {z:z92}, pages = {223-242}, url = {http://www.ora.on.ca/biblio.html#mark:z-and-eves http://www.ora.on.ca/biblio.html#mark:z-eves} } @InProceedings{ z:saal97, title = {The {Z/EVES} System}, author = {M. Saaltink}, annote = {}, pages = {72-85}, crossref = {z:z97} } @Article{ z:saie92, author = {H. Saiedian}, title = {Mathematics of Computing}, journal = {Journal of Computer Science Education}, volume = 3, number = 3, pages = {203-221}, year = 1992 } @Article{ z:saie94, author = {H. Saiedian}, title = {Information Systems and the Engineering Paradigm: Integrating the Formal Methods Technology into the Development Process}, journal = {International Journal of Computing and Information Technology}, year = 1994, volume = 2, number = 4, pages = {277-290} } @InProceedings{ z:saie95, author = {H. Saiedian and M. G. Hinchey}, title = {Issues Surrounding the Transferring of Formal Methods Technology into the Actual Workplace}, booktitle = {Proc.\ International Workshop on Formal Methods Application in Software Engineering Practice}, organization = {17th International Conference on Software Engineering}, month = apr, year = 1995, address = {Seattle, USA}, pages = {69-76}, publisher = {IEEE Computer Society Press} } @Article{ z:saie96, author = {H. Saiedian}, title = {An Invitation to Formal Methods}, journal = {IEEE Computer}, year = 1996, volume = 29, number = 4, pages = {16-30}, annote = {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.} } @Article{ z:saie96c, author = {H. Saiedian and M. G. Hinchey}, title = {Challenges in the Successful Transfer of Formal Methods Technology into Industrial Applications}, journal = {Information and Software Technology}, volume = 38, number = 5, month = may, pages = {313-321}, year = 1996 } @InCollection{ z:saie97, author = {H. Saiedian}, title = {Formal Methods in Information Systems Engineering}, editor = {R. Thayer and M. Dorfman}, booktitle = {Software Requirements Engineering}, year = 1997, pages = {336-349}, publisher = {IEEE Computer Society Press}, other = {Los Alamitos, California, USA} } @InCollection{ z:saie97b, author = {H. Saiedian}, title = {Information Systems Design is an Engineering Process}, editor = {A. Kent}, booktitle = {Encyclopedia of Information Science}, volume = 60, year = 1997, publisher = {Marcel Dekker}, address = {New York, USA}, pages = {120-133} } @InProceedings{ z:samp90, author = {A. C. A. Sampaio and S. L. Meira}, title = {Modular Extensions to {Z}}, annote = {}, crossref = {z:bjor90}, pages = {211-232} } @Article{ z:sand89, author = {P. Sanders and M. Johnson and R. Tinker}, title = {From {Z} Specifications to Functional Implementations}, journal = {British Telecom Technology Journal}, volume = 7, number = 4, month = oct, year = 1989 } @InProceedings{ z:sant98, title = {On the Semantic Relation of {Z} and {HOL}}, author = {T. Santen}, annote = {}, pages = {96-115}, crossref = {z:z98} } @InCollection{ z:sche96, author = {M. Schenke and A. P. Ravn}, title = {Refinement from a Control Problem to Programs}, editor = {J.-R. Abrial and E. B\"orger and H. Langmaack}, booktitle = {Formal Methods for Industrial Applications}, annote = {}, crossref = {z:abri96b}, pages = {403-427} } @InProceedings{ z:scho97, title = {Towards a Formal Semantics for an Integrated {SA/RT} \& {Z} Specification Language}, author = {Scholz, D. and Petersohn, C.}, pages = {28-37}, annote = {}, crossref = {z:hinc97} } @InCollection{ z:schu87, author = {S. A. Schuman and D. H. Pitt}, title = {Object-oriented subsystem specification}, editor = {L. G. L. T. Meertens}, booktitle = {Program Specification and Transformation}, publisher = {Elsevier Science Publishers (North-Holland)}, pages = {313-341}, year = 1987, abstract = {The {\em object-oriented} paradigm has proved to be an extremely effective technique for decomposing and reasoning about complex systems. The goal of this paper is to provide a useful counterpart to those facilities at the level of formal specification, using a variant of Z.} } @InCollection{ z:schu90, author = {S. A. Schuman and D. H. Pitt and P. J. Byers}, title = {Object-Oriented Process Specification}, editor = {C. Rattray}, booktitle = {Specification and Verification of Concurrent Systems}, publisher = {Springer-Verlag}, isbn = {3-540-19581-5}, pages = {21-70}, year = 1990 } @InProceedings{ z:semm91, author = {L. T. Semmens and P. M. Allen}, title = {Using {Yourdon} and {Z}: An Approach to Formal Specification}, annote = {}, crossref = {z:z91}, pages = {228-253} } @Article{ z:semm92, author = {L. T. Semmens and R. B. France and T. W. G. Docker}, title = {Integrated Structured Analysis and Formal Specification Techniques}, journal = {The Computer Journal}, volume = 35, number = 6, pages = {600-610}, month = dec, year = 1992 } @InCollection{ z:senn89, author = {C. T. Sennett}, title = {Formal Specification and Implementation}, editor = {C. T. Sennett}, booktitle = {High-Integrity Software}, publisher = {Pitman}, series = {Computer Systems Series}, year = 1989 } @InProceedings{ z:senn91, author = {C. T. Sennett}, title = {Using Refinement to Convince: Lessons Learned from a Case Study}, pages = {172-197}, annote = {}, crossref = {z:morg91} } @InProceedings{ z:senn92, author = {C. T. Sennett}, title = {Demonstrating the Compliance of {Ada} Programs with {Z} Specifications}, annote = {}, crossref = {z:jone92b} } @Article{ z:shep89, author = {D. E. Shepherd and G. Wilson}, title = {Making Chips that Work}, journal = {New Scientist}, volume = 1664, pages = {61-64}, month = may, year = 1989, annote = {A general article containing information on the formal development of the T800 floating-point unit for the Transputer including the use of Z.} } @Article{ z:shep90, author = {D. E. Shepherd}, editor = {H. S. M. Zedan}, title = {Verified Microcode Design}, journal = {Microprocessors and Microsystems}, month = dec, year = 1990, volume = 14, number = 10, pages = {623-630}, abstract = {This article shows how a high-level program in Occam was transformed to a low level implementation that matched the micromachine functions of the T800 Transputer in order to verify its microcode. The high-level specification is first given in Z.}, annote = {This article is part of a special feature on {\em Formal aspects of microprocessor design}, edited by H.~S.~M.\ Zedan. See also \cite{z:bowe90d}.} } @Book{ z:shep95, author = {D. Sheppard}, title = {An Introduction to Formal Specification with {Z} and {VDM}}, publisher = {McGraw Hill}, series = {International Series in Software Engineering}, isbn = {0-07-707907-8}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0077079078}, price = {\pounds19.95, paperback}, length = 398, other = {Department of Computer Studies, University of Glamorgan, UK}, year = 1995 } @InProceedings{ z:sher93, author = {L. B. Sherrell and D. L. Carver}, title = {{Z} meets {Haskell}: A case study}, booktitle = {COMPSAC '93: Proc.\ 17th Annual International Computer Software and Applications Conference}, location = {Phoenix, Arizona, November 1993}, publisher = {IEEE Computer Society Press}, pages = {320-326}, month = nov, year = 1993, annote = {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.} } @Article{ z:sher94, title = {Experiences in Translating {Z} Designs to {Haskell} Implementations}, author = {Sherrell, L. B. and Carver, D. L.}, journal = {Software---Practice and Experience}, year = 1994, volume = 24, number = 12, pages = {1159-1178}, issn = {0038-0644}, abstract = {Z is a widely used, model-oriented specification language. Haskell is a programming language that was recently developed to serve as a standard for non-strict, purely functional languages. Although functional languages have proved to be excellent prototyping tools, Haskell was designed as a general purpose language which could be used when building large software systems. This paper develops two designs for a computerized class roll. The development begins with a description of the requirements and initial specification. The next section delineates the designs and explains how each design targets a specific Haskell data structure: design one employs sequences to model lists, whereas design two uses a Z function to describe a Haskell array. The corresponding implementations follow, along with a critical analysis of each translation from Z notation to flashed code. The paper demonstrates that Z design schemas map well to at least two Haskell data types, namely the list and the array. Furthermore, it includes insights into how software developers might translate similar Z designs to Haskell.}, keywords = {ML, programs, functional programming, formal methods, specification, system design} } @Article{ z:sher95, author = {L. B. Sherrell and D. L. Carver}, title = {{FunZ}: An Intermediate Specification Language}, journal = {The Computer Journal}, year = 1995, volume = 38, number = 3, pages = {193-206}, issn = {0010-4620}, abstract = {During the last few years, the field of software engineering has witnessed an increased interest in formal methods and software reuse. At the same time, functional programming languages, often espoused as rapid prototyping tools, have begun to enjoy more mainstream usage. Assuming that these trends continue, software developers will need improved methods to transform existing specifications into functional implementations. In this paper, we discuss the intermediate specification language FunZ, an integral part of a methodology to produce purely functional programs from Z specifications. To illustrate the concepts of FunZ, we specify the design of a simple software system using both the Z notation and that of FunZ. FunZ itself is best described as an extension of Haskell, yet the language also retains a Z-like flavour in that it contains notational conventions similar to those of standard Z and several object-oriented variants. In addition, software design with FunZ parallels the activity in Z except that each step has functional overtones to better accommodate a final implementation in a purely functional language.}, keywords = {programs, ML} } @Article{ z:shih95, title = {An Operational Semantics Approach to Disciplined Exceptions in Logic Programming}, author = {Shih, T. K. and Lin, F. Y.}, journal = {Computers and Artificial Intelligence}, year = 1995, volume = 14, number = 1, pages = {1-33}, issn = {0232-0274}, abstract = {This paper presents a disciplined exception mechanism based on continuations. Continuations provide mechanisms for labels and jumps. We present a mechanism to preserve a Prolog program continuation to be invoked at a later point. This mechanism is used in the design of exception signals, handlers, and exception continuations for logic programs. An exception continuation specifies how a computation should continue (e.g. resume, undo, alternate, or terminate) after an exception is raised. Short examples illustrate the difficulty of recovering from error conditions in logic programs using traditional control constructs, and show how easily they can be handled using our approach. The Z notation is used to specify the continuation semantics of logic programs with exceptions. Based on the semantic functions, an interpreter written in Prolog is derived to justify our approach.}, keywords = {exceptions, logic programming, operational semantics, continuations} } @Article{ z:shih97, title = {A {Z} Specification Approach to Multimedia Modeling}, author = {Shih, T. K.}, journal = {Computers and Artificial Intelligence}, year = 1997, volume = 16, number = 5, pages = {465-495}, issn = {0232-0274}, abstract = {An interactive multimedia presentation system is introduced. We first define a model for interactive presentations in the Z notation. The model looks at tile presentation from two views: the navigation view and the representation view. The presentation navigation is based on message passing among presentation frames of a presentation, while common information is inherited and shared by frames. The system allows a presenter to plan the audience's reaction in advance. When the audience is watching a presentation, the underlying inference system is learning from his/her responses. This mechanism makes a presentation to be proceeded again act according to the audience's background and knowledge. Thus, the resulting presentation is more diversified. We also propose a multimedia resource database and a number of important resource attributes that we used in the classification of resources. A resource browser is implemented to allow users to preview resources and maintain tile database. The prototype system is implemented under MS Windows. This system can be used for general purpose presentations or demonstrations in different fields such as education, training, product demonstration. and others.}, keywords = {authoring, intelligent multimedia presentation, multimedia database} } @Article{ z:shih97b, title = {Using {Z} to Specify Object-Oriented Software Complexity Measures}, author = {Shih, T. K. and Wang, C. C. and Chung, C. M.}, journal = {Information and Software Technology}, year = 1997, volume = 39, number = 8, pages = {515-529}, issn = {0950-5849}, abstract = {Software metrics have been a key strategy for software engineers to assure software quality and measure software complexity for many years. However, the complexity metrics of object inheritance hierarchies have not yet been carefully studied. This paper proposes an inheritance level-based metric for measuring the object-oriented software complexity of an inheritance hierarchy. We introduce an algorithm which is proved to be complete and sound to decompose an inheritance hierarchy into a number of measured elements, namely, unit repeated inheritances (URIs). We use the Z specification to model the inheritance hierarchy and describe an inheritance level technique (ILT) based on URIs as a guide to measure the inheritance hierarchy. The proposed metric shows that inheritance has a close relation to object-oriented software complexity. The metric also reveals that overuse of repeated (multiple) inheritance will increase software complexity and thus is prone to implicit software errors. The measurement of inheritance metrics is formed based on the proposed mechanism.}, keywords = {software metrics, inheritance hierarchy, unit repeated inheritance, inheritance level technique, Z specification} } @InProceedings{ z:sinc95, author = {J. E. Sinclair and D. C. Ince}, title = {The Use of {Z} in Specifying Securuty Properties}, pages = {27-39}, annote = {}, crossref = {z:habr95} } @InProceedings{ z:sinn94, author = {R. O. Sinnott and K. J. Turner}, title = {Modeling {ODP} Viewpoints}, editor = {H. Kilov and W. Harvey and H. Mili}, booktitle = {Proc.\ Workshop on Precise Behavioral Specifications in Object-Oriented Information Modeling, OOPSLA 1994}, organization = {OOPSLA}, comment = {Robert Morris College, Coraopolos and Pittsburgh, Pennsylvania 15108-1189, USA}, pages = {121-128}, location = {Portland, Oregon, USA, 24 October 1994}, address = {Portland, USA}, month = {24 October}, year = 1994 } @InProceedings{ z:sinn96, author = {R. O. Sinnott and K. J. Turner}, title = {Specifying {ODP} Computational Objects in {Z}}, editor = {E. Najm and J.-B. Stefani}, booktitle = {Proc.\ 1st IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems}, pages = {375-390}, location = {Paris, France, March 1996}, publisher = {Chapman \& Hall}, isbn = {0-41279-770-4}, month = mar, year = 1996 } @InProceedings{ z:sinn96b, author = {R. O. Sinnott and K. J. Turner}, title = {Specifying Multimedia Binding Objects in {Z}}, editor = {O. Spaniol and C. Linnhoff-Popien and B. Meyer}, booktitle = {Trends in Distributed Systems}, publisher = {Springer-Verlag}, series = lncs, volume = 1161, pages = {244-258}, other = {{CORBA} and Beyond}, location = {October 1996}, year = 1996 } @InProceedings{ z:sinn97, author = {R. O. Sinnott and K. J. Turner}, title = {Type Checking in Open Distributed Systems: A Complete Model and its {Z} Specification}, editor = {Rolia, J. and Slonim, J. and Botsford, J.}, booktitle = {Proc.\ IFIP/IEEE International Conference on Open Distributed Processing and Distributed Platforms (ICODP/ICDP)}, month = {26--30 May}, year = 1997, address = {Toronto, Canada}, pages = {85-96}, publisher = {Chapman \& Hall}, isbn = {0-41-281230-4}, location = {Toronto, Ontario, Canada, 26--30 May 1997} } @InProceedings{ z:smit90, author = {A. Smith}, title = {The {Knuth-Bendix} Completion Algorithm and its Specification in {Z}}, annote = {}, crossref = {z:z90}, pages = {195-220}, year = 1990 } @InProceedings{ z:smit90b, author = {G. Smith and R. Duke}, title = {Modelling a Cache Coherence Protocol using {Object-Z}}, booktitle = {Proc.\ 13th Australian Computer Science Conference ({ACSC-13})}, pages = {352-361}, year = 1990 } @InProceedings{ z:smit91, author = {P. Smith and R. Keighley}, title = {The Formal Development of a Secure Transaction Mechanism}, annote = {}, note = {}, crossref = {z:preh91}, pages = {457-476} } @InProceedings{ z:smit92, author = {A. Smith}, title = {On Recursive Free Types in {Z}}, annote = {}, crossref = {z:z92}, pages = {3-39} } @PhDThesis{ z:smit92b, author = {G. Smith}, title = {An Object-Oriented Approach to Formal Specification}, school = {Department of Computer Science, University of Queensland}, address = {St.\ Lucia 4072, Australia}, length = 238, annote = {A detailed description of a version of Object-Z similar to (but not identical to) that in \cite{z:duke91}. The thesis also includes a formalization of temporal logic history invariants and a fully-abstract model of classes in Object-Z.}, url = {ftp://ftp.cs.uq.oz.au/pub/Thesis/graeme_smith.ps.Z}, month = oct, year = 1992 } @InProceedings{ z:smit94, author = {G. Smith}, title = {A Object-Oriented Development Framework for {Z}}, pages = {89-107}, annote = {}, crossref = {z:z94} } @InProceedings{ z:smit95, author = {G. Smith}, title = {Extending {$\cal W$} for {Object-Z}}, pages = {276-295}, annote = {}, crossref = {z:z95} } @Article{ z:smit95b, author = {G. Smith}, title = {A Fully Abstract Semantics of Classes for {Object-Z}}, journal = {Formal Aspects of Computing}, publisher = {Springer-Verlag}, volume = 7, number = 3, pages = {289-313}, year = 1995 } @InBook{ z:somm92, author = {I. Sommerville}, title = {Software Engineering}, chapter = 9, pages = {153-168}, publisher = {Addison-Wesley Publishing Company}, edition = {4th}, isbn = {0-201-56529-3}, year = 1992, annote = {A chapter entitled {\em Model-Based Specification} including examples using Z.} } @InProceedings{ z:sore81, author = {I. H. S{\o}rensen}, editor = {J. Staunstrup}, title = {A Specification Language}, booktitle = {Program Specification: Proceedings of a Workshop}, publisher = {Springer-Verlag}, series = lncs, volume = 134, pages = {381-401}, year = 1981, location = {{\AA}rhus, Denmark, August 1981} } @InProceedings{ z:sore98, title = {Using {B} to Specify, Verify and Design Hardware Circuits}, author = {I. H. S\o{}rensen}, comment = {Invited speaker.}, note = {Extended abstract}, annote = {}, pages = {60-65}, crossref = {z:z98} } @Book{ z:spiv88b, author = {J. M. Spivey}, title = {Understanding {Z}: A Specification Language and its Formal Semantics}, publisher = {Cambridge University Press}, series = {Cambridge Tracts in Theoretical Computer Science}, volume = 3, length = 131, month = jan, year = 1988, isbn = {0-521-33429-2}, annote = {Published version of 1985 DPhil thesis.} } @Article{ z:spiv89b, author = {J. M. Spivey}, title = {An Introduction to {Z} and Formal Specifications}, journal = {IEE/BCS Software Engineering Journal}, volume = 4, number = 1, pages = {40-50}, month = jan, year = 1989 } @InProceedings{ z:spiv90, author = {J. M. Spivey and B. A. Sufrin}, title = {Type Inference in {Z}}, crossref = {z:bjor90}, pages = {426-438}, annote = {Also published as \cite{z:spiv90c}.} } @Article{ z:spiv90b, author = {J. M. Spivey}, title = {Specifying a Real-Time Kernel}, journal = {IEEE Software}, volume = 7, number = 5, pages = {21-28}, month = sep, year = 1990, annote = {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.} } @InProceedings{ z:spiv90c, author = {J. M. Spivey and B. A. Sufrin}, title = {Type Inference in {Z}}, crossref = {z:z90}, pages = {6-31}, year = 1990, annote = {}, other = {Also published as \cite{z:spiv90}.} } @Unpublished{ z:spiv90d, author = {J. M. Spivey}, title = {A Guide to the {\tt zed} Style Option}, note = oucl, address = oxford, length = 14, month = dec, year = 1990, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zguide.ps.Z ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zed.sty}, annote = {A description of the Z style option `\verb"zed.sty"' for use with the \LaTeX\ document preparation system \cite{z:lamp93}. This early and influential style option is now largely superseded by \verb"fuzz.sty" \cite{z:spiv92b}, \verb"oz.sty" \cite{z:king90d} and other style options.}, email = {Mike.Spivey@comlab.ox.ac.uk} } @Book{ z:spiv92, author = {J. M. Spivey}, title = {The {Z} Notation: A Reference Manual}, publisher = {Prentice Hall International Series in Computer Science}, edition = {2nd}, length = 150, year = 1992, isbn = {013-978529-9}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0139785299}, price = {\pounds18.99 (\$32.00) paperback}, annote = {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 \cite{z:brie92}. \par Contents: Tutorial introduction; Background; The Z language; The mathematical tool-kit; Sequential systems; Syntax summary; Changes from the first edition; Glossary.} } @Manual{ z:spiv92b, author = {J. M. Spivey}, title = {The {\large\it f\kern0.1em}{\normalsize\sc uzz} Manual}, organization = {Computing Science Consultancy}, address = {34 Westlands Grove, Stockton Lane, York YO3 0EF, UK}, length = 68, edition = {2nd}, month = jul, year = 1992, price = {\pounds500 (\$1,000) for single user licence, \pounds500 (\$1,000) for academic site licence, \pounds1,500 (\$3,000) for commercial site licence, \pounds5 (\$10) for additional copies of the documentation.}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/fuzz}, annote = {The manual describes a Z type-checker and `\verb"fuzz.sty"' style option for \LaTeX\ documents \cite{z:lamp93}. The package is compatible with the book, {\em The Z Notation: A Reference Manual} by the same author \cite{z:spiv92}.}, other = {Technical enquiries can be sent to Mike Spivey by e-mail at \verb"Mike.Spivey@comlab.ox.ac.uk".} } @Article{ z:spiv96, author = {J. M. Spivey}, title = {The Consistency Theorem for Free Type Definitions in {Z}}, journal = {Formal Aspects of Computing}, publisher = {Springer-Verlag}, volume = 8, pages = {369-375}, year = 1996, other = {Short communication} } @Article{ z:spiv96b, author = {J. M. Spivey}, title = {Richer Types for {Z}}, journal = {Formal Aspects of Computing}, publisher = {Springer-Verlag}, volume = 8, pages = {565-584}, year = 1996 } @Unpublished{ z:steg94, author = {P. Steggles and J. Hulance}, title = {Z Tools Survey}, note = {Imperial Software Technology Ltd. / Formal Systems (Europe) Ltd.}, address = uk, url = {ftp://ftp.ist.co.uk/pub/doc/zola/ztool-survey.ps}, month = jun, year = 1994 } @Article{ z:step87, author = {S. Stepney and S. P. Lord}, title = {Formal Specification of an Access Control System}, journal = {Software---Practice and Experience}, volume = 17, number = 9, pages = {575-593}, month = sep, year = 1987 } @Article{ z:step92b, author = {S. Stepney and R. Barden and D. Cooper}, title = {A Survey of Object Orientation in {Z}}, journal = {IEE/BCS Software Engineering Journal}, volume = 7, number = 2, pages = {150-160}, month = mar, year = 1992 } @Book{ z:step92c, editor = {S. Stepney and R. Barden and D. Cooper}, title = {Object Orientation in {Z}}, booktitle = {Object Orientation in {Z}}, series = {Workshops in Computing}, publisher = {Springer-Verlag}, isbn = {3-540-19778-8 or 0-387-19778-8}, url = {http://www.dcs.gla.ac.uk/springer-verlag/30.html}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?3540197788}, year = 1992, annote = {This is a collection of papers describing various OOZ approaches -- Hall, ZERO, MooZ, Object-Z, OOZE, Schuman \& Pitt, Z$^{++}$, ZEST and Fresco (an object-oriented 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.} } @Book{ z:step93, author = {S. Stepney}, title = {High Integrity Compilation: A Case Study}, publisher = {Prentice Hall}, year = 1993, isbn = {0-13-3810339-9}, annote = {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.} } @Article{ z:step93b, author = {S. Stepney and R. Barden}, title = {Annotated {Z} Bibliography}, journal = {Bulletin of the European Association of Theoretical Computer Science}, volume = 50, pages = {280-313}, month = jun, year = 1993 } @InProceedings{ z:step95, author = {S. Stepney}, title = {Testing as Abstraction}, pages = {137-151}, annote = {}, crossref = {z:z95} } @InProceedings{ z:step98, title = {More Powerful Data Refinement in {Z}}, author = {S. Stepney and D. Cooper and J. C. P. Woodcock}, annote = {}, pages = {284-307}, crossref = {z:z98} } @InProceedings{ z:stoc91, author = {P. Stocks and D. A. Carrington}, title = {Deriving Software Test Cases from Formal Specifications}, booktitle = {6th Australian Software Engineering Conference}, pages = {327-340}, month = jul, year = 1991 } @Article{ z:stoc92, author = {P. Stocks and K. Raymond and D. Carrington and A. Lister}, title = {Modelling Open Distributed Systems in {Z}}, journal = {Computer Communications}, publisher = {Butterworth-Heinemann}, volume = 15, number = 2, pages = {103-113}, month = mar, year = 1992, annote = {In a special issue on the practical use of FDTs (Formal Description Techniques) in communications and distributed systems, edited by Dr.\ Gordon S.\ Blair.} } @InProceedings{ z:stoc93b, author = {P. Stocks and D. A. Carrington}, title = {Test Templates: A Specification-based Testing Framework}, booktitle = {Proc.\ 15th International Conference on Software Engineering}, url = {ftp://ftp.cs.uq.oz.au/pub/TECHREPORTS/department/TR0243.ps.Z} , pages = {405-414}, month = may, year = 1993, annote = {Also available in a longer form as Technical Report UQCS-243, Department of Computer Science, University of Queensland.} } @InProceedings{ z:stoc93c, author = {P. Stocks and D. A. Carrington}, title = {Test Template Framework: A Specification-based Testing Case Study}, booktitle = {Proc.\ International Symposium on Software Testing and Analysis (ISSTA'93)}, url = {ftp://ftp.cs.uq.oz.au/pub/TECHREPORTS/department/TR0255.ps.Z} , pages = {11-18}, month = jun, year = 1993, annote = {Also available in a longer form as Technical Report UQCS-255, Department of Computer Science, University of Queensland.} } @PhDThesis{ z:stoc93d, author = {P. Stocks}, title = {Applying Formal Methods to Software Testing}, school = {Department of Computer Science, University of Queensland}, address = {St.\ Lucia 4072, Australia}, url = {ftp://ftp.cs.uq.oz.au/pub/Thesis/phil_stocks.ps.Z}, year = 1993 } @Article{ z:stoc96, title = {A Framework for Specification-Based Testing}, author = {Stocks, P. and Carrington, D.}, journal = {IEEE Transactions on Software Engineering}, year = 1996, volume = 22, number = 11, pages = {777-793}, issn = {0098-5589}, abstract = {Test templates and a test template framework are introduced as useful concepts in specification-based testing. The framework can be defined using any model-based specification notation and used to derive tests from model-based specifications-in this paper, it is demonstrated using the Z notation. The framework formally defines test data sets and their relation to the operations in a specification and to other test data sets, providing structure to the testing process. Flexibility is preserved, so that many testing strategies can be used. Important application areas of the framework are discussed, including refinement of test data, regression testing, and test oracles.}, keywords = {formal specifications, software, specification-based testing, testing strategies, test data, test oracles, Z notation} } @InProceedings{ z:stod92, author = {W. J. Stoddart and P. Knaggs}, title = {The {Event Calculus} (Formal Specification of Real Time Systems by means of Diagrams and {Z} Schemas)}, booktitle = {Proc.\ 5th International Conference on Putting into Practice Methods and Tools for Information System Design}, organization = {University of Nantes, Institute Universitaire de Technologie}, other = {3 Rue du Mar\'echal Joffre, 44041 Nantes Cedex 01, France}, address = {Nantes, France}, month = sep, year = 1992 } @InProceedings{ z:stod95, author = {W. J. Stoddart and C. Fencott and S. Dunne}, title = {Modelling Hybrid Systems in {Z}}, pages = {11-25}, annote = {}, crossref = {z:habr95} } @InProceedings{ z:stod97, title = {An Introduction to the {Event Calculus}}, author = {W. J. Stoddart}, annote = {}, pages = {10-34}, crossref = {z:z97} } @InProceedings{ z:stod98, title = {The Specification and Refinement of an Environmental Model}, author = {W. J. Stoddart}, annote = {}, pages = {24-41}, crossref = {z:z98} } @InProceedings{ z:stor94, author = {A. C. Storey and H. P. Haughton}, title = {A Strategy for the Production of Verifiable Code Using the {B} Method}, annote = {}, crossref = {z:naft94}, pages = {346-365} } @InProceedings{ z:stru95, author = {B. Strulo}, title = {How Firing Conditions Help Inheritance}, pages = {264-275}, annote = {}, crossref = {z:z95} } @InCollection{ z:sufr82, author = {B. A. Sufrin}, editor = {D. Neel}, title = {Formal System Specification: Notation and Examples}, booktitle = {Tools and Notations for Program Construction}, publisher = {Cambridge University Press}, year = 1982, annote = {An example of a filing system specification, this was the first published use of the schema notation to put together states.} } @Article{ z:sufr84b, author = {B. A. Sufrin}, title = {Towards Formal Specification of the {ICL} Data Dictionary}, journal = {ICL Technical Journal}, month = aug, year = 1984 } @InCollection{ z:sufr86, author = {B. A. Sufrin}, title = {Formal Specification of a Display-oriented Editor}, editor = {N. Gehani and A. D. McGettrick}, booktitle = {Software Specification Techniques}, publisher = {Addison-Wesley Publishing Company}, series = {International Computer Science Series}, price = {\pounds27.95}, length = 477, year = 1986, pages = {223-267}, annote = {Originally published in {\em Science of Computer Programming}, 1:157--202, 1982.} } @InCollection{ z:sufr86b, author = {B. A. Sufrin}, editor = {M. D. Harrison and A. F. Monk}, title = {Formal Methods and the Design of Effective User Interfaces}, booktitle = {People and Computers: Designing for Usability}, publisher = {Cambridge University Press}, year = 1986 } @InProceedings{ z:sufr87, author = {B. A. Sufrin}, title = {A formal framework for classifying interactive information systems}, booktitle = {IEE Colloquium on Formal Methods and Human-Computer Interaction}, publisher = {The Institution of Electrical Engineers}, address = {London, UK}, pages = {4/1-14}, series = {IEE Digest}, number = {09}, location = {London, UK, January 1987}, year = 1987 } @Article{ z:sufr87c, author = {B. A. Sufrin and J. C. P. Woodcock}, title = {Towards the Formal Specification of a Simple Programming Support Environment}, journal = {IEE/BCS Software Engineering Journal}, volume = 2, number = 4, pages = {86-94}, month = jul, year = 1987 } @InCollection{ z:sufr89, author = {B. A. Sufrin}, title = {Effective Industrial Application of Formal Methods}, editor = {G. X. Ritter}, booktitle = {Information Processing 89: Proc.\ 11th {IFIP} Computer Congress}, organization = {IFIP}, publisher = {Elsevier Science Publishers (North-Holland)}, pages = {61-69}, year = 1989, annote = {This paper presents a Z model of the Unix {\em make} utility.} } @InCollection{ z:sufr90, author = {B. A. Sufrin and {He Jifeng}}, title = {Specification, Analysis and Refinement of Interactive Processes}, editor = {M. D. Harrison and H. Thimbleby}, booktitle = {Formal Methods in Human-Computer Interaction}, publisher = {Cambridge University Press}, series = {Cambridge Series on Human-Computer Interaction}, volume = 2, chapter = 6, pages = {153-200}, year = 1990, isbn = {0-521-37202-X}, annote = {A case study on using Z for process modelling.} } @InProceedings{ z:swat91, author = {P. A. Swatman and P. M. C. Swatman and R. Duke}, title = {Electronic Data Interchange: A high-level formal specification in {Object-Z}}, booktitle = {Proc.\ 6th {Australian} Software Engineering Conference ({ASWEC'91})}, location = {Sidney, Australia, July 1991}, address = {Sidney, Australia}, month = jul, year = 1991 } @InProceedings{ z:swat92, author = {P. A. Swatman and D. Fowler and C. Y. M. Gan}, title = {Extending the Useful Application Domain for Formal Methods}, annote = {}, crossref = {z:z92}, pages = {125-144} } @InCollection{ z:swat92b, author = {P. A. Swatman and P. M. C. Swatman}, title = {Is the Information Systems Community Wrong to Ignore Formal Specification Methods?}, editor = {R. Clarke and J. Cameron}, booktitle = {Managing Information Technology's Organisational Impact}, publisher = {Elsevier Science Publishers (North-Holland)}, month = oct, year = 1992 } @InProceedings{ z:swat92c, author = {P. A. Swatman and P. M. C. Swatman}, title = {Managing the Formal Specification of Information Systems}, booktitle = {Proc.\ International Conference on Organization and Information Systems}, location = {Bled, Slovania}, month = sep, year = 1992 } @Article{ z:swat92d, author = {P. A. Swatman and P. M. C. Swatman}, title = {Formal Specification: An Analytic tool for (Management) Information Systems}, journal = {Journal of Information Systems}, volume = 2, number = 2, pages = {121-160}, month = apr, year = 1992 } @PhDThesis{ z:swat92e, author = {P. A. Swatman}, title = {Increasing Formality in the Specification of High-Quality Information Systems in a Commercial Context}, address = {Perth, Western Australia}, school = {Curtin University of Technology, School of Computing}, month = jul, year = 1992 } @InProceedings{ z:swat93, author = {P. A. Swatman}, title = {Using Formal Specification in the Acquisition of Information Systems: Educating Information Systems Professionals}, annote = {}, crossref = {z:z93}, pages = {205-239} } @InProceedings{ z:tagu97, title = {The State-Based {CCS} Semantics for Concurrent {Z} Specification}, author = {Taguchi, K. and Araki, K.}, pages = {283-292}, annote = {}, crossref = {z:hinc97} } @Article{ z:thom90, author = {S. Thompson}, address = {Canterbury, Kent, UK}, title = {Specification Techniques [9004-0316]}, journal = {ACM Computing Reviews}, pages = 213, volume = 31, number = 4, month = apr, year = 1990, annote = {A review of {\em Formal methods applied to a floating-point number system} \cite{z:barr89}.} } @Proceedings{ z:till94, editor = {D. Till}, title = {6th Refinement Workshop}, booktitle = {6th Refinement Workshop}, other = {BCS-FACS}, publisher = {Springer-Verlag}, series = {Workshop in Computing}, location = {London, UK, 5--7 January 1994}, isbn = {3-540-19886-5}, year = 1994, url = {http://www.dcs.gla.ac.uk/springer-verlag/31.html}, annote = {The workshop was held at City University, London, UK, 5--7 January 1994. See \cite{z:fidg94,z:lano94}.} } @Article{ z:todd87, author = {B. S. Todd}, title = {A Model-Based Diagnostic Program}, journal = {IEE/BCS Software Engineering Journal}, volume = 2, number = 3, pages = {54-63}, month = may, year = 1987 } @Article{ z:todd95, title = {A Computer-Based Flowcharting System for Clinical Protocols}, author = {Todd, B. S. and Ledger, W. L.}, journal = {Medical Informatics}, year = 1995, volume = 20, number = 3, pages = {177-198}, issn = {0307-7640}, abstract = {In medicine, scientific and technological developments for investigation and treatment are proceeding al an ever increasing rate. Protocols for patient management are becoming ever more complicated. Rational design and scientific evaluation of protocols requires precise documentation. We propose a notation based on a series of simple flowcharts which describe procedures in increasing derail. Each step in a flowchart is justified by a reasoned argument, possibly including reference to published articles. General correctness requirements of a protocol include, for example, conformity with known indications and contraindications for investigations and treatments. These correctness requirements can be specified declaratively in mathematical logic and justified by reasoned argument. This makes the correspondence between a protocol and its scientific foundation even more explicit. Flowcharts of this nature are more easily created and modified using a personal computer. Furthermore, use of the computer enables a protocol to be checked automatically against its specification for more rapid identification of errors during development and maintenance of the protocol. We present the structured design of our flowcharting system in the `Z' specification language, and we examine the practicality of our approach by means of a case study: the management of infertility. Our flowcharting system may also have application outside medicine where it is necessary to describe formal protocols for complex procedures.}, keywords = {medical-practice guidelines, algorithms, emergency, accident, management, prose, flowchart, clinical algorithm, formal specification, verification} } @InCollection{ z:took86, author = {R. Took}, title = {The Presenter -- A Formal Design for an Autonomous Display Manager}, editor = {I. Sommerville}, booktitle = {Software Engineering Environments}, pages = {151-169}, publisher = {Peter Peregrinus}, address = {London}, year = 1986 } @Article{ z:toyn95, author = {I. Toyn and J. A. McDermid}, title = {{CADiZ}: An Architecture for {Z} Tools and its Implementation}, journal = {Software---Practice and Experience}, volume = 25, number = 3, pages = {305-330}, month = mar, year = 1995 } @InProceedings{ z:toyn96, author = {I. Toyn}, title = {Formal Reasoning in the {Z} Notation using {CADiZ}}, length = 7, url = {ftp://ftp.cs.york.ac.uk/hise_reports/cadiz/uitp.ps.Z}, booktitle = {Proc.\ 2nd Workshop on User Interfaces to Theorem Provers, York}, location = {York, UK, July 1996}, month = jul, year = 1996 } @InProceedings{ z:toyn98, title = {Innovations in Standard {Z} Notation}, author = {I. Toyn}, annote = {}, pages = {193-213}, crossref = {z:z98} } @Article{ z:tray95, author = {O. Traynor and P. Kearney and E. Kazmierczak and {Li Wang} and E. Karlsen}, title = {Extending {Z} with Modules}, note = {Proc.\ ACSC'95}, journal = {Australian Computer Science Communications}, volume = 17, number = 1, year = 1995 } @InProceedings{ z:vale92, author = {S. H. Valentine}, title = {{Z$^{--}$}, an Executable Subset of {Z}}, annote = {}, crossref = {z:z92}, pages = {157-187} } @InProceedings{ z:vale93, author = {S. H. Valentine}, title = {Putting Numbers into the Mathematical Toolkit}, annote = {}, crossref = {z:z93}, pages = {9-36} } @Article{ z:vale95, author = {S. Valentine}, title = {The Programming Language {Z$^{--}$}}, journal = {Information and Software Technology}, volume = 37, number = {5--6}, pages = {293-301}, month = {May--June}, year = 1995 } @InProceedings{ z:vale95b, author = {S. H. Valentine}, title = {Equal Rights for Schemas in {Z}}, pages = {183-202}, annote = {}, crossref = {z:z95} } @InProceedings{ z:vale95c, author = {S. H. Valentine}, title = {An Algebraic Introduction of Real Numbers into {Z}}, pages = {183-204}, annote = {}, crossref = {z:habr95} } @InProceedings{ z:vale98, title = {Inconsistency and Undefinedness in {Z} -- A Practical Guide}, author = {S. H. Valentine}, annote = {}, pages = {233-249}, crossref = {z:z98} } @InProceedings{ z:vanh91, author = {K. M. {van Hee} and L. J. Somers and M. Voorhoeve}, title = {{Z} and High Level {Petri} Nets}, annote = {}, note = {}, crossref = {z:preh91}, pages = {204-219} } @Book{ z:vanz93, editor = {H. J. {van Zuylen}}, title = {The {REDO} Compendium: Reverse Engineering for Software Maintenance}, publisher = {John Wiley \& Sons}, isbn = {0-471-93607-3}, length = 405, year = 1993, annote = {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 \cite{z:lano93}.} } @InProceedings{ z:wald96, author = {M. Wald\'en and K. Sere}, title = {Refining Action Systems with {B}-Tool}, pages = {85-104}, annote = {}, crossref = {z:gaud96} } @InProceedings{ z:webe96, author = {M. Weber}, title = {Combining {Statecharts} and {Z} for the Design of Safety-Critical Control Systems}, pages = {307-326}, annote = {}, crossref = {z:gaud96} } @Article{ z:west92, author = {M. M. West and B. M. Eaglestone}, title = {Software Development: Two approaches to Animation of {Z} Specifications using {Prolog}}, journal = {IEE/BCS Software Engineering Journal}, pages = {264-276}, volume = 7, number = 4, month = jul, year = 1992 } @InProceedings{ z:west95, author = {M. M. West}, title = {Types and Sets in {G\"odel} and {Z}}, pages = {389-407}, annote = {}, crossref = {z:z95} } @InProceedings{ z:weze94, author = {C. D. Wezeman and A. Judge}, title = {{Z} for Managed Objects}, pages = {108-119}, annote = {}, crossref = {z:z94}, url = {http://www.labs.bt.com/bookshop/papers/4885813.htm} } @Article{ z:weze95, author = {C. D. Wezeman}, title = {Using {Z} for Network Modelling: An Industrial Experience Report}, journal = {Computer Standards \& Interfaces}, volume = 17, number = {5--6}, pages = {631-638}, month = sep, year = 1995, publisher = {Elsevier Science Publishers (North-Holland)}, url = {http://www.labs.bt.com/bookshop/papers/5090608.htm} } @InProceedings{ z:whit90, author = {R. W. Whitty}, title = {Structural Metrics for {Z} Specifications}, annote = {}, crossref = {z:z90}, pages = {186-191}, year = 1990 } @InProceedings{ z:whys91, author = {P. J. Whysall and J. A. McDermid}, title = {Object-Oriented Specification and Refinement}, pages = {151-184}, annote = {}, crossref = {z:morr91} } @InProceedings{ z:whys91b, author = {P. J. Whysall and J. A. McDermid}, title = {An Approach to Object-oriented Specification using {Z}}, annote = {}, crossref = {z:z91}, pages = {193-215} } @Proceedings{ z:wift95, editor = {R. B. France and S. L. Gerhart}, title = {Proc.\ {Workshop on Industrial-strength Formal Specification Techniques}}, booktitle = {Proc.\ {Workshop on Industrial-strength Formal Specification Techniques}}, publisher = {IEEE Computer Society Press}, length = {172 + viii}, other = {WIFT'95}, location = {Boca Raton, Florida, USA, 5-7 April 1995}, isbn = {0-8186-7005-3 (paper), 0-7803-2529-X (fiche)}, year = 1995 } @Article{ z:wing90, author = {J. M. Wing}, title = {A Specifier's Introduction to Formal Methods}, journal = {IEEE Computer}, year = 1990, month = sep, volume = 23, number = 9, pages = {8-24} } @InProceedings{ z:wing91, author = {J. M. Wing and A. M. Zaremski}, title = {Unintrusive Ways to Integrate Formal Specifications in Practice}, annote = {}, note = {}, crossref = {z:preh91}, pages = {545-570} } @InProceedings{ z:wing95, author = {J. M. Wing}, title = {Hints for Writing Specifications}, pages = 497, annote = {}, crossref = {z:z95}, other = {Invited paper} } @Article{ z:wood88b, author = {J. C. P. Woodcock}, title = {Teaching How to Use Mathematics for Large-Scale Software Development}, journal = {Bulletin of BCS-FACS}, month = jul, year = 1988 } @Book{ z:wood88c, author = {J. C. P. Woodcock and M. Loomes}, title = {Software Engineering Mathematics: Formal Methods Demystified}, publisher = {Pitman}, length = 291, year = 1988, isbn = {0-27-302673-9}, url = {http://heg-school.aw.com/cseng/authors/woodcock/software/software.html} , price = {\pounds10.95, paperback}, annote = {Also published as: {\em Software Engineering Mathematics}, Addison-Wesley, 1989.} } @Article{ z:wood89, author = {J. C. P. Woodcock}, title = {Calculating Properties of {Z} Specifications}, journal = {ACM SIGSOFT Software Engineering Notes}, volume = 14, number = 4, pages = {43-54}, year = 1989 } @Article{ z:wood89d, author = {J. C. P. Woodcock}, title = {Structuring Specifications in {Z}}, journal = {IEE/BCS Software Engineering Journal}, volume = 4, number = 1, pages = {51-66}, month = jan, year = 1989 } @InProceedings{ z:wood89g, author = {J. C. P. Woodcock}, title = {Mathematics as a Management Tool: Proof Rules for Promotion}, booktitle = {Proc.\ 6th Annual {CSR} Conference on Large Software Systems}, address = {Bristol, UK}, location = {Bristol, UK, September 1989}, month = sep, year = 1989 } @InProceedings{ z:wood90, author = {J. C. P. Woodcock and C. C. Morgan}, title = {Refinement of State-Based Concurrent Systems}, crossref = {z:bjor90}, pages = {340-351}, annote = {Work on combining Z and CSP.} } @InProceedings{ z:wood90b, author = {J. C. P. Woodcock}, editor = {D. Craigen and K. Summerskill}, title = {{Z}}, booktitle = {Formal Methods for Trustworthy Computer Systems (FM89)}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, isbn = {3-540-19635-8}, chapter = {4.9}, pages = {57-62}, year = 1990, location = {Halifax, Canada, 23--27 July 1989}, other = {Report from FM89: A workshop on the assessment of formal methods for trustworthy computer systems. In chapter 4, `Formal Methods'.} } @Article{ z:wood90c, author = {W. G. Wood}, title = {Application of Formal Methods to System and Software Specification}, journal = {ACM SIGSOFT Software Engineering Notes}, volume = 15, number = 4, editor = {M. Moriconi}, booktitle = {Proc.\ {ACM SIGSOFT} International Workshop on Formal Methods in Software Development}, location = {Napa, California, USA, 9--11 May 1990}, publisher = {Association for Computing Machinery}, pages = {144-146}, month = sep, year = 1990, isbn = {0-89791-415-5} } @InProceedings{ z:wood91, author = {J. C. P. Woodcock}, title = {A Tutorial on the Refinement Calculus}, annote = {}, note = {}, crossref = {z:preh91b}, pages = {79-140} } @InProceedings{ z:wood91b, author = {K. R. Wood}, title = {The Elusive Software Refinery: a Case Study in Program Development}, pages = {281-325}, annote = {}, crossref = {z:morr91} } @InProceedings{ z:wood91c, author = {J. C. P. Woodcock}, title = {Implementing Promoted Operations in {Z}}, pages = {366-378}, annote = {}, crossref = {z:morr91} } @InProceedings{ z:wood92, author = {J. C. P. Woodcock and S. M. Brien}, title = {{$\cal W$}: A Logic for {Z}}, annote = {}, crossref = {z:z92}, pages = {77-96} } @Article{ z:wood92b, author = {J. C. P. Woodcock}, title = {The Rudiments of Algorithm Design}, journal = {The Computer Journal}, volume = 35, number = 5, pages = {441-450}, month = oct, year = 1992 } @Proceedings{ z:wood93, editor = {J. C. P. Woodcock and P. G. Larsen}, title = {{FME'93}: Industrial-Strength Formal Methods}, booktitle = {{FME'93}: Industrial-Strength Formal Methods}, organization = {Formal Methods Europe}, location = {Odense, Denmark, 19--23 April 1993}, publisher = {Springer-Verlag}, series = lncs, volume = 670, isbn = {3-540-56662-7}, year = 1993, annote = {The 1st FME Symposium was held at Odense, Denmark, 19--23 April 1993. Z-related papers include \cite{z:bowe93g,z:crai93b,z:fidg93,z:jack93,z:mart93,z:pola93}.} } @Article{ z:wood93b, author = {K. R. Wood}, title = {A practical approach to software engineering using {Z} and the refinement calculus}, booktitle = {Proc.\ SIGSOFT'93 Symposium on the Foundations of Software Engineering}, journal = {ACM Software Engineering Notes}, volume = 18, number = 5, pages = {79-88}, month = dec, year = 1993, abstract = {We present a methodology for the formal specification and development of software system using Z and the refinement calculus. The methodology combines the data restructuring capabilities and the codified discrete mathematics of Z with the data encapsulation properties and development style of the refinement calculus, and it aims to provide a formal path from design to implementation without unnecessary transformations of notation or the definition of a new calculus. It is illustrated here by the development of two systems, a simple diary and (part of) a text editor, and is contrasted with the use of Z on its own. We discuss related and future work and conclude with some general comments on applied formal methods.} } @InProceedings{ z:wood94, author = {J. C. P. Woodcock and P. H. B. Gardiner and J. R. Hulance}, title = {The Formal Specification in {Z} of {Defence Standard} 00-56}, pages = {9-28}, annote = {}, crossref = {z:z94}, other = {Invited paper} } @Article{ z:wood95, author = {J. C. P. Woodcock and P. G. Larsen}, title = {Guest Editorial}, journal = {IEEE Transactions on Software Engineering}, volume = 21, number = 2, pages = {61-62}, month = feb, year = 1995, annote = {Best papers from the FME'93 Symposium \cite{z:wood93}. See \cite{z:bica95,z:bosw95,z:crai95b,z:jack95}.} } @Book{ z:wood96, author = {J. C. P. Woodcock and J. Davies}, title = {Using {Z}: Specification, Proof and Refinement}, publisher = {Prentice Hall International Series in Computer Science}, url = {http://www.comlab.ox.ac.uk/usingz.html}, isbn = {0-13-948472-8}, price = {\pounds18.95 or \$37.95}, year = 1996, length = 391, annote = {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. \par 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.} } @Article{ z:woon97, title = {Formal Derivation to Object-Oriented Implementation of Financial Policies}, author = {Woon, I. M. Y. and Loh, W. L.}, journal = {International Journal of Computer Applications in Technology}, year = 1997, volume = 10, number = {5--6}, pages = {316-326}, issn = {0952-8091}, abstract = {The use of formal methods promises correctness, verifiability, robustness and reliability of operational software systems which have been developed so far. Object-oriented methods enable easier development and maintenance of software application systems and promote the reuse of design and program code. Mapping formal specifications into an object-oriented application will therefore give a system that is not only correct and reliable, but easy to develop and enhance. In this paper, we show how specifications containing major decisions that financial managers typically make, can be expressed in the Z notation. These specifications are subsequently translated into pseudo object-oriented programs.}, keywords = {financial policies, formal specification, object-oriented method, Z notation} } @InProceedings{ z:word86, author = {J. B. Wordsworth}, title = {Teaching Formal Specification Methods in an Industrial Environment}, booktitle = {Proc.\ Software Engineering '86}, organization = {IEE/BCS}, publisher = {Peter Peregrinus}, address = {London}, year = 1986 } @InProceedings{ z:word88, author = {J. B. Wordsworth}, title = {Specifying and Refining Programs with {Z}}, booktitle = {Proc.\ 2nd {IEE}/{BCS} Conference on Software Engineering}, organization = {IEE/BCS}, location = {Liverpool, UK, July 1988}, series = {Conference Publication}, number = 290, pages = {8-16}, month = jul, year = 1988, comment = {A tutorial summary.} } @InProceedings{ z:word91, author = {J. B. Wordsworth}, title = {The {CICS} Application Programming Interface Definition}, annote = {}, crossref = {z:z91}, pages = {285-294} } @Book{ z:word93, author = {J. B. Wordsworth}, title = {Software Development with {Z}: A Practical Approach to Formal Methods in Software Engineering}, publisher = {Addison-Wesley Publishing Company}, isbn = {0-201-62757-4}, url = {http://www.blackwell.co.uk/cgi-bin/bb_item?0201627574}, length = 334, price = {\pounds21.95}, year = 1993, url = {http://heg-school.aw.com/cseng/authors/wordsworth/softdev/softdev.html} , annote = {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. \par 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.} } @InProceedings{ z:word94, author = {R. Worden}, title = {Fermenting and Distilling}, pages = {1-6}, annote = {}, crossref = {z:z94}, other = {Invited paper} } @Manual{ z:xiao94, author = {{Xiaoping Jia}}, title = {{ZTC}: A Type Checker for {Z} -- User's Guide}, organization = {Institute for Software Engineering, Department of Computer Science and Information Systems, DePaul University}, address = {Chicago, IL 60604, USA}, length = 54, year = 1994, price = {Free}, other = {E-mail: \verb"jia@cs.depaul.edu".}, annote = {ZTC is a type checker for the Z specification language. ZTC accepts two forms of input: \LaTeX\ \cite{z:lamp93} with the \verb"oz.sty" / \verb"zed.sty" \cite{z:king90d,z:spiv90d} 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.}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/ZTC-1.3/guide.ps.Z} } @InProceedings{ z:youn89, author = {W. D. Young}, title = {Comparing Specifications Paradigms: {Gypsy} and {Z}}, booktitle = {Proc.\ 12th National Computer Security Conference}, location = {Baltimore, Maryland, USA, 10--13 October 1989}, address = {Baltimore, Maryland, USA}, month = {10--13 October}, other = {Also Technical Report 45, from Computational Logic Inc., 1717 W.\ 6th St., Suite 290, Austin, Texas 78703, USA}, length = 21, year = 1989, telephone = {+1-512-322-9951} } @Proceedings{ z:z90, editor = {J. E. Nicholls}, title = {{Z} User Workshop, {Oxford} 1989}, booktitle = {{Z} User Workshop, {Oxford} 1989}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, location = {Rewley House, Oxford, UK, 15 December 1989}, length = 288, year = 1990, isbn = {3-540-19627-7}, price = {\pounds24.00 soft cover (BCS members \pounds19.00)}, url = {http://www.dcs.gla.ac.uk/springer-verlag/51.html}, annote = {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 \cite{z:oakl90}. For individual papers, see \cite{z:benj90,z:brow90,z:brya90,z:coop90,z:dick90,% z:flyn90,z:grav90,z:haye90b,z:hepw90,z:john90,z:lano90,z:nash90,% z:phil90,z:smit90,z:spiv90c,z:whit90}.} } @Proceedings{ z:z91, editor = {J. E. Nicholls}, title = {{Z} User Workshop, {Oxford} 1990}, booktitle = {{Z} User Workshop, {Oxford} 1990}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, location = {Lady Margaret Hall, Oxford, UK, 17--18 December 1990}, length = 387, year = 1991, isbn = {3-540-19672-2}, price = {\pounds26.00 Soft cover (BCS members \pounds20.00}, url = {http://www.dcs.gla.ac.uk/springer-verlag/50.html}, annote = {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 \cite{z:bain91,z:breu91,z:butl91,z:coom91,z:gard91,z:grav91,z:haye91,% z:hepw91,z:iach91,z:jone91,z:jord91,z:lano91,z:meir91,z:moff91,% z:neil91,z:nich91,z:norc91,z:rand91,z:semm91,z:whys91b,z:word91}. The proceedings also includes an {\em Introduction and Opening Remarks}, a {\em Selected Z Bibliography}, a selection of posters and information on Z tools.} } @Proceedings{ z:z92, editor = {J. E. Nicholls}, title = {{Z} User Workshop, {York} 1991}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, location = {University of York, UK, 16--17 December 1991}, length = 401, year = 1992, isbn = {3-540-19780-X}, price = {\pounds29.00 paperback}, url = {http://www.dcs.gla.ac.uk/springer-verlag/21.html}, annote = {Proceedings of the 6th Z User Meeting, York, UK. Published in collaboration with the British Computer Society. For individual papers, see \cite{z:arth92,z:bard92,z:deba92,z:carr92,z:dill92,z:duke92,% z:harr92,z:neil92,z:nich92,z:pola92,z:saal92,z:smit92,z:swat92,% z:vale92,z:wood92,z:zave92}.} } @Proceedings{ z:z93, editor = {J. P. Bowen and J. E. Nicholls}, title = {{Z} User Workshop, {London} 1992}, booktitle = {{Z} User Workshop, {London} 1992}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, location = {DTI Offices, London, UK, 14--15 December 1992}, length = 347, year = 1993, isbn = {3-540-19818-0}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zum92.ps.Z}, url = {http://www.dcs.gla.ac.uk/springer-verlag/7.html}, price = {\pounds37.00 paperback (\pounds30.00 to workshop participants and BCS members)}, other = {Phone +44-81-947-1280 or fax +44-81-947-4651}, annote = {Proceedings of the 7th Z User Meeting, DTI Offices, London, UK. Published in collaboration with the British Computer Society. For individual papers, see \cite{z:bard93,z:brad93,z:coom93,z:crai93c,z:cusa93,z:cusa93b,% z:drap93,z:haye93d,z:jack93b,z:knig93,z:lano93c,z:love93,z:maun93,% z:nich93,z:norm93,z:rafs93,z:rudd93,z:swat93,z:vale93}. The proceedings also includes an {\em Introduction and Opening Remarks}, a {\em Select Z Bibliography} and a section answering {\em Frequently Asked Questions}.} } @Proceedings{ z:z94, editor = {J. P. Bowen and J. A. Hall}, title = {{Z} User Workshop, {Cambridge} 1994}, booktitle = {{Z} User Workshop, {Cambridge} 1994}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, url = {http://www.comlab.ox.ac.uk/archive/z/zum94.html}, isbn = {3-540-19884-9}, year = 1994, length = 403, price = {\pounds39.00 paperback (\pounds31.00 to workshop participants and BCS members)}, other = {Phone +44-81-947-1280 or fax +44-81-947-4651}, annote = {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 \cite{z:baum94,z:bowe94b,z:breu94,z:carr94,% z:chan94,z:dill94b,z:enge94,z:evan94,z:garl94,z:hall94,z:hall94b,% z:hamm94,z:hass94,z:lamp94,z:mata94,z:pola94,z:smit94,z:weze94,% z:wood94,z:word94}. The proceedings also includes an {\em Introduction and Opening Remarks}, a {\em Select Z Bibliography} and a section answering {\em Frequently Asked Questions}.} } @Proceedings{ z:z95, editor = {J. P. Bowen and M. G. Hinchey}, title = {{ZUM'95}: The {Z} Formal Specification Notation, 9th International Conference of {Z} Users, {Limerick}, {Ireland}, September 7--9, 1995, Proceedings}, booktitle = {{ZUM'95}: The {Z} Formal Specification Notation}, location = {Limerick, Ireland, 7--9 September 1995}, publisher = {Springer-Verlag}, series = lncs, volume = 967, url = {http://www.comlab.ox.ac.uk/archive/z/zum95.html}, isbn = {3-540-60271-2}, year = 1995, annote = {Proceedings of the 9th Z User Meeting, University of Limerick, Ireland. For individual papers presented at the main conference, see \cite{z:banc95,z:bern95,z:brya95,z:ciac95,z:deli95,z:derr95,z:dinv95,% z:edmo95,z:fran95,z:germ95,z:good95,z:hall95,z:horc95,z:hugh95,% z:jack95c,z:kraa95,z:lisk95,z:luck95,z:macd95,z:mikk95,z:parn95,% z:reil95,z:rush95,z:smit95,z:step95,z:stru95,z:vale95b,z:west95}. Some papers formed part of an associated Educational Issues Session organized by Neville Dean \cite{z:ciac95b,z:dean95b,z:grie95,z:miku95,z:parn95b,z:wing95}. The proceedings also includes as appendices a {\em Select Z Bibliography} and a section answering {\em Frequently Asked Questions}.} } @Proceedings{ z:z97, editor = {J. P. Bowen and M. G. Hinchey and D. Till}, title = {{ZUM'97}: The {Z} Formal Specification Notation, 10th International Conference of {Z} Users, {Reading}, {UK}, 3--4 April 1997}, booktitle = {{ZUM'97}: The {Z} Formal Specification Notation}, publisher = {Springer-Verlag}, series = lncs, volume = 1212, url = {http://www.cs.reading.ac.uk/zum97/}, isbn = {3-540-62717-0}, year = 1997, annote = {Proceedings of the 10th Z User Meeting, The University of Reading, UK. For individual papers presented at the main conference, see \cite{z:acha97,z:borg97,z:butl97,z:cian97,z:derr97,z:dinv97,% z:evan97,z:hall97,z:hall97b,z:heit97,z:helk97,z:hewi97,z:jack97b,% z:knig97,z:kraa97,z:lano97,z:lano97b,z:saal97,z:stod97}. The proceedings also includes as appendices a {\em Select Z Bibliography} \cite{z:bowe97b} and a section answering {\em Frequently Asked Questions} \cite{z:bowe97c}.} } @Proceedings{ z:z98, editor = {J. P. Bowen and A. Fett and M. G. Hinchey}, title = {{ZUM'98}: The {Z} Formal Specification Notation, 11th International Conference of {Z} Users, {Berlin}, {Germany}, 24--26 September 1998}, booktitle = {{ZUM'98}: The {Z} Formal Specification Notation}, publisher = {Springer-Verlag}, series = lncs, volume = 1493, url = {http://www.fmse.cs.reading.ac.uk/zum98/}, year = 1998, annote = {Proceedings of the 11th Z User Meeting, Technical University of Berlin, Germany. For individual papers presented at the main conference, see \cite{z:arth98,z:bowe98,z:cian98,z:derr98,z:dupu98,z:fisc98,% z:frie98,z:grim98,z:hend98,z:jack98,z:lano98,z:leve98,z:luth98,% z:maho98,z:murr98,z:olde98,z:paig98,z:sant98,z:sore98,z:step98,% z:stod98,z:toyn98,z:vale98}. The proceedings also includes as appendices this bibliography \cite{z:bowe98b} and a section answering {\em Frequently Asked Questions} \cite{z:bowe98c}.} } @InProceedings{ z:zave91, author = {P. Zave and M. Jackson}, title = {Techniques for Partial Specification and Specification of Switching Systems}, note = {}, crossref = {z:preh91}, pages = {511-525}, annote = {Also published as \cite{z:zave92}.} } @InProceedings{ z:zave92, author = {P. Zave and M. Jackson}, title = {Techniques for Partial Specification and Specification of Switching Systems}, crossref = {z:z92}, pages = {205-219}, annote = {}, other = {Also published as \cite{z:zave91}.} } @Article{ z:zave93, author = {P. Zave and M. Jackson}, title = {Conjunction as Composition}, journal = {ACM Transactions on Software Engineering and Methodology (TOSEM)}, volume = 2, number = 4, pages = {379-411}, month = oct, year = 1993, annote = {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.} } @Article{ z:zave96, author = {P. Zave and M. Jackson}, title = {Where do Operations Come From? {A} Multiparadigm Technique}, journal = {IEEE Transactions on Software Engineering}, volume = 22, number = 7, pages = {508-528}, month = jul, year = 1996, annote = {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.}, issn = {0098-5589}, abstract = {We propose a technique to help people organize and write complex specifications, exploiting the best features of several different specification languages. 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. Consistency analysis of the resulting specification is based on the structural rules. The technique is illustrated by two examples, a graphical human-computer interface and a telecommunications system.}, keywords = {systems, formal methods, multiparadigm specification, consistency analysis, telecommunications, graphical human-computer interfaces, Z} } @Article{ z:zhan91, author = {Y. Zhang and P. Hitchcock}, title = {{EMS}: Case Study in Methodology for Designing Knowledge-based Systems and Information Systems}, journal = {Information and Software Technology}, publisher = {Butterworth-Heinemann}, pages = {518-526}, volume = 33, number = 7, month = sep, year = 1991 } @Misc{ z:zzarc, key = {ZZarchive}, editor = {J. P. Bowen}, title = {{Z} Archive}, howpublished = {URL: \verb"http://www.comlab.ox.ac.uk/archive/z.html"}, year = {1994 onwards}, url = {http://www.comlab.ox.ac.uk/archive/z.html}, annote = {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 \cite{z:00bib} 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 {\tt ftp://ftp.comlab.ox.ac.uk/pub/Zforum/} directory.}, other = {For information on access via electronic mail, send a message to {\tt archive-server@comlab.ox.ac.uk} containing the command `{\tt help}'.} }