Open-Source Projects

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

The new features include:

• Multiselection in Requality Explorer. Now you can perform operations with multiple nodes at once!
• Export of self-contained reports.
• On-disk format versioning of Requality projects. In case of introduction of a new on-disk format Requality will warn you and offer to convert an old project. If your project requires newer Requality version you will be warned as well.
• Hot-keys for copy, paste and move operations in Requality Explorer.
• Informative diagnostic of paste and move operation failures in Requality Explorer.

Also various bugs has been fixed in:

• Move, copy/paste and delete operations.
• Undo/redo operations for Reports and Documents.
• Synchronization of UniEditor and Properties view.
• Elements order in different Requality views.
• Marking up of crossing locations in Document editor.

A complete list of changes can be found in changelog.

Описаны существующие возможности создания репозиториев и доступа к ним: Repositories

Master's student Ilja Zakharov under Vadim Mutilin supervision successfully finished Google Summer of Code 2013 project Generation of Environment Model for Verification of Multi-module Device Drivers for The Linux Foundation.

Ilja worked in the following directions:

1. Experiments with extraction of interconnected Linux kernel modules.
2. New implementation for a Linux-related stack of components of the LDV Tools.

Ilja developed a new approach for extracting a graph of all interconnected Linux kernel modules and a new method for a graph clusterization specific for verification purposes. Obtained groups of modules rarely exceed 5 modules in size. Further research for generating environment model and study of corner cases lie ahead.

Kernel Manager, Build Command Extractor and Command Stream Divider components of the LDV Tools were completely redesigned. The most notable features that they support now include an adjustment on the basis of an extendable common configuration, a results caching, various strategies of module extraction and an extracting of the Linux kernel modules for the ARM architecture. Also a new architecture of these components allow to avoid all old bugs like this. Integration of the components with LDV Tools is ongoing.

Уважаемые коллеги!

В пятницу 22 ноября с 10:00 до 12:00 планируется перенос
сервера forge.ispras.ru. Будут временно недоступны следующие сервисы:

http://forge.ispras.ru/wiki/index.php - информационная система ИСП РАН (с данными по ПРНД)

Redmine 2.3.3
Доступ к git репозиториям по протоколу https

http://forge.ispras.ru/ - хостинг проектов, в основном отдела 11 - Технологий программирования.

MediaWiki 1.21.3
Semantic MediaWiki 1.9 beta-1

After more then 2 years of active development we are happy to announce that we released version 0.4 of LDV Tools. This version includes a lot of improvements and many bug fixes. In total it consists of about 900 commits that were made just in the LDV Tools repository not including submodules. The most significant changes are:

• Improvements in existing rule models: Module get/put, Atomic allocation in interrupt context, Mutex lock/unlock, Memory allocation under spinlocks, NOIO allocation under USB lock.
• Support of 25 new rule models: Possible TTY NULL dereference, Block requests, Usage of msleep(), USB gadget driver (de)registration, Initialization of spinlocks, Integer underflow in calling copy_from_user(), copy_to_user(), etc., Usage of spin_lock_irq*(), Usage of local_irq_*(), RW locks lock/unlock, probe() return values, Arguments of find_next_zero_bit(), Initialization of sysfs attributes, USB reference counting, Double kfree_skb(), Error handling in probe(), usb_deregister() and usb_serial_deregister(), netif_napi_add()/netif_napi_del(), napi_enable()/napi_disable(), register_netdev()/unregister_netdev(), alloc_netdev()/free_netdev(), Usage of mod_timer(), Usage of semaphores, Work with clocks, RCU read sections nesting, RCU update operations inside read sections, Initialization of completions.
• Fixing patterns for several driver callback structures to generate correct environment models.
• Introducing C Instrumentation Framework - a user-friendly interface for Aspectator.
• Supporting reusable blocks of aspect files and corresponding rearranging all existing rule models.
• Added ability to make source code querying with help of Aspectator, which is used in construction of rule models on the basis of instrumented source code (see corresponding news) and in generation of environment models.
• Support of a more user-friendly interface for reachability C verifiers.
• Switch to 2.7.1 version of BLAST - a default verifier of LDV Tools.
• Better integration with CPAchecker verifier that was included as submodule of LDV Tools.
• Integration with UFO verifier.
• Introducing a common format of error traces and improving visualization of error traces of different verifiers.
• Knowledge Base support for automatic marking unsafe verdicts of verifiers.
• Support for an automatic validation of LDV Tools and verifiers on known bugs in the Linux kernel.
• Coverage generation for debugging LDV Tools and different analyses of CPAchecker verifier.

Validation of LDV Tools 0.4 with different verifiers on 38 known bugs in the Linux kernel showed that:

• BLAST is able to detect 15 of them.
• CPAchecker is able to detect 13 of them.

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

We are happy to announce availability of MASIW Framework 4.1 under Eclipse Public License.

MASIW Framework is an Eclipse-based IDE for development and analysis of AADL models.
The major features of the toolset include:
- support of AADL v2.1;
- textual and graphical editors for AADL models;
- checker for AADL legality and consistency rules;
- checker of AADL models for compliance with constraints described as REAL theorems.

You are welcome to leave your feedback and bug reports at the main project site:
http://forge.ispras.ru/projects/masiw-oss

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

The new features include:

• Support for adding comments to requirements and test purposes that facilitates team communication and review process.
• An option to choose a browser engine (Mozilla or WebKit) to be used in ReqMarker and UniEditor.
• Support for custom report templates.
• Search and hot-keys in UniEditor.

Also various bugs has been fixed in:

• Undo/Redo operations.
• Copying and moving nodes in Requality Explorer and UniEditor.
• Document import process. Also now you can import documents with Cyrillic name.
• Documents and requirements removal and its effect to related requirements and locations.
• Update Processor.
• Order of nodes in Requality Explorer, Properties view and Outline.
• Handling pictures in requirement or test purpose description.
• Requality help documents also have been fixed and supplemented.

A complete list of changes can be found in changelog.

C++TESK Testing ToolKit v1.0.22 has been released. The following things have been done.

• Diagnostics subsystem has been seriously refactored
• Multimodel facilities have been debugged
• Cache coherence checking example has been updated
• Support of configuration files has been added
• Lagged Fibonacci generator has been implemented

The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.

Java Constraint Solver API v0.2.2 has been released. The following things have been done:

• support of constant folding has been added
• support of user-defined calculators has been added
• several bugs have been fixed

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

C++TESK and MicroTESK hardware verification toolkits were presented at the University Booth exhibition of the Design Automation Conference - the premier event for the design of electronic circuits and systems, electronic design automation (EDA), embedded systems and software (ESS), and intellectual property (IP). The conference took place on 2-6 June, 2013 in Austin, TX, USA (the city, which was nicknamed "the Silicon Hills" in the 1990s because of its unique hi-tech industry).

The conference is sponsored by the Association for Computing Machinery (ACM), the Electronic Design Automation Consortium (EDA Consortium), the Institute of Electrical and Electronics Engineers (IEEE) and ACM's Special Interest Group on Design. Read more...