Open-Source Projects

Aspect-oriented Tracing facility.

Provides extensible trace format specification and framework for creating traces, analyzing them and creating modularizable reports. Supports pluggable independent libraries of message types (each library presents its own "aspect"), facilitates merging and linking data from different aspects and converting it into mutually-linked report entities....

Набор инструментов для верификации моделей политик безопасности и их реализаций в ответственных системах.

• Инструменты дедуктивной верификации моделей политик безопасности...

Расширяемый инструментарий для анализа процесса сборки программных проектов.
Основная область применения на начальном этапе - извлечение информации о структуре Си программ с целью их последующего анализа.

Gradle-based build system for Eclipse projects

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). The main part of the toolkit is a library of C++ classes and macros that define facilities for constructing formal specifications (reference models), adapters of components under test, test scenarios and test coverage metrics. Basing on C++ descriptions provided by a user, a test system 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 toolkit includes a report generator, means for parallelizing test execution on computer clusters, and Eclipse-based IDE....

Castle (Control flow & Abstract Syntax Tree Library, Etc.) is a simple library for developing translators and code generators.

Licensing and Distribution¶

The Castle package is distributed under the Apache License, Version 2.0, which implies the freedom to use the software for any purpose (to distribute it, to modify it and to distribute modified versions of the software) under the terms of the license, but requires preservation of the copyright notice and disclaimer....

C Instrumentation Framework is a tool that implements aspect-oriented programming for the C programming language. You can find more information about it in paper An approach to implementation of aspect-oriented programming for C.

CIF documentation: https://cif.readthedocs.io....

Clade is a tool for intercepting build commands (stuff like compilation, linking, mv, rm, and all other commands that are executed during build). Intercepted commands can be parsed (to search for input and output files, and options) and then used for various purposes:...

Base Eclipse plugins for integration of additional languages.

Library managing hierarchical coverage structures and annotated Java descriptions for them.

UniTESK technology for C programming language

CTESK depends on UniTESK Reports for test trace processing and report generation.

Прототип архитектуры инструмента моделирования, основанной на использовании и композиции полиморфного строго типизированного чисто-функционального кода

Работа поддержана грантом РФФИ №17-01-00504

Публикации, связанные с проектом
...

Курс "Формальные методы верификации программ" / "Верификация ПО. Часть 2" (читается с осени 2013 года).

Fortress (FORmula TRanslation, Evaluation and Symbolic Simplification), former JCSA (Java Constraint Solver API), is an open-source and extendable Java library providing facilities for manipulation with formulae (terms and constraints). The library allows creating formulae (in the form of syntax trees), translating them into external formats (programming languages, XML, SMT-LIB, etc.), evaluating them and doing symbolic simplification. It also supports constraint solving using built-in solvers as well as external ones (like Yices, Z3, CVC4, Boolector, etc.). For more information, read Wiki....

Набор инструментов тестирования сетевых сервисов на основе формальных спецификаций
(см. Repository (Хранилище) -> README.md).

Java 5 frontend consists of syntax checker (parser) building AST and semantic checker verifying static semantics.

Note: Semantic checker implementation is in JavaTESK project as a part of semantic checker for the extension of Java language. It will be extracted when we have enough resources....

JOGS provides facilities for flexible processing of graphs of Java objects.
It's capable of "remembering", "restoring", and "comparing" state(s) of the whole object graph without
creating new instances of classes involved in the graph structure.

Java SoftFloat is a Java implementation of the Berkeley SoftFloat library, a free, high-quality software implementation of binary floating-point that conforms to the IEEE Standard for Floating-Point Arithmetic. As the original version, Java SoftFloat fully implements four floating-point formats: 32-bit single-precision, 64-bit double-precision, 80-bit double-extended-precision, and 128-bit quadruple-precision....

UniTESK technology for Java programming language

JavaTESK depends on UniTESK Reports for test trace processing and report generation.

Kartographer is designed to build a call graph of the Linux kernel for a given configuration. It also collects information about macros, function pointers, object and source files.

Besides the Linux kernel, Kartographer can be used in other projects written in C....

MicroTESK is a reconfigurable (retargetable and extendable) model-based test program generator (TPG) for microprocessors and other programmable devices (such kind of tools are also called instruction stream generators or ISG). The generator is customized with the help of instruction-set architecture (ISA) specifications and configuration files, which describe parameters of the microprocessor subsystems (pipeline, memory and others). The suggested approach eases the model development and makes it possible to apply the model-based testing in the early design stages when the microprocessor architecture is frequently modified....

Mozilla XULRunner packaged as Eclipse-plugin

Update site: http://forge.ispras.ru/repo/xulrunner-eclipse/site/

Data Race Detector for Linux Kernel

KEDR is an extensible system for dynamic (runtime and post factum) analysis and verification of Linux kernel modules. KEDR tools operate on the modules chosen by the user and can perform function call monitoring, fault simulation, memory leak detection and more....

Klever is a software verification framework that aims at automated checking of programs developed in the GNU C programming language against a variety of requirements using software model checkers (automatic software verification tools) implementing such methods of thorough static analysis as Bounded Model Checking and Counterexample-Guided Abstraction Refinement. Software model checking allows finding faults that can be hardly detected by other software quality assurance techniques like code review, testing and static analysis. In addition, it is capable to prove formal correctness of programs checked against particular requirements under certain assumptions....

A C library for high-precision floating-point computations.

The library is designed to be compatible with a standard libm library. Just change the -lm compiler option to -lunifloat -fno-builtin when building your application and you'll get high-precision versions of trigonometric (sin, tan, ...), bessel (jn, yn, ...) and other functions declared in the standard math.h header file....

This page is a development portal of the Linux Driver Verification project. The aim of LDV is to build a comprehensive application suite for static verification of source code of Linux device drivers, and monitoring their quality....

Материалы, посвящённые созданию Технологического центра исследования безопасности ядра Linux.

По всем вопросам пишите:
khoroshilov@ispras.ru

Local site support. Please follow Site Information And Rules.

Данный проект посвящен задаче верификации разделения ресурсов в операционных системах для встроенных систем.
Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта №16-01-00356.

Научный отчет...

Курс "Верификация моделей программ" для студентов 1-ого курса магистратуры ВМиК (читается с февраля 2016 года).

NJL (Native Java Launcher) is platform-dependent launcher for Java applications.
This launcher is written in C and can be ported to many platforms.
NJL reads Java classpath and command-line options from configuration file to make Java application command-line much simpler....

Preliminary manual translations of verified C/ACSL functions into Imperative HOL

A set of Isabelle proof methods and commands that facilitates the use of relatively complete decision procedures (e.g. SMT solvers and paramodulation-based provers) with deterministic quantifier instantiation based on bounded E-matching. More about TSMT is explained in the TSMT Tutorial....

QEMU4V ("QEMU for Verification") is an open source emulator for assembler programs that is based on QEMU project. The tool performs emulation for programs of several hardware architectures and provides some features (tracing, etc.) for system verification of microprocessors....

Requality is an open source Eclipse-based Requirements Management Tool that supports both development of requirements from scratch as well as recreation of a hierarchy of requirements from existing documents. Requality keeps linkage between a requirement and fragments of documents that became a source for the requirement that makes Requality very attractive for reverse engineering of requirements. Another important feature of the tool is a support for Requirements-based Test Purpose Design....

Retrascope is a toolkit for Reverse Engineering, visualization and TRAnsformation of digital hardware designs described in such HDLs (hardware description languages) as Verilog and VHDL. The toolkit allows analysing HDL descriptions, reconstructing and visualization of the underlying models (extended finite state machines, EFSMs) and using the derived models for test generation, property checking and other tasks. 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....

Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы.

Semantic Testing Kit

Syntax Testing Kit

TestBase is a knowledge base used for test data generation. It stores data constraints and generators and handles user queries to build test data providers.

UNDER CONSTRUCTION

Licensing and Distribution¶

The TestBase package is distributed under the Apache License, Version 2.0, which implies the freedom to use the software for any purpose (to distribute it, to modify it and to distribute modified versions of the software) under the terms of the license, but requires preservation of the copyright notice and disclaimer....

Experimental track finding tools for the MPD detector of the NICA project.

Test trace processing tools and report generators

The library for testing of translators (input files -> output files) using TestNG.

Verilog Translator (VeriTrans) is an ANTLR-based Verilog front-end in couple with some back-ends.

Licensing and Distribution¶

The VeriTrans package is distributed under the Apache License, Version 2.0, which implies the freedom to use the software for any purpose (to distribute it, to modify it and to distribute modified versions of the software) under the terms of the license, but requires preservation of the copyright notice and disclaimer....

A simple utility aimed at generating C-Verilog synchronization components of a test environment:

table=. {font-style:italic; font-weight:bold; background:#dddddd}. |<. Component |<. Description | |<. Testbench |<. a Verilog wrapper around the DUT that generates a clock signal, launches a test scenario, and does cycle-by-cycle synchronization w/ the test environment |...

VerKer: Verification of Linux Kernel Library Functions

See more details in our wiki.

MASIW Framework is an open source Eclipse-based IDE for development and analysis of AADL models. It is developed by ISPRAS in cooperation with GosNIIAS.

• textual and graphical editors for AADL model;...

Выкладываются электронные материалы конференций и семинаров, в работе которых мы участвовали

Проекты автоматизированного тестирования программных интерфейсов с использованием моделей. В качестве фреймворка для тестов используется библиотека Summer.