Now showing items 1-27 of 27

  • Specification and validation of the MODAM module manager

    Utting, Mark; Boulaire, Fanny (2015)
    Electricity distribution networks are large complex systems that are continuously evolving. Agent-based models are a useful way of exploring possible future scenarios for these networks. This paper introduces MODAM, a ...
  • A Parallel semantics for normal logic programs plus time

    Cleary, John G.; Utting, Mark; Clayton, Roger (University of Waikato, Department of Computer Science, 2013-11-11)
    It is proposed that Normal Logic Programs with an explicit time ordering are a suitable basis for a general purpose parallel programming language. Examples show that such a language can accept real-time external inputs and ...
  • The JStar language philosophy

    Utting, Mark; Weng, Min-Hsien; Cleary, John G. (University of Waikato, Department of Computer Science, 2013-11-11)
    This paper introduces the JStar parallel programming language, which is a Java-based declarative language aimed at discouraging sequential programming, en-couraging massively parallel programming, and giving the compiler ...
  • The JStar language philosophy

    Utting, Mark; Weng, Min-Hsien; Cleary, John G. (Association for Computing Machinery (ACM), 2013)
    This paper introduces the JStar parallel programming language, which is a Java-based declarative language aimed at discouraging sequential programming, encouraging massively parallel programming, and giving the compiler ...
  • A taxonomy of model-based testing approaches

    Utting, Mark; Pretschner, Alexander; Legeard, Bruno (Wiley, 2012)
    Model-based testing (MBT) relies on models of a system under test and/or its environment to derive test cases for the system. This paper discusses the process of MBT and defines a taxonomy that covers the key aspects of ...
  • Improving our fitnesse: From concrete executions to partial specification

    Streader, David; Utting, Mark; Mugridge, Rick (University of Waikato, Department of Computer Science, 2011-04-07)
    Fitnesse and FIT [5] allow systems tests to be written by non-programmers using a Wiki or HTML style of input. However, there is little support for syntactic and semantic checks as the tests are being designed. This paper ...
  • Evolving web-based test automation into agile business specifications

    Mugridge, Rick; Utting, Mark; Streader, David (MDPI, 2011)
    Usually, test automation scripts for a web application directly mirror the actions that the tester carries out in the browser, but they tend to be verbose and repetitive, making them expensive to maintain and ineffective ...
  • Datalog as a parallel general purpose programming language

    Cleary, John G.; Utting, Mark; Clayton, Roger (University of Waikato, Department of Computer Science, 2010-08-27)
    The increasing available parallelism of computers demands new programming languages that make parallel programming dramatically easier and less error prone. It is proposed that datalog with negation and timestamps is a ...
  • A semantics and implementation of a causal logic programming language

    Cleary, John G.; Utting, Mark; Clayton, Roger (University of Waikato, Department of Computer Science, 2009-02-11)
    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 describes a semantics for ...
  • Putting formal specifications under the magnifying glass: Model-based testing for validation

    Aydal, Emine G.; Paige, Richard F.; Utting, Mark; Woodcock, Jim (IEEE Computer Society, 2009)
    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 generated. The success ...
  • The Role of Model-Based Testing

    Utting, Mark (Springer, 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.
  • A Comparison of State-Based Modelling Tools for Model Validation

    Aydal, Emine G.; Utting, Mark; Woodcock, Jim (Springer, 2008)
    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 are examples of popular ...
  • Unit testing of Z specifications

    Utting, Mark; Malik, Petra (Springer, 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 standard Z, and are executable ...
  • A subset of precise UML for Model-based Testing

    Bouquet, Fabien; Grandpierre, C.; Legeard, Bruno; Peureux, Fabien; Vacelet, N.; Utting, Mark (ACM, 2007)
    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 model coverage criteria. ...
  • Jumble Java Byte Code to Measure the Effectiveness of Unit Tests

    Irvine, Sean A.; Pavlinic, Tin; Trigg, Leonard E.; Cleary, John G.; Inglis, Stuart J.; Utting, Mark (IEEE Computer Society, 2007)
    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 to speed the checking ...
  • A Taxonomy of model-based testing

    Utting, Mark; Pretschner, Alexander; Legeard, Bruno (2006-04-01)
    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 that allows ...
  • CZT: A Framework for Z Tools

    Malik, Petra; Utting, Mark (Springer, 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 and printing standard Z ...
  • Symbolic Animation of JML Specifications

    Fabrice, Bouquet; Dadeau, Frederic; Legeard, Bruno; Utting, Mark (Springer, 2005)
    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 constraints on state ...
  • Controlling test case explosion in test generation for B formal models: Research Articles

    Legeard, Bruno; Peureux, Fabien; Utting, Mark (John Wiley & Sons, Ltd., 2004)
    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 used and validated on several ...
  • ZML:XML support for standard Z.

    Utting, Mark; Toyn, Ian; Sun, Jing; Martin, Andrew; Dong, Jin Song; Daley, Nicholas; Currie, David (2002-12-01)
    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 based upon a comparison ...
  • Object orientation without extending Z

    Utting, Mark; Wang, Shaochun (2002-12-01)
    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 news is that this ...
  • A Comparison of the BTT and TTF Test-Generation Methods

    Legeard, Bruno; Peureux, Fabien; Utting, Mark (Springer, 2002)
    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 Z specification. The B ...
  • Automated Boundary Testing from Z and B

    Legeard, Bruno; Peureux, Fabien; Utting, Mark (Springer, 2002)
    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 boundary values of that ...
  • Data structures for Z testing tools.

    Utting, Mark (University of Waikato, Department of Computer Science, 2001-06-01)
    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 undefined terms, simplification ...
  • Teaching formal methods lite via testing

    Utting, Mark; Reeves, Steve (John Wiley & Sons, Ltd., 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 specification and testing can ...
  • A survey of software development practices in the New Zealand software industry

    Groves, Lindsay; Nickson, Ray; Reeve, Greg; Reeves, Steve; Utting, Mark (2000-04)
    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 general questionnaire ...
  • A survey of software requirements specification practices in the New Zealand software industry

    Groves, Lindsay; Nickson, Ray; Reeve, Greg; Reeves, Steve; Utting, Mark (1999-06)
    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 general questionnaire ...

Showing up to 5 theses - most recently added to Research Commons first.

  • Automatic Parallelization of Data-Driven JStar Programs

    Weng, Min-Hsien (University of Waikato, 2013)
    Data-driven problems have common characteristics: a large number of small objects with complex dependencies. This makes the traditional parallel programming approaches more difficult to apply as pipe-lining the task ...
  • Parallelization of JStar Programs on a Distributed Computer

    Crosby, Simon Graeme (University of Waikato, 2012)
    In the past, the performance of sequential programs grew exponentially as the performance of CPUs increased with Moore’s Law. Since 2005 however, performance improvements have come in the form of more parallel CPU cores. ...
  • Patterns of Change: Can modifiable software have high coupling?

    Taube-Schock, Craig (University of Waikato, 2012)
    There are few aspects of modern life that remain unaffected by software, and as our day-to-day challenges change, so too must our software. Software systems are complex, and as they grow larger and more interconnected, ...