The main ideas of the UniTESK technology are as follows:

  • The well-known Design by Contract approach is used to represent formal specifications. Program contracts consist of preconditions and postconditions of interface operations and data type invariants. On the one hand, program contracts are convenient for software developers since they are closely related to the architecture of the software; on the other hand, owing to their representation they stimulate efforts to formulate implementation-independent correctness criteria of the target system. The main advantage of program contracts is that they enable automatic construction of test oracles that check the conformance of the target system behavior to the specifications.
  • The structure of contracts is also used to define test coverage criteria, which are necessary to evaluate the quality of testing from the viewpoint of the requirements for the target software. To make possible automatic extraction of such criteria, additional operators for defining functional branches are introduced. A functional branch corresponds to a subdomain of the “same” behavior in the operation domain. We may assume that the behavior is “the same” if the constraints imposed on the operation's results and on the change of state are described by the same expressions in the postcondition for all points of the subdomain.
  • To automatically construct sequences of test inputs, the system under test is modelled as a finite state machine (FSM). A test sequence is generated as a sequence of calls of target operations corresponding to a path in the state transition graph of the FSM; for example, it can be a transition tour on the FSM. Since the FSM model is used only to generate a test sequence rather than to verify the behavior of the target system, which is performed by oracles, the FSM does not need to be completely defined. It is sufficient to specify a way for identifying its states and a method for iterating through inputs depending on the current state. FSMs in such an implicit way can be conveniently represented in the form of test scenarios.

The table below presents UniTESK process of specification development, test development and testing. The process is presented as a sequence of steps, but in practice it often becomes necessary to return to some of the previously performed steps and to revise the decisions made. So, the actual process is iterative, but its matter is a move from requirements to tests and test results analysis.

1. Analysis of functional software requirements on the base of documents available or knowledge and expertise of project participants and experts, transformation of requirements into formal specifications.
2. Formulation of requirements to testing quality as a level of test coverage to achieve. After achieving this coverage level the testing can be finished.
3. Development of test scenarios set that ensures the achievement of the target coverage level. Scenarios are developed on the base of specifications and are not related with some specific implementation of target system or its specific version.
4. Binding specifications with the target software interface. The set of mediators should be developed for that.
5. Test system construction. To obtain a ready-for-use test system specifications, mediators, and test scenarios should be translated into target programming language and then compiled into binaries.
6. Test execution with debugging of specifications, mediators, scenarios.
7. Test results analysis. The testing quality should be assessed on the base of coverage criteria stated before. After that we can return to test scenario development to achieve higher coverage, or can finish testing and develop a report describing errors detected.

Details on the UniTESK technology and supporting tools are presented at http://www.unitesk.com/.