UniTESK technology is designed to develop reliable test suites based on formal specifications. The technology was originally developed for testing application program interfaces (API), but due to the flexibility of its architecture, it is also applicable for testing other kinds of program systems. The technology has been developed in the Institute for System Programming (ISP) of the Russian Academy of Sciences (RAS)

UniTESK technology is based on use of formal specifications to describe requirements for the system under test. Specifications in UniTESK are expressed mostly in the form of constraints: preconditions and postcondition of operations and data integrity constraints. Axiomatic and executable specifications can be used as well, but require some extra work.

Requirements are described in a specification extension of common programming languages (such as C, C++, C#, Java). Specification extension enriches the basic programming language with special constructions, that make it possible to describe requirements to system under test and other components of the test system in a compact and handy form. It maximizes convenience of test suite development and minimizes training cost for developers, familiar with the basic language.

Formal specifications are used for automatic generation of test oracles that check consistency between behavior of the system under test and the requirements. Generated oracles allow to solve the problem of estimating correctness of the system under test in a reliable way.

UniTESK suggests a technique for test sequence construction based on finite state machine (FSM) models. In contrast to classical approaches, consisting in explicit definition of possible states and transitions, UniTESK technology uses implicit definition of FSM. It simplifies test development greatly and, at the same time, allows to reach high quality of testing due to specially developed algorithms of FSM traversal.

The quality of testing is carefully analyzed. Test coverage metrics are derived from formal requirements and are automatically tracked during the test run. It is possible to get a test coverage report on each test run.

High emphasis in UniTESK technology is placed on flexible architecture of test system and extensive reuse of its components, using specification description on several levels of abstraction and concept of refinement. Mediators ensure independence of specifications from technical details of the implementation.

UniTESK is not only a reliable technology for high quality tests development, but also allows to raise up the level of software development process as a whole. The formal specifications can be used in UniTESK technology for parallel development of both software and tests for it. Thus, it is the way to reduce the software development time and to use resources more regularly.

In addition testing systems modeled by standard finite-state machines, UniTESK supports nondeterministic state machines and state machines with postponed reactions. It allows to apply the technology to testing such complex systems as protocol stacks and distributed systems.