Mark Utting's Web Home
Gidday! I work as an associate professor in the
Computer Science Department
Waikato University for 20% of the
In the other 80% I am a Senior Research Fellow in Software Engineering at
QUT, working on agent-based simulations of the Queensland
Electricity Network, to incorporate higher levels of renewables, such as
Solar Power and Battery Storage.
Note: During A semester of 2014, I will be in my office most days
during weeks 2-3, 5, 7, 8-9, and 11-12, and available online via email at
other times. I am not teaching during B semester.
In 2014, I am teaching the following paper:
"Extremely Parallel Programming", which introduces
several different ways of programming with thousands of threads
(Modules: Java performance, Hadoop, OpenCL on GPUs, Java dataflow programming, JStar).
(see CS Teaching page
for the 453/553 Paper Outline.).
In 2007, Bruno Legeard and I wrote a book on model-based testing, called
Practical Model-Based Testing: A Tools
I am a member of the following research projects:
I also work on the semantics of object-oriented languages,
theorem proving and real-time specification and refinement.
is a new retargetable parallel programming language that we are
developing. It is a pure declarative language with a Java-like
syntax, and its semantics is based on ideas from our earlier Starlog
project (1997-2003), which used a logic-programming style and a
compiler that automatically chose the best data structures for your
NEW: An Eclipse plugin that implements version 2.1.0 (beta)
of the JStar language can be installed into Eclipse 4.2.x+XText 2.3.1
(first install XText 2.3.1 and XTend 2.3.1 from its
update site) from the JStar Eclipse update site: http://www.cs.waikato.ac.nz/~marku/eclipse.jstar.updatesite.
- Jumble is a tool that
will tell you how good your JUnit tests are. It uses mutation
testing to measure the effectiveness of the unit tests, from 0%
(worthless) to 100% (angelic!).
is an open-source model-based testing tool
that generates test suites from models written as Java classes.
It can be used to automate the testing of Java systems as well as
other non-Java systems.
The Community Z Tools project is a
collaborative project to build open-source framework and tools
for the Z specification language and several of its extensions.
We have developed an XML
format for Z, a Java framework for building tools and a
collection of example tools.
I have been working on ZLive (a successor to my
Jaza animator for Z).
CZT provides a simple GUI interface for analyzing Z specifications,
plus two nice IDEs for editing Z: JEdit/CZT and Eclipse/CZT.
CZT also supports Object-Z and Circus.
is a French software company that has commercialized the
model-based testing techniques developed in our
'BZ-TT' (B/Z Testing Tools) project, which was a collaboration
between Waikato University and the
at the University of Franche-Comte. The Smartesting
Test Designer tool now generates system tests from UML models.
I was a senior consultant to Smartesting for several years.
- Waikato Formal Methods
Laboratory: Developing improved tools and calculi for the
development of correct software. My recent research has focussed
on tools for model-based testing, such as ModelJUnit.
Some other topics that interest me:
- The JStar Language Philosophy
by Mark Utting, Min-Hsien Weng and John G. Cleary. Parallel Computing 40(2) Feb. 2014.
This describes the JStar language (a Java-oriented parallel declarative language with the
same semantics as Starlog) and speedup results for several benchmark programs.
- A parallel
semantics for Normal Logic Programs plus time, by J. G. Cleary,
M. Utting and R. Clayton. Working Paper No. 05/2013, Department of Computer
Science, The University of Waikato, 2013. This is a very technical paper about the
semantics and allowable parallel implementations of Starlog and JStar.
- Practical Model-Based Testing: A Tools Approach by Mark Utting
and Bruno Legeard, Morgan-Kaufmann, 2007. The first
book on model-based testing for practicing engineers and testers.
- Position Paper:
Model-Based Testing, my position paper for the
Verified Software: Theories,
Tools, Experiments (VSTTE) conference on the "Program Verifier"
Taxonomy of Model-Based Testing, Department of Computer Science
Working Paper 04/2006.
- Symbolic Animation
of JML Specifications published in FM2005.
This describes an animation tool for the
Java Modelling Language (JML).
- Controlling test case explosion in test generation from B
formal models, by Bruno Legeard, Fabien Peureux, and Mark Utting.
The Journal of Software Testing, Verification and Reliability,
volume 14, number 2, pages 81-103, 2004.
The best overview of the BZTT test generation process.
- CZT: A Framework for Z Tools
by Petra Malik and Mark Utting. Presented at
This gives a good overview of our
Community Z Tools (CZT)
- Object-Orientation without extending Z by Mark Utting and Shaochun Wang. Presented at
This describes a technique of using loose axiomatic definitions
to specify supertype behaviour, with tighter definitions being
added for subtypes.
XML Support for Standard Z
by Mark Utting, Ian Toyn, Jing SUN, Andrew Martin, Jin Song DONG,
Nicholas Daley, and David Currie. Presented at
This describes an XML format for ISO standard Z, which is the
basis of the CZT project. See
http://czt.sourceforge.net/zml for recent changes to this format.
- Ergo 6: a
generic proof engine that uses Prolog proof technology, by
Mark Utting, Peter Robinson and Ray Nickson. The LMS JCM, (5)
194-219, Nov 2002.
- Automated Boundary Testing from Z
and B by Bruno Legeard, Fabien Peureux and Mark Utting,
FME 2002, Copenhagen, Denmark.
Describes an early version of the BZ-TT test generation method
for B and Z.
- BZ-TT: A tool-set for test generation from Z and B using
constraint logic programming, by F. Ambert, F. Bouquet, S. Chemin,
S. Guenaud, B. Legeard, F. Peureux, N. Vacelet, and M. Utting.
Pages 105-119, in Formal
Approaches to Testing of Software, Satellite
Workshop of CONCUR02, August
24th, Brno, Czech Republic, 2002.
A good overview of the BZ-TT tools and architecture.
- A Comparison of the BTT
and TTF Test-Generation Methods by Bruno Legeard, Fabien Peureux
and Mark Utting. ZB2002, Grenoble, France, Jan
This compares the TTF test generation method for Z,
with an early version of the BZ-TT test generation method.
- Verification of Starlog
Programs by John Cleary and Mark Utting. Presented at the
Australasian Workshop on Computational Logic (AWCL'2001), Bond
This presents a simple methodology for proving Starlog programs
correct with respect to predicate calculus specifications.
- Data Structures
considered Harmful by John Cleary, Mark Utting and Roger Clayton.
Presented at the Australasian Workshop on Computational Logic
(AWCL'2000), ANU, Canberra, Australia.
This describes how Starlog programs avoid a premature commitment
to data structures.
- Teaching Formal Methods
Lite via Testing, by Mark Utting and Steve Reeves.
Journal of Software Testing Verification and Reliability (STVR),
11(3), p181-195, Sept 2001.
Structures for Z Testing Tools, by Mark Utting.
Presented at the FM-TOOLS 2000 conference in Germany, July 2000
(in TR 2000-07, Information Faculty, University of Ulm).
Describes the design philosophy of my Z animation tool (Jaza),
and has a brief experimental comparison of several Z animation tools.
- Implementing the Z_c logic in
Ergo, by Mark Utting and Steve Reeves.
Presented at WESTAPP 2000: The Third International Workshop on Explicit
Substitutions: Theory and Applications to Programs and Proofs
in Norwich, England, July 2000.
survey of software development practices in the New
Zealand software industry, by Lindsay Groves, Ray Nickson, Greg
Reeve, Steve Reeves, Mark Utting. In 2000 Australian Software
Engineering Conference: proceedings, 28-29 April 2000, Canberra,
Australia.(pp. 189-201). Los Alamitos, Calif.: IEEE Computer Society
- Reasoning about
Aliasing, by Mark Utting. In Proceedings of the
Fourth Australasian Refinement Workshop (ARW-95),
pages 195--211. School of Computer Science and Engineering, The
University of New South Wales, April 1995.
Identifies key criteria for reasoning about aliasing, then
proposes an extension of the local store technique for
flexible reasoning about pointers.
- A real-time refinement calculus that changes only time,
by M. Utting and C. J. Fidge.
In He Jifeng, editor, BCS-FACS Seventh Refinement Workshop.
- A tactic language for Ergo, by
Andrew Martin, Ray Nickson and Mark Utting.
In Formal Methods Pacific '97, Springer Series in Discrete
Mathematics and Theoretical Computer Science.
Lindsay Groves and Steve Reeves, editors.
Pages 186--207. Springer-Verlag, 1997.
- Modular reasoning in an object-oriented refinement calculus,
by Mark Utting and Ken Robinson.
In Mathematics of Program Construction. Second International
Conference, Oxford, U.K., June/July 1992, pages
344--367. Springer-Verlag, 1993. LNCS 669.
This is essentially Chapter 4 of my PhD.
Dr Mark Utting
Department of Computer Science
School of Computing and Mathematical Sciences
The University of Waikato, Private Bag 3105, Hamilton, New Zealand.
Phone: +64 7 838 4791
Fax: +64 7 858 5095
Last modified: Sat Mar 22 13:16:43 EST 2014