@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.zuser.org/z/bib.html"}, year = {1990 onwards}, url = {http://www.zuser.org/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"jpbowen@zuser.org".}, comment = {Master Z Bibliography in BibTeX database format. Maintained by Jonathan Bowen. Prof. Jonathan Bowen, Professor of Computing Faculty of Business, Computing and Information Management London South Bank University, Borough Road, London SE1 0AA, UK Tel: +44 (0)20 7815 7462 Fax: +44 (0)870 133 8371 Email: jonathan.bowen@lsbu.ac.uk URL: http://www.jpbowen.com/ Centre for Applied Formal Methods: http://www.cafm.sbu.ac.uk/ Please send new entries to Jonathan Bowen. Copyright © 1990-2003 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, 5 August 2003. 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-users.cs.york.ac.uk/~susan/bib/ss/zip/index.htm}, 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://www.afm.sbu.ac.uk/cgi/archive/isbn?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 = {http://www.museophile.sbu.ac.uk/pub/jpb/proc87.pdf}, 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 = {http://www.museophile.sbu.ac.uk/pub/jpb/proc88.pdf}, 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.afm.sbu.ac.uk/zbook/}, 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.zuser.org/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.afm.sbu.ac.uk/cgi/archive/isbn?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}, url = {http://www.icis.qut.edu.au/~davee/im/}, 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 = {115-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 = {Pro