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.

Supporting the software testing process through specification animation

Achieving consistency between a specification and its implementation is an important part of software development. In this paper, we present a method for generating passive test oracles that act as self-checking implementations. The implementation is verified using an animation tool to check that the behavior of the implementation matches the behavior of the specification. We discuss how to integrate this method into a framework developed for systematically animating specifications, which means a tester can significantly reduce testing time and effort by reusing work products from the animation. One such work product is a testgraph: a directed graph that partially models the states and transitions of the specification. Testgraphs are used to generate sequences for animation, and during testing, to execute these same sequences on the implementation.

Site-directed mutagenesis and kinetic studies of the West Nile virus NS3 protease identify key enzyme-substrate interactions

The flavivirus West Nile virus (WNV) has spread rapidly throughout the world in recent years causing fever, meningitis, encephalitis, and fatalities. Because the viral protease NS2B/NS3 is essential for replication, it is attracting attention as a potential therapeutic target, although there are currently no antiviral inhibitors for any flavivirus. This paper focuses on elucidating interactions between a hexapeptide substrate (Ae-KPGLKR-p-nitroanilide) and residues at S1 and S2 in the active site of WNV protease by comparing the catalytic activities of selected mutant recombinant proteases in vitro. Homology modeling enabled the predictions of key mutations in VWNV NS3 protease at S1 (V115A/F, D129A/ E/N, S135A, Y150A/F, S160A, and S163A) and S2 (N152A) that might influence substrate recognition and catalytic efficiency. Key conclusions are that the substrate P1 Arg strongly interacts with S1 residues Asp-129, Tyr-150, and Ser-163 and, to a lesser extent, Ser-160, and P2 Lys makes an essential interaction with Asn-152 at S2. The inferred substrate-enzyme interactions provide a basis for rational protease inhibitor design and optimization. High sequence conservation within flavivirus proteases means that this study may also be relevant to design of protease inhibitors for other flavivirus proteases.

A graphical specification of model transformations with triple graph grammars

Models and model transformations are the core concepts of OMG's MDA (TM) approach. Within this approach, most models are derived from the MOF and have a graph-based nature. In contrast, most of the current model transformations are specified textually. To enable a graphical specification of model transformation rules, this paper proposes to use triple graph grammars as declarative specification formalism. These triple graph grammars can be specified within the FUJABA tool and we argue that these rules can be more easily specified and they become more understandable and maintainable. To show the practicability of our approach, we present how to generate Tefkat rules from triple graph grammar rules, which helps to integrate triple graph grammars with a state of a art model transformation tool and shows the expressiveness of the concept.

Formal analysis of human-computer interaction using model checking

Experiments with simulators allow psychologists to better understand the causes of human errors and build models of cognitive processes to be used in human reliability assessment (HRA). This paper investigates an approach to task failure analysis based on patterns of behaviour, by contrast to more traditional event-based approaches. It considers, as a case study, a formal model of an air traffic control (ATC) system which incorporates controller behaviour. The cognitive model is formalised in the CSP process algebra. Patterns of behaviour are expressed as temporal logic properties. Then a model-checking technique is used to verify whether the decomposition of the operator's behaviour into patterns is sound and complete with respect to the cognitive model. The decomposition is shown to be incomplete and a new behavioural pattern is identified, which appears to have been overlooked in the analysis of the data provided by the experiments with the simulator. This illustrates how formal analysis of operator models can yield fresh insights into how failures may arise in interactive systems.