Browsing by Author "Utting, Mark"

Now showing items 1-5 of 29

  • 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 ...
  • Bound analysis for Whiley programs

    Weng, Min-Hsien; Utting, Mark; Pfahringer, Bernhard (Elsevier, 2015)
    The Whiley compiler can generate naive C code, but the code is inefficient because it uses infinite integers and dynamic array sizes. Our project goal is to build up a compiler that can translate Whiley programs into ...
  • 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 ...
  • 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 ...
  • 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 ...

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

  • Efficient compilation of a verification-friendly programming language

    Weng, Min-Hsien (The University of Waikato, 2019)
    This thesis develops a compiler to convert a program written in the verification friendly programming language Whiley into an efficient implementation in C. Our compiler uses a mixture of static analysis, run-time monitoring ...
  • 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, ...