Softool 2011

UniTESK technology was presented at Softool 2011 on October 25-28 in All-Russian Exhibition Centre, Exhibition Hall №69, place E47.


The following exhibits were presented:

С++TESK test development tool

C++TESK is an open-source C++based tool intended for automated functional testing of RTL models of digital hardware. The main part of the tool is a library of classes and macros that define  facilities for constructing reference models of hardware, adapters of RTL models, test scenarios and test coverage metrics. Basing on C++ descriptions provided by a user, a testbench is compiled; it allows automatically generating and applying sequences of stimuli to the component under test, checking correctness of its reactions and collecting statistics on test execution. Besides the basic library, the tool includes a test report generator and a means for parallelizing test execution on computer clusters.

Linux device drivers verification system

The verification system is intended for detection of typical errors in source code of Linux device drivers. The system is based on static analysis of source code that allows finding hard to reproduce errors which occur in rare situations. One more important feature of the system is that you can verify a driver without having a real device. The verification system is now under development, but it have already helped to detect several dozen bugs in Linux device drivers which were accepted and fixed by driver developers. See bug descriptions at

KEDR - a Framework for Dynamic Analysis of Linux Kernel Modules KEDR is a framework for dynamic (runtime and post factum) analysis of Linux kernel modules, including device drivers, file system modules, etc. The components of KEDR operate on a kernel module chosen by the user. They can intercept the function calls made by the module and, based on that, detect memory leaks, simulate resource shortage in the system, save the information about the function calls to a kind of "trace" for future analysis by the user-space tools.  For the present, KEDR is provided for 32- and 64-bit x86 systems.  KEDR can be used in the development of kernel modules (as a component of QA system) as well as when analyzing the kernel failures on a user's system (technical support). It may also be valuable for the certification systems for device drivers and other kernel-mode components.  KEDR is free software and is distributed under the terms of GPL v2.

Hypervisor-based security system aimed to protect trusted applications inside untrusted environment

Sevigator is a protection system that allows to control execution of trusted applications inside untrusted environment. The system is aimed to preserve consistency and confidentiality of user data processed by applications. Sevigator is based on hardware-assisted virtualization technology which allows to use hypervisor to monitor different events inside operating system. Hypervisor itself is running with higher privileges than OS and thus is not vulnerable for attacks even from compromised OS kernel. At the same time, hypervisor is able to control access to hardware devices (such as network adapter or storage media) and to prevent unauthorized modifications of application address space.

Test suite «Mathematics»

Test suite «Mathematics» — is a suite of tests for mathematical functions of POSICX standard programming interface checking both implementation conformance to the standard and accuracy of results on a huge set of specifically selected test data. Test data sources for the suite are intervals of homogeneous behavior of the functions under test, boundary and special values of floating-point numbers, and numbers, for which accurate computation of a function value requires more than average effort. The test reports can present results both in a brief view and with detailed distribution of the errors detected and lists of most serious errors.

Test suite for kernel API of ARINC-653 real-time operating systems

Test suite for functional testing of various real-time operating systems (RTOS) on conformance with requirements of ARINC-653 standard in respect to the behaviour of the main interfaces of RTOS kernel. The test suite is based on automatic generation of tests from formal specifications of the standard's requirements. ISPRAS's own UniTESK technology is used to implement this approach. As a result of the project we have created requirements catalog, developed formal specifications and corresponding tests for 56 system APIs of RTOS kernel. The tests detected several dozens of inconsistencies with the ARINC-653 requirements in RTOS kernels that has declared successful passing of ARINC-653 Part 3 tests.

LSB certification tests

Within the scope of the LSB Infrastructure Program run by ISPRAS under a contract with the Linux Foundation certification tests were developed for GNU/Linux operating systems aimed to check if system libraries meet requirements of the Linux Standard Base (LSB). Certification tests cover low-level system libraries (in particular, libc), as well as for higher level components such as Qt or GTK+ stack. All the tests were developed using unique ISPRAS technologies - UniTESK (for high-quality, "deep" tests), T2C ("normal" tests) and API Sanity Autotest ("shallow" tests that only check the basic functionality).

Copyright © 2014 Institute for System Programming of the Russian Academy of Sciences