Software Engineering

Own Technologies

LDV. A technology for static verification of Linux kernel drivers

Bugs in Linux kernel drivers directly affect security, reliability and performance of the kernel and user space applications. Code review, automated testing and static analysis allows detection quite a lot of bugs in Linux kernel drivers. However, just static verification aims at identifying all bugs of a particular type. Configurable framework for static verification of Linux kernel drivers LDV KLEVER provides means for automated preparation of source code of drivers for verification on the base of environment model specifications and checking it against correctness rule specifications using static verification tools.


MicroTESK (Microprocessor TEsting and Specification Kit) is a framework for generating test programs in assembly language for functional verification of microprocessors. It uses formal specifications as a source of knowledge about the configuration of the microprocessor under verification. Generation tasks are described in a special Ruby-based language which allows formulating verification goals in terms of test situations derived from formal specifications. Such an approach simplifies configuring the framework and improves the level of test coverage. MicroTESK has been successfully applied in industrial projects for verification of ARMv8 and MIPS64 microprocessors.

Retrascope. Reverse engineering tool for HDL descriptions

HDL Retrascope is a toolkit for reverse engineering and transformation of digital hardware designs described in such HDLs (hardware description languages) as Verilog и VHDL. The toolkit allows analyzing HDL descriptions, reconstructing the underlying models (extended finite state machines, EFSMs) and using the derived models for test generation, property checking and other tasks. HDL Retrascope is organized as an extendable framework with the ability to add new types of models as well as tools for their analysis and transformation. The primary application domain of the toolkit is functional verification of hardware at the unit level.

MASIW. Software tools for development of Integrated Modular Avionics

MASIW – Modular Avionics System Integrator Workplace. This is the development environment providing tools to develop model of modular avionics of aircrafts, tools to performing analyzes of models for compliance to requirements and tools for generation of configurations data and binary images of program code based on models.

AstraVer Toolset. Deductive verification of Linux kernel modules and security policy models

Software plays a key role in many systems, e.g., safety-, security-, and missioncritical systems. Bugs in such software can lead to catastrophic consequences. As a result development of critical software is regulated by certification standards/guidelines (like DO-178С, ISO/IEC 15408, etc) that require following best practices in development process.


CTESK is a toolkit for testing applications developed in C. CTESK implements UniTESK concepts of automated testing based on specifications.


C++TESK Testing ToolKit is an open-source C++ based toolkit intended for automated functional testing of software components (mostly in C/C++) and RTL (HDL) models of digital hardware (in Verilog and VHDL).


System of management requirements Requality is tool for working with requirements, especially for software systems.


JavaTESK is a toolkit for testing applications developed in Java.


PyTESK is a technology of software testing based on formal specifications.


UniTESK is a technology for testing application program interfaces (API) which is primarily designed for unit testing.
UniTESK stands for Unified TEsting Specification based toolKit. UniTESK uniformity is provided by the fact that the common testing methodology and general architecture can be implemented for testing modules written in almost all programming languages. Currently there are UniTESK implementations for such languages as C (CTESK), C++ (C++TESK), Java (JavaTESK and Summer), Python (PyTESK).


SemaTESK (Semantics Testing Kit) is an automatic method for  generation of test sets for a translator front end.


OTK (Optimizer Testing Kit) is an automated test development tool for software using complex data structures.


SynTESK (Syntax Testing Kit) is a toolkit for testing parsers of formal languages.


RaceHound is a software for data race detection in Linux kernel modules.

Other technologies


KEDR is a framework for dynamic (runtime and post factum) analysis of Linux kernel modules, including device drivers, file system modules, etc.