Everest

conformancE Verification on tEsting ReactivE SysTems

Everest

Everest is a practical tool to check whether an implementation complies with its respective specification, and also generate complete test suites. The conformance checking is provided in a white-box testing mode, where the internal implementation behavior is known. Implementations can be checked against their respective specifications based on a more general conformance relation using regular languages. The classical IOCO relation is a particular case of the new conformance relation and it is also provided by the tool. Moreover, our tool can generate test suites in practical black-box testing scenarios.

Development

Everest is developed in Java and composed by four modules: View, Parser, Automaton Construction, and Verification & Generation. Arrows indicate the data flow among the modules.

The Swing library is used in the View module to create the interface that deals with input and output data. The user can provide IUTs and specification models in Aldebaran format, the conformance verification mode, IOCO or language-based, the regular expressions that model (un)desirable behaviors, and the number of test cases to be generated. Verdicts of conformance testing and the associated details are produced by the tool on conformance verification. In the test suite generation can also be informed an upper bound on the number of states of implementations to be covered, multi-graph and TPs can also be provided for the test generation and execution.

The Parser module checks if the IUT and the specification models given in Aldebaran files are valid. The Automaton construction module gets underlying automaton from IOLTS/LTS model and also the automaton that recognizes the regex received by the view. The process of checking conformance between IUT and specification, and test generation/run is performed by the Verification & Generation module.

Aldebaran format (.aut)

An example of Aldebaran file format and its corresponding model. Input labels are tagged by '?', and output labels are tagged by '!'.

The header indicates the initial state, the number of transitions and the number of states, respectively.

Each line below the header is a transition, which is defined as a tuple (s,l,p), where 's' is source state, 'l' is the label of transition and 'p' is the target state

Interface - Configuration

Fields:

  • Model: inform the path where the specification model is in .aut file
  • Implementation: inform the path where the implementation model is in .aut file
  • Model type: the models of implementation and specification are IOLTS ou LTS;
  • Label: if the models are IOLTS must inform how to distinguish the inputs and output label, it's possible to do automatically if .aut file contains a label with tag '!' and '?', or inputs and outputs labels can be manually informed;
  • Input/output: these fields will appear if is choose to inform manually the input and output labels of IOLTS;

Interface - IOCO Conformance

  • view model/view IUT: graphically display the model and IUT;
  • input labels/output labels: partitioning between input and output labels in case of IOLTS models, or just the labels in case of LTS;
  • # Test cases: the number of test cases to be generated in case of verdict of non-conformance
  • verify: clicking on the button will verify that the implementation complies with the specification. The conformance verdict is displayed in front of the button. In the case of non-conformance, Everest show test cases in the text area below;
  • warnings: displays a message informing empty fields or incorrectly filled fields;

Interface - Language-Based Conformance

Fields:

  • view model/view IUT: graphically display the model and IUT;
  • input labels/output labels: partitioning between input and output labels in case of IOLTS models, or just the labels in case of LTS;
  • Desirable behavior: represents the desired behavior of implementation express in regex;
  • Undesirable behavior: represents the undesired behavior of implementation express in regex;
  • # Test cases: the number of test cases to be generated in case of verdict of non-conformance
  • verify: clicking on the button will verify that the implementation complies with the specification. The conformance verdict is displayed in front of the button. In the case of non-conformance, Everest show test cases in the text area below;
  • warnings: displays a message informing empty fields or incorrectly filled fields;

Interface - Test Generation & Run

  • view model/view IUT: graphically display the model and IUT;
  • input labels/output labels: partitioning between input and output labels;
  • #Max IUT states: upper bound on the number of states of black-box implementations to be covered;
  • # Test purpose: the number of test purposes to be generated in case of non-conformance verdict;
  • Multigraph: the path where the multigraph is (.aut file) to generate and run the tests;
  • Test purpose folder: the directory containing the test purposes to be run;
  • Generate: clicking on the button will generate the multigraph;
  • Test Generation + Run: clicking on the button will generate the multigraph and test purposes;
  • Run: clicking on the button will generate the test purposes and run on implementation;
  • Run TPs: clicking on the button will run the test purposes on implementation;
  • warnings: displays a message informing empty fields or incorrectly filled fields;

Bytecode

Everest is developed in Java and the Bytecode is available for download click here.

Source Code

The source code is available on the Gitlab Repository click here.

IOLTS Models

download IOLTS(.aut)

download IOLTS(.aut)

download IOLTS(.aut)

Configuration View

Using the above models, the configuration view must be filled in according to the figure on the side. The models are IOLTS. In .aut file, the input labels are started with '?' and output labels with '!'

Examples

Example 1: The IOCO verification between the S and R models result in non-conformity, and the test cases generate are {b,aa,ba,aaa,ab,ax,abb,axb}.

Example 2a: The IOCO verification between the S and Q models result in conformity.

Example 2b: The language-based conformance verification using the models S, Q and regex D=(a|b)*ax and F=∅, result in non-conformity verdict, and the test cases generate are {ababax, abaabax}.

Example 3a: The mutigraph generation using specification S, and the coverage of implementations with up to 4 states.

Example 3b: The test purpose generation using multigraph (generated in Example 3a) and run on implementation R. The tool detected a fault when generated and executed the third test purpose.

Example 3c: The test run using the test purposes at the 'TPs' folder (generated in Example 3b), and run on implementation R. A fault was found.