About NAT2TEST

A strategy for generating test cases from natural language requirements.

NAT2TEST (NATural language requirements to TEST cases) is a completely automatic strategy for generation of test cases from natural language requirements, which might consider discrete or continuous temporal properties. Automation is essential for this task, since we cannot expect that practitioners will always have formal modelling knowledge. Automation also allows an early application of formal methods within the software development process.

This strategy is particularly tailored for reactive systems whose behaviour can be described as actions that should be taken when particular conditions are met. Test cases are generated possibly using commercial tools (like T-VEC and RT-Tester) or based on a formal conformance relation using tools like FDR and Z3, in which case the test generation is proved sound.

The NAT2TEST tool, which supports the strategy with same name, is written in Java, and its Graphical User Interface (GUI) is built using the Eclipse RCP framework. The tool can be easily installed and runs on multiple platforms.

First, one needs to manually write the system requirements according to a controlled natural language, which is a subset of English with a well-defined grammar. For each relevant domain of application, a dictionary is defined (and evolved) to classify the words according to their grammatical classes.

Afterwards, a series of automatic steps process the requirements to generate test cases; namely, syntactic and semantic analyses, and generation of an internal model, for instance, a DFRS, which stands for Data-flow Reactive System – a formal representation of the system behaviour.

Finally, with the aid of other tools, automatic test cases are generated. A test case (see below) is a sequence of test vectors, each one being a sequence of values of inputs and expected outputs over the time.

NAT2TEST tool

Features

Main features supported by the NAT2TEST tool.

  • Guidance when writing requirements according to a controlled natural language.
  • Definition of aliases to promote text reuse.
  • Creation of domain-specific dictionary.
  • Semantic interpretation of requirements based on the Case Grammar linguistic theory.
  • Inference of underlying formal model to give semantics to system requirements.
  • Traceability information between formal model and requirements.
  • Animation of requirements via underlying formal model.
  • Generation of SCR (Software Cost Reduction) specification from underlying formal model.
  • Generation of CSPM (Communicating Sequential Processes) specification from underlying formal model.
  • Generation of test cases from CSP model with requirement coverage criteria.
  • Generation of Coq specification from underlying formal model.
  • Generation of test cases from Coq specification.
Guidance when writing requirements according to a controlled natural language Definition of aliases to promote text reuse Creation of domain-specific dictionary Semantic interpretation of requirements based on the Case Grammar linguistic theory Inference of underlying formal model to give semantics to system requirements Traceability information between formal model and requirements Animation of requirements via underlying formal model Generation of SCR specification from underlying formal model Generation of CSPm specification from underlying formal model Generation of test cases from CSP model with requirement coverage criteria

Download

System requirements: Linux (x64) + Java (x64) >= 1.7

License: the NAT2TEST tool is only freely available for academic teaching and research purposes.

For all other uses please contact us to discuss licensing options.

  • Installation steps:
    1. Download and extract the NAT2TEST tool: link;
    2. Download and install FDR2 (Linux x64): external link;
    3. Download and install Z3 (Linux x64): external link;
  • To run: double-click on "F/nat2test/Nat2Test", (F = folder where the NAT2TEST tool was extracted)
  • Examples available for download:
    1. NPP -- Nuclear Power Plant Control system: link
      • A toy example with no temporal properties.
    2. VM -- Vending Machine system: link
      • A toy example with temporal properties.
    3. TIS -- Turn Indicator System: link
      • Example inspired by the benchmark freely provided by Daimler.
  • Important notes:
    1. Before using the NAT2TEST tool, we suggest reading the "Overview" and the "Tutorial" available in the tool.
    2. To generate test cases, remember to set the FDR and Z3 path in "General Info" (in the "Navigation View").
    3. When animating the DFRS or generating test cases, it is reasonable to do so from its initial state.
      • For the available examples, after generating the DFRS, open "Variables and Types" and change:
        • VM: "the_system_mode" to "idle"
        • NPP: "the_safety_injection_mode" to "on"; "the_pressure_mode" to "low"
        • TIS: "the_indication_lights" to "off"; "the_flashing_mode" to "no flashing"
          • Append ", 81" to the values of "the_voltage" (double-click on "Expected Values").
      • Afterwards, open the "Animation" screen and generate the CSPM model ("Generate CSPm").

If you have any doubts or face any problems, please do not hesitate to contact us at: ghpc AT cin DOT ufpe DOT br.

Contact Us

Please do not hesitate to contact us at: ghpc AT cin DOT ufpe DOT br. Thank you for your attention.