Innovations

Astraver Verification Toolset

AstraVer Toolset is a deductive verification system for key software components. It allows developing and verifying security policy models as well as proving the correctness of software modules written in the C programming language. AstraVer is essential for ensuring the required trust levels from ADV_SPM and ADV_FSP assurance families as defined in the ISO/IEC 15408 standard.

TestOS: software testing environment

TestOS is an environment for unit testing of software on target hardware. It allows to debug software for critical applications on ARM, PowerPC, MIPS and x86 architectures to perform certification and other activities.

MASIW: support for designing highly reliable software systems

MASIW is a toolset for developing highly reliable hardware and software systems for avionics, medicine, and other safety critical areas. It is designed for engineers creating airborne hardware/software systems that are developed using the integrated modular avionics (IMA) approach. MASIW can be easily adapted for other application areas.

MicroTESK: a test program generator

MicroTESK is a reconfigurable and extendable framework for generating test programs for functional verification of microprocessors. MicroTESK allows automatically constructing test program generators based on formal specifications of microprocessor architectures. MicroTESK supports a wide range of architectures including RISC, CISC, VLIW, and DSP. MicroTESK supports online test program generation.

Retrascope: static analysis of hdl descriptions

Retrascope is a functional verification toolkit for digital hardware designs. Retrascope provides automated engines for code analysis, formal model extraction and functional test generation. The toolkit accepts digital hardware module descriptions as inputs, written on the synthesizable subset of Verilog and VHDL languages, as well as their behavioral specifications.

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.

Klever: a verification framework for models of industrial software

Klever is a framework for verifying models that are automatically extracted from large software systems’ source code written in the C programming language. Klever allows specifying various security and safety requirements and verifying them automatically with the preconfigured precision level.