A framework and tool support for the systematic testing of model-based specifications

Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively. This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.

Effects of phytase supplementation of diets with two tiers of nutrient specifications on growth performance and protein efficiency ratios of broiler chickens

in two feeding experiments male and mixed-sex broiler chicks were offered diets based on sorghum and a wheat-sorghum blend with two tiers of nutrient specifications, without and with microbial phytase (600 and 800 FTU/kg), from 7-25 and 1-42 days post-hatch, respectively. The nutrient specifications for protein, amino acids, energy density and phosphorus (P) of standard diets were reduced to formulate the modified diets on a least-cost basis. Calculated differences in nutrient specifications between standard and modified diets ranged from 14.3 to 17.1 g/kg crude protein, 0.24 to 0.40 MJ/kg apparent metabolisable energy (AME) and 1.06 to 1.20 g/kg available P. In both experiments, reduced nutrient specifications had a negative impact on growth rates and feed efficiency and phytase supplementation had a positive influence on growth performance and protein efficiency ratios (PER). Phytase addition to the less expensive, modified diets either partially or entirely compensated for reduced growth performance and, consequently, feed costs per kg of live weight gain were reduced. In Experiment 1, phytase increased (p<0.001) nitrogen-corrected AME (AMEn) from 15.39 to 15.89 MJ/kg dry matter. For nitrogen (N) retention there was an interaction (p<0.05) between diet type and phytase as the effects of phytase on N retention were more pronounced in the modified diets, with an increase from 0.512 to 0.561. These results demonstrate the positive effects of phytase on protein and energy utilisation, in addition to its established liberation of phytate-bound P and illustrate the feasibility of assigning nutrient replacement values to the feed enzyme for consideration in least-cost ration formulations. Further work is, however, required to define the most appropriate reductions in nutrient specifications in association with phytase supplementation.

Refactoring object-z specifications

Object-Z offers an object-oriented means for structuring formal specifications. We investigate the application of refactoring rules to add and remove structure from such specifications to forge object-oriented designs. This allows us to tractably move from an abstract functional description of a system toward a lower-level design suitable for implementation on an object-oriented platform.

Model checking Z specifications using SAL

The Symbolic Analysis Laboratory (SAL) is a suite of tools for analysis of state transition systems. Tools supported include a simulator and four temporal logic model checkers. The common input language to these tools was originally developed with translation from other languages, both programming and specification languages, in mind. It is, therefore, a rich language supporting a range of type definitions and expressions. In this paper, we investigate the translation of Z specifications into the SAL language as a means of providing model checking support for Z. This is facilitated by a library of SAL definitions encoding the Z mathematical toolkit.

Tool support for generating passive C++ test oracles from object-z specifications

A test oracle provides a means for determining whether an implementation behaves according to its specification. A passive test oracle checks that the correct behaviour has been implemented, but does not implement the behaviour itself. In previous work, we have presented a method that allows us to derive passive C++ test oracles from formal specifications written in Object-Z. We describe the "Warlock" prototype tool that supports the method. Warlock is built on top of an existing Object-Z type checker and generates oracle code for a substantial subset of the Object-Z language. We describe the architecture of Warlock and its application to a number of Object-Z specifications. We also discuss its current limitations.

Animation of object-z specifications using a Z animator

We discuss a methodology for animating the Object-Z specification language using a Z animation environment. Central to the process is the introduction of a framework to handle dynamic instantiation of objects and management of object references. Particular focus is placed upon building the animation environment through pre-existing tools, and a case study is presented that implements the proposed framework using a shallow encoding in the Possum Z animator. The animation of Object-Z using Z is both automated and made transparent to the user through the use of a software tool named O-zone.