A semantics and implementation of a causal logic programming language (2009)
Cleary, John G., Utting, Mark, Clayton, Roger
The increasingly widespread availability of multicore and manycore computers demands new programming languages that make parallel programming dramatically easier and less error prone. This paper...
Putting formal specifications under the magnifying glass: Model-based for Validation (2009)
Aydal, Emine G., Paige, Richard F., Utting, Mark, Woodcock, Jim
A software development process is effectively an abstract form of model transformation, starting from an end-user model of requirements, through to a system model for which code can be automatically...
Object orientation without extending Z (2008)
Mark Utting, Mark Utting, Mark Utting, Shaochun Wang, Shaochun Wang, Shaochun Wang
Abstract. The good news of this paper is that without extending Z, we can elegantly specify object-oriented systems, including encapsulation, inheritance and subtype polymorphism (dynamic dispatch)....
The date of receipt and acceptance will be inserted by the editor Abstract. We present a comprehensive refinement calculus for the development of sequential, real-time programs from real-time...
Position paper: model-based testing (2008)
This position paper gives an overview of model-based testing and discusses how
The Role of Model-Based Testing (2008)
This position paper gives an overview of model-based testing and discusses how it might fit into the proposed grand challenge for a program verifier.
Unit testing of Z specifications (2008)
We propose a simple framework for validation unit testing of Z specifications, and illustrate this framework by testing the first few levels of a POSIX specification. The tests are written in...
A Comparison of State-Based Modelling Tools for Model Validation (2008)
Aydal, Emine G., Utting, Mark, Woodcock, Jim
In model-based testing, one of the biggest decisions taken before modelling is the modelling language and the model analysis tool to be used to model the system under investigation. UML, Alloy and Z...
Andrew Martin, Andrew Martin, Ray Nickson, Ray Nickson, Mark Utting, Mark Utting
reports are available via anonymous ftp, from svrc.it.uq.edu.au in the directory /pub/techreports. Abstracts and compressed postscript files are available via
Lindsay Groves Ray, Ray Nickson, Greg Reeve, Steve Reeves, Mark Utting
. We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with...
Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, David Currie
Abstract. This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new...
A Comparison of the BTT and TTF Test-Generation Methods (2007)
Bruno Legeard, Fabien Peureux, Mark Utting
Abstract. This paper compares two methods of generating tests from formal specications. The Test Template Framework (TTF) method is a framework and set of heuristics for manually generating test sets...
Verification of Starlog Programs (2007)
Starlog is a purely declarative, temporal, logic programming language. It supports both bottom-up and top-down execution and is well-suited to writing reactive programs. This paper presents a simple...
Teaching Formal Methods Lite via Testing (2007)
A new style of formal methods course is described, based on a pragmatic approach that emphasizes testing. The course introduces students to formal specification using Z, and shows how formal...
Jumble Java Byte Code to Measure the Effectiveness of Unit Tests (2007)
Irvine, Sean A., Pavlinic, Tin, Trigg, Leonard E., Cleary, John G., Inglis, Stuart J., Utting, Mark
Jumble is a byte code level mutation testing tool for Java which inter-operates with JUnit. It has been designed to operate in an industrial setting with large projects. Heuristics have been included...
A subset of precise UML for Model-based Testing (2007)
Bouquet, Fabien, Grandpierre, C., Legeard, B., Peureux, F., Vacelet, N., Utting, Mark
This paper presents an original model-based testing approach that takes a UML behavioural view of the system under test and automatically generates test cases and executable test scripts according to...
A Taxonomy of model-based testing (2006)
Utting, Mark, Pretschner, Alexander, Legeard, Bruno
Model-based testing relies on models of a system under test and/or its environment to derive test cases for the system. This paper provides an overview of the field. Seven different dimensions define...
A Taxonomy of model-based testing (2006)
Utting, Mark, Pretschner, Alexander, Legeard, Bruno
Model-based testing relies on models of a system under test and/or its environment to derive test cases for the system. This paper provides an overview of the field. Seven different dimensions define...
Abstractions for Model-Based Testing (2006)
Mark Utting, Alexander Pretschner, C Mark Utting, Er Pretschner, Bruno Legeard, Bruno Legeard, ...
c LEIRIOS Technologies and Laboratoire d’Informatique de l’Université de Franche-Comté
Symbolic Animation of JML Specifications (2005)
Fabrice, Bouquet, Dadeau, Frederic, Legeard, Bruno, Utting, Mark
This paper presents a model-based framework for the symbolic animation of object-oriented specifications. A customized set-theoretic solver is used to simulate the execution of the system and handle...
CZT: A Framework for Z Tools (2005)
The Community Z Tools (CZT) project is an open-source Java framework for building formal methods tools for Z and Z dialects. It also includes a set of tools for parsing, typechecking, transforming...
Symbolic Animation of JML Specifications (2005)
Fabrice, Bouquet, Dadeau, Frederic, Legeard, Bruno, Utting, Mark
This paper presents a model-based framework for the symbolic animation of object-oriented specifications. A customized set-theoretic solver is used to simulate the execution of the system and handle...
CZT: A Framework for Z Tools (2005)
The Community Z Tools (CZT) project is an open-source Java framework for building formal methods tools for Z and Z dialects. It also includes a set of tools for parsing, typechecking, transforming...
Jaza User Manual and Tutorial (2005)
Jaza stands for ‘Just Another Z Animator’. It is an open-source animator for the Z specification language. It is written in Haskell, which is a modern strongly-typed functional programming...
CZT: A Framework for Z Tools (2005)
Abstract. The Community Z Tools (CZT) project is an open-source Java framework for building formal methods tools for Z and Z dialects. It also includes a set of tools for parsing, typechecking,...
Controlling test case explosion in test generation for B formal models: Research Articles (2004)
Legeard, Bruno, Peureux, Fabien, Utting, Mark
BZ-TESTING-TOOLS (BZ-TT) is a tool set for automated test case generation from B and Z specifications. BZ-TT uses boundary and cause–effect testing on the basis of the formal model. It has been...
Controlling test case explosion in test generation for B formal models: Research Articles (2004)
Legeard, Bruno, Peureux, Fabien, Utting, Mark
BZ-TESTING-TOOLS (BZ-TT) is a tool set for automated test case generation from B and Z specifications. BZ-TT uses boundary and cause–effect testing on the basis of the formal model. It has been...
Dissertation (LLB(Hons))--University of Auckland, 2003.
D.: ZML: XML Support for Standard Z (2003)
Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, Nicholas Daley, ...
Abstract. This paper proposes an XML format for standard Z.We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new...
D.: ZML: XML Support for Standard Z (2003)
Nicholas Daley, Nicholas Daley, Mark Utting, Mark Utting, Mark Utting, Ian Toyn, ...
Abstract. This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new...
Object orientation without extending Z (2002)
The good news of this paper is that without extending Z, we can elegantly specify object-oriented systems, including encapsulation, inheritance and subtype polymorphism (dynamic dispatch). The bad...
ZML:XML support for standard Z. (2002)
Utting, Mark, Toyn, Ian, Sun, Jing, Martin, Andrew, Dong, Jin Song, Daley, Nicholas, ...
This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new proposal is...
Object orientation without extending Z (2002)
The good news of this paper is that without extending Z, we can elegantly specify object-oriented systems, including encapsulation, inheritance and subtype polymorphism (dynamic dispatch). The bad...
ZML:XML support for standard Z. (2002)
Utting, Mark, Toyn, Ian, Sun, Jing, Martin, Andrew, Dong, Jin Song, Daley, Nicholas, ...
This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new proposal is...
Ergo 6: a generic proof engine that uses Prolog proof technology (2002)
Utting, Mark, Robinson, Peter, Nickson, Ray
This paper describes the architecture of the Ergo theorem prover. It discusses the use of Prolog technology as the implementation language. The paper provides a useful comparison of this technology...
Ergo 6: a generic proof engine that uses Prolog proof technology (2002)
Utting, Mark, Robinson, Peter, Nickson, Ray
This paper describes the architecture of the Ergo theorem prover. It discusses the use of Prolog technology as the implementation language. The paper provides a useful comparison of this technology...
Waitangi Tribunal Bibliography and Parliamentary Debates (2002)
Williams, David, Utting, Mark, Shaw, Joshua
Items in ResearchSpace are protected by copyright, with all rights reserved, unless otherwise indicated. Previously published items are made available in accordance with the copyright policy of the...
A Comparison of the BTT and TTF Test-Generation Methods (2002)
Legeard, Bruno, Peureux, Fabien, Utting, Mark
This paper compares two methods of generating tests from formal specifications. The Test Template Framework (TTF) method is a framework and set of heuristics for manually generating test sets from a...
Automated Boundary Testing from Z and B (2002)
Legeard, Bruno, Peureux, Fabien, Utting, Mark
We present a method for black-box boundary testing from B and Z formal specifications. The basis of the method is to test every operation of the system at every boundary state using all input...
A Comparison of the BTT and TTF Test-Generation Methods (2002)
Legeard, Bruno, Peureux, Fabien, Utting, Mark
This paper compares two methods of generating tests from formal specifications. The Test Template Framework (TTF) method is a framework and set of heuristics for manually generating test sets from a...
Automated Boundary Testing from Z and B (2002)
Legeard, Bruno, Peureux, Fabien, Utting, Mark
We present a method for black-box boundary testing from B and Z formal specifications. The basis of the method is to test every operation of the system at every boundary state using all input...
Automated Boundary Testing from Z and B (2002)
Bruno Legeard, Fabien Peureux, Mark Utting
Abstract. We present a method for black-box boundary testing from B and Z formal specications. The basis of the method is to test every operation of the system at every boundary state using all input...
Optimising Tabling Structures for Bottom-Up Logic Programming (2002)
Roger Clayton, John G. Cleary, Bernhard Pfahringer, Mark Utting
In this paper we show how ecient data structures can be automatically introduced into programs that are written using at database like relations. We describe a compilation process for Starlog, which...
Data structures for Z testing tools. (2001)
This paper describes some of the difficulties and challenges that arise during the design of tools for validating Z specifications by testing and animation. We address three issues: handling...
Data structures for Z testing tools. (2001)
This paper describes some of the difficulties and challenges that arise during the design of tools for validating Z specifications by testing and animation. We address three issues: handling...
A sequential real-time refinement calculus (2001)
This substantial (64 page) journal article is the first journal article on the real-time refinement calculus and forms the start of fruitful a line of research in this area. The paper takes a...
A sequential real-time refinement calculus (2001)
This substantial (64 page) journal article is the first journal article on the real-time refinement calculus and forms the start of fruitful a line of research in this area. The paper takes a...
Teaching formal methods lite via testing (2001)
A new style of formal methods course is described, based on a pragmatic approach that emphasizes testing. The course introduces students to formal specification using Z, and shows how formal...
Teaching formal methods lite via testing (2001)
A new style of formal methods course is described, based on a pragmatic approach that emphasizes testing. The course introduces students to formal specification using Z, and shows how formal...
A sequential real-time refinement calculus (2001)
This substantial (64 page) journal article is the first journal article on the real-time refinement calculus and forms the start of fruitful a line of research in this area. The paper takes a...
A survey of software development practices in the New Zealand software industry (2000)
Groves, Lindsay, Nickson, Ray, Reeve, Greg, Reeves, Steve, Utting, Mark
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a...
A survey of software development practices in the New Zealand software industry (2000)
Groves, Lindsay, Nickson, Ray, Reeve, Greg, Reeves, Steve, Utting, Mark
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a...
Data structures for Z testing tools (2000)
Abstract: This paper describes some of the difficulties and challenges that arise during the design of tools for validating Z specifications by testing and animation. We address three issues:...
Data structures considered harmful (2000)
John G. Cleary, Mark Utting, Roger Clayton
We describe an approach to logic programming where the execution of a pure logic program is ordered on "temporal " values in the program. The resulting programs are relational and...
Data Structures for Z Testing Tools (2000)
: This paper describes some of the diculties and challenges that arise during the design of tools for validating Z specications by testing and animation. We address three issues: handling undened...
Groves, Lindsay, Nickson, Ray, Reeve, Greg, Reeves, Steve, Utting, Mark
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a...
Groves, Lindsay, Nickson, Ray, Reeve, Greg, Reeves, Steve, Utting, Mark
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a...
Thesis (MA--Russian)--University of Auckland, 1999.
Lindsay Groves, Ray Nickson, Greg Reeve, Steve Reeves, Mark Utting
Abstract. We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software...
Deadlines Are Termination (1998)
Ian J. Hayes, Ian J. Hayes, Mark Utting, Mark Utting
s and compressed postscript files are available from http://svrc.it.uq.edu.au Deadlines are termination Ian J. Hayes Mark Utting y Abstract We have recently extended the sequential refinement...
Deadlines are termination (1998)
from svrc.uq.edu.au in the directory /pub/techreports. Abstracts and compressed postscript files are available from
Coercing real-time refinement: A transmitter (1997)
Note: Most SVRC technical reports are available via anonymous ftp, from svrc.uq.edu.au in the directory /pub/techreports. Abstracts and compressed postscript files are available from
The Ergo 5 Generic Proof Engine (1997)
s and compressed postscript files are available via http://svrc.it.uq.edu.au The Ergo 5 Generic Proof Engine Mark Utting Abstract This paper describes the design principles and the architecture of...
A Tactic Language for Ergo (1997)
Andrew Martin, Andrew Martin, Ray Nickson, Ray Nickson, Mark Utting, Mark Utting
A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on Angel, for tactic programming, user interface, and proof representation. This paper describes...
A Sequential Real-time Refinement Calculus (1997)
Ian J. Hayes, Ian J. Hayes, Mark Utting, Mark Utting
s and compressed postscript files are available from http://svrc.it.uq.edu.au A Sequential Real-time Refinement Calculus Ian J. Hayes Mark Utting y Abstract We present a comprehensive refinement...
Refinement of Infeasible Real-Time Programs (1997)
Mark Utting, Mark Utting, Colin Fidge, Colin Fidge
. Embedded real-time programs can be succinctly specified using timed traces. Each sequentially executed statement acts to define a distinct trace segment. An elegant way of defining the effect of...
Interpretation and Instantiation of Theories for Reasoning about Formal Specifications (1997)
Nicholas Hamilton, Nicholas Hamilton, Ray Nickson, Ray Nickson, Owen Traynor, ...
In this paper an outline is given of an approach to formally reasoning about importation, parameterisation and instantiation of specifications written in a modular extension of the Z language (called...
Reasoning about Aliasing (1997)
. Object-oriented systems are typically structured as complex networks of interacting mutable objects. To reason about such systems, simple and efficient techniques for coping with aliasing are...
A formal method for building concurrent real-time software (1997)
Colin Fidge, Peter Kearney, Mark Utting
Quartz is a formal development method for concurrent real-time programs. It comprises • real-time requirements specification in a variant of the Z notation,
Ergo 4.1 Reference Manual (1996)
Holger Becht, Holger Becht, Anthony Bloesch, Anthony Bloesch, Ray Nickson, Ray Nickson, ...
This document describes the commands available in the theorem prover Ergo. It assumes that the reader is familiar, to some extent, with Ergo (refer to the Ergo User Manual [UW94]). As such, it is...
Reasoning about Aliasing (1996)
Object-oriented systems are typically structured as complex networks of interacting mutable objects. To reason about such systems, simple and efficient techniques for coping with aliasing are needed....
Coercing real-time refinement: A transmitter (1996)
Ian J. Hayes, Ian J. Hayes, Mark Utting, Mark Utting
Our overall goal is to support the development of real-time programs from specifications via a process of stepwise refinement. One problem in developing a real-time program in a high-level...
A Real-Time Refinement Calculus That Changes Only Time (1996)
Mark Utting, Mark Utting, Colin Fidge, Colin Fidge
The behaviour of a real-time system that interacts repeatedly with its environment is most succinctly specified by its possible traces, or histories. We present a way of using the refinement calculus...
A New Face For Ergo: Adding A User Interface To A Programmable Theorem Prover (1995)
Ray Nickson, Ray Nickson, Mark Utting, Mark Utting
We describe some of the technology we used to build a user interface for a programmable theorem prover. By separating the user interface from the application itself, it is possible to experiment with...
Animating Z: Interactivity, Transparency and Equivalence (1994)
The ability to animate Z specifications is useful in allowing a specifier to explore the behaviour of a specification. This paper defines three new evaluation criteria for animation systems,...
Pipeline Specification of a MIPS R3000 CPU (1994)
Mark Utting, Mark Utting, Peter Kearney, Peter Kearney
This document contains a specification of the behavioural and real-time aspects of a typical MIPS R3000 RISC CPU. To increase assurance of correctness relative to the operational behaviour of the...
Real Time Behaviour of a (1994)
Peter Kearney, Peter Kearney, Mark Utting, Mark Utting, Keith Whitwell, Keith Whitwell
. This paper gives an overview of: two levels of formal specification of the real-time behaviour of a commercial RISC chip; an approach to verifying the higher-level specification relative to the...
Instruction Level Specification of a MIPS R3000 CPU (1994)
R Cpu, Mark Utting, Mark Utting
This specification builds on top of a low level pipeline specification of the MIPS R3000 and presents a more abstract view of instruction execution. The specification defines a more abstract...
A Layered Real-Time Specification of a RISC Processor (1994)
Peter Kearney, Peter Kearney, Mark Utting, Mark Utting
This paper gives an overview of the real-time specification of a commercial RISC processor. The specification is at two related levels, with an abstraction relation defined between them. The lower...
A Haskell implementation of Z data types (1994)
This report describes a Haskell [HPe92] module that implements finite versions of the set, relation and function types from Z [Hay87] [Spi89]. It uses the literate script convention, where each...
Mark Utting, Mark Utting, Keith Whitwell, Keith Whitwell
this document to describe Qu-Prolog in detail. However, since Ergo is implemented in Qu-Prolog, some comments about Qu-Prolog are required in order to use its syntax during interaction with the...
Specification Issues for Real-Time Behaviour of RISC Processors (1992)
Mark Utting, Mark Utting, Peter Kearney, Peter Kearney
This report presents an overview of some of the main issues relevant to the task of specifying the real-time behaviour of various commercially available RISC architectures. These issues were...
An Object-Oriented Refinement Calculus with Modular Reasoning (1992)
In this thesis, the refinement calculus is extended to support a variety of object-oriented programming styles. The late binding of procedure calls in object-oriented languages is modelled by...