Mark Utting's Web Home

Note: During A semester of 2012, I will be in my office most days during weeks 1-2, 4-5, 7-8, and 10-11, and available online via email at other times.

In 2012, I am teaching the following paper:

• COMP453/553A: "Extremely Parallel Programming", which introduces several different ways of programming with thousands of threads. (Paper Outline).

In 2007, Bruno Legeard and I wrote a book on model-based testing, called Practical Model-Based Testing: A Tools Approach.

I am a member of the following research projects:

• JStar 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 program.
• 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!).
• ModelJUnit 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.
• CZT: 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.
• Smartesting: is a French software company that has commercialized the model-based testing techniques developed in our collaborative French/NZ BZ-TT (B/Z Testing Tools) project. The Smartesting Test Designer tool now generates system tests from UML models. I am a senior consultant to Smartesting.
• 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:

• You can help Feed the Hungry, by clicking on a web button!
• Programming Languages -- some of the newer ones are well worth trying!
• Formal methods: making programming easier and more reliable is my goal...
• Object-oriented language design and refinement (my phd topic).
• Software and web sites for learning French.
• Music Programs (for children, and for me).
• How to become a programmer (quickly!)
• Check out Christopher Raphael's Music Plus One piano accompaniment system (interprets MIDI files in the style of a human player).
• The 50-year anniversary of the first stored-program digital computer. (The Baby Mark-1 at Manchester University -- you can even write a program for it!).
• Lego Mindstorms Robotics Kit: 'A Lego Brick with a Brain'.
• Entertainment (mostly New Zealand).
• HiFi companies, reviews, magazines and links.
• Interesting/useful organisations that are on the web.
• The Economist, on world-wide trends in the nature and funding of Universities and the Internet economy.
• Open source (free) software: Novel funding models like: the Free Software Baazar, the Cooperative Market (here is a survey of Free Software Funding models). I am currently developing some open source software.
• Teaching ideas.
• Journals and publishers on the web.
• Reference works and indexes.
• Our local SCMS help pages.
• Some Utting family history and people (which I haven't yet connected with my ancestors). Here are some more general ancestor searching sites: Heartland; Kings Lynn Online
• Artificial life is now available as a game for your PC. Nurture your own `Norms' (little animated bundles of fluff with saucer eyes and floppy ears, wrapped around a neural net with biochemistry!). Read about how they work in IEEE Expert, Jul/Aug 97. I bought the `Creatures' game from Dick Smith for about NZ$29. Here is an NZ site for Norn-related programming.

  Of Norns, it can truly be said: "Watch your thoughts: they become words. Watch your words: they become actions. Watch your actions: they become habits. Watch your habits: they become character. Watch your character: it becomes your destiny."
  [I guess this is true of humans too!]

• News sites: Deja.com and Remarq.com.

Selected Publications

• 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" grand challenge.
• A 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 ZB2005.
  This gives a good overview of our Community Z Tools (CZT) sourceforge project.
• Object-Orientation without extending Z by Mark Utting and Shaochun Wang. Presented at ZB2005.
  This describes a technique of using loose axiomatic definitions to specify supertype behaviour, with tighter definitions being added for subtypes.
• ZML: XML Support for Standard Z by Mark Utting, Ian Toyn, Jing SUN, Andrew Martin, Jin Song DONG, Nicholas Daley, and David Currie. Presented at ZB2003.
  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. © Springer-Verlag, LNCS 2391
  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 2002. © Springer-Verlag, LNCS 2272
  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 University, Australia.
  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.
• Data 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.
• A 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 Press.
• 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. Springer-Verlag, 1996.
• 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.