Open-Source Projects

The new release contains the following changes:

• The logic of test sequence building and processing has been improved
• The format of generated test programs has been improved
• Several bug fixes and general improvements have been made

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files

The new release contains the following changes:

• Several bug fixes and general improvements have been made

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files

The new build contains the following changes:

• Convenience methods simplifying access to expression value and type information were implemented
• The expression transformer facility was enhanced
• The possibility to control the order of visiting operands of an expression was implemented

The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files

Version 0.17 of Requality has been released, with some new important additions and fixes.

• A brand new update processor that allows to automatically markup requirements in a new version of a document that has been manually marked up before. As a result of the update processor execution each requirement having a location in the old version of the document gets the corresponding location in the new version if the processor detects it.
• A new sorting method that orders requirements by positions of their locations in the original document.
• A new builtin report template that presents coverage information by coloring text of original requirement document.
• Progress bar and ability to cancel document processors.
• API interface to develop user-specific document processors.
• Warning message if there are no available browser engines detected by Requality.
• Improvements in markup support:
  • behaviour of locations-related operations is consistent now in both cases when Req Marker is open and when it is not;
  • performance of markup-related operations improved on large documents.
• Usage of css classes instead of 'bold', 'underlined' and 'italic' tags in document importer.
• EXPERIMENTAL support for requirements and test cases parametrization and re-use. It allows
  • to reuse requirements subtree in several places;
  • to generate uniform elements (requirements or test cases) using parameterized patterns and iterators.

A complete list of changes can be found in changelog.

• Compatibility with Linux kernel 3.17-3.19.
• Improvements in 12 existing rule specifications:
  • sysfs_attr_init() call before device_create_file() call.
  • usb_deregister()/usb_serial_deregister().
  • Usb alloc/free urb.
  • Possible TTY NULL dereference.
  • Atomic allocation in interrupt context.
  • Memory allocation inside spinlocks.
  • NOIO allocation under usb_lock.
  • Initialization of completion.
  • Locking and unlocking SDIO bus.
  • Underflow in call copy_from_user() etc.
  • All allocated socket buffers should be freed.
  • Error handling in probe().
• Verification on a remote host using BLAST in a Docker container.
• Verification in the CPAchecker cloud.
• Support of Public Pool of Bugs.
• Many bug fixes and several new features in Rule Instumentor and CIF - LDV Tools components used to weave specifications into source code under verification.
• Numerous improvements and bug fixes in components for uploading and visualizing verification results.

Results of validation of LDV Tools 0.7 and LDV Tools 0.6 with different verification tools on 41 known bugs in the Linux kernel are presented in the table below.

Both BLAST and CPAchecker were able to find two more reference bugs thanks to improvements in rule specifications sysfs_attr_init() call before device_create_file() call and usb_deregister()/usb_serial_deregister().

The source code repository can be browsed by v0.7 tag. To get and to install LDV Tools see instructions.

Vitaly Mordan successfully finished Google Summer of Code 2014 project Public Pool of Bugs in Linux Kernel Modules under Evgeny Novikov supervision.

• Wrote a comprehensive specification of Public Pool of Bugs in which all requirements of LDV Tools developers for that project were considered.
• Extended linuxtesting.org in order to present LDV Tools verification results beyond the ISP RAS. New web pages were developed to represent full information about found bugs/false alarms (for the Linux kernel developers) and to edit information (for the LDV Tools developers).
• Extended LDV Knowledge Base and LDV Analytics Center in order to make it possible to publish verification results (such as kernel version, module, corresponding error trace, verdict, etc) to linuxtesting.org and to synchronize them later.
• Developed an authorization module for LDV Analytics Center to exclude an accidental publishing of unnecessary data, so only authorized users could publish verification results.

All changes to LDV Tools components were merged to master in 363f810.

Completing this project made possible to share any new found potential bugs in Linux kernel modules with its full description with the Linux kernel developers. In future this project will increase the number of found bugs in Linux kernel modules with the help of LDV Tools.

The new release contains the following changes:

• Facilities to describe data segment in test templates were implemented
• Function 'trace' (nML) was supported
• Possibility to create instances of modes and ops in nML code was implemented
• Aliases for memory locations (mem, reg, var) were supported
• Specification of the miniMIPS ISA was added to the examples

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files

The first build of the HDL Retrascope IDE has been released.

The Retrascope IDE is implemented as an Eclipse IDE plugin. The main function of the environment is configuration and launching of Retrascope engines. For more information, see Installation Guide and Getting Started.

The tool can be downloaded from here: http://forge.ispras.ru/projects/retrascope-ide/files

You are welcome to report bugs and leave your feedback at the main project site: http://forge.ispras.ru/projects/retrascope

We are happy to announce the first build of the HDL Retrascope toolkit.

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.

To reconstruct EFSM models and generate tests for them, Retrascope requires the SMT-solver be installed. See Installation Guide for more information.

In the 0.1.1 build the following features have been implemented:

- Support for VHDL/Verilog little-size designs (without iteration loops/functions/sub-modules);
  - Support for control flow graph (CFG) construction;
  - Support for CFG visualization in GraphML format;
  - Support for interface signals extraction from CFG;
  - Support for guarded actions decision diagram (GADD) construction;
  - Support for GADD visualization in GraphML format;
  - Support for extended finite state machine (EFSM) extraction;
  - Support for EFSM visualization in GraphML format;
  - Support for read/write conflicts extraction from EFSM;
  - Support for conflicts saving into XML format;
  - Support for test sequences generation for EFSM;
  - Support for test sequences saving into VHDL testbenches/XML format.

The tool can be downloaded from here: http://forge.ispras.ru/projects/retrascope/files

You are welcome to report bugs and leave your feedback at the main project site: http://forge.ispras.ru/projects/retrascope

Merry Christmas and Happy New Year!

The new release includes the following changes:

• Methods for converting BitVector from and to BigInteger
• Class NodeBinding that provides support SMT-LIB let-constructs
• Basic support for managing symbolic S-expressions
• Support for arbitrary size integers (LOGIC_INTEGER is based on BigInteger)
• Textual representation of a constraint is included in error log when solver fails
• Utility method ExprUtils.isSAT for checking satisfiability of expressions
• Utility method ExprUtils.getVariables for getting the list of variables contained in an expression
• Class CollectionUtils that contains utility methods for manipulating collections
• Class ConstraintUtils that provides methods to simplify creating and solving constraints
• Improvement in solver implementation that allows interpreting boolean operands of bit vector operators as bit vectors of length 1
• Debug and silent modes for SMT solvers (in the silent mode .smt files are not saved in file system after a constant has been solved)
• Support for the BVEXTRACT operator in expression type calculation logic
• Class DataMap for representing data of the MAP type
• New rules for expression transformation in the predefined rule set

The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files