Projects

Development of test sets for math libraries

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.

Summer

Summer is a Java-based test development and test execution framework similar to JUnit and TestNG, but supporting model based testing techniques (like NModel for C#).

Linux Driver Verification (LDV)

Linux Driver Verification (LDV) program is aimed to meet increased demand for large-scale verification tools applicable to high profile software.

Technology for integration testing in large information systems

The project conducted in partnership with JSC "VimpelCom" is aimed at development of software testing practices at the level of enterprise information system as a whole. The project covers a wide variety of topics: from requirement gathering for legacy-systems to coverage analysis in end-to-end system testing.

UniTESK

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).

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.

MicroTESK: a test program generator

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.

MASIW. Software tools for development of Integrated Modular Avionics

The Modular Avionics System Integrator Workplace framework is intended to automate the design of real-time aviation electronics systems based on Integrated Modular Avionics (IMA) architecture.

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.

Development of a system for functional verification of the L3 cache of the "Processor 1" project using the C++TESK tool.

Development of systems for standalone functional verification of the L3 and DB devices of the "Processor 1" and "Processor 2" projects using the C++TESK tool.

LSB Infrastructure Program

LSB Infrastructure was run by ISPRAS under a contract with the Linux Foundation. The project started in September 2006 and was targeted at long term partnership to advance LSB infrastructure quality and usability for supporting the rapidly growing LSB community. The key ISPRAS areas in the project included LSB Infrastructure Tools (this is to develop and later on maintain and mature various infrastructure tools to support LSB development and promotion), Linux Testing, various investigation and analytical work to find and fix various LSB related issues, perform data mining and prepare decision making materials.