Ilja Zakharov successfully finished Google Summer of Code 2014 project Parallel Verification of Linux Kernel Modules under Evgeny Novikov supervision.
During the project Ilja made an overview of available technologies of cloud and distributed computing which are suitable for software verification tools deployment - the actual task since such tools are characterized by high time and memory consumption. Working in touch with other LDV developers he also contributed to the new perspective version of LDV Tools which is still under development. As a result he improved performance of verification task generation and proceeded with a solution of an infrastructure for establishing distributed Docker-based verification. As a part of the project Ilja also implemented verification on a remote host using BLAST in a Docker container and CPAchecker cloud web-interface task submitting. The latter was merged to master in 960e64e.
The new release contains the following changes:
- Support for VLIW was implemented
- Support for floating-point types was implemented
- Ability to specify initialization code in test templates (the 'preparator' construct) was implemented
- New test data generators were implemented
- The test templates library was improved (including new text printing facilities and ability to specify unknown immediate values)
- New examples of test templates demonstrating features of MicroTESK were added
- Ability to use labels rather than addresses in the generated code was implemented
The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files
The HDL-to-EFSM extraction method used in HDL Retrascope will be presented at the All-Russia Science & Technology Conference
Problems of Advanced Micro- and Nanoelectronic Systems Development (MES) - the largest conference in the field of CAD microelectronics in Russia and CIS countries. The conference will take place on September 29 - October 3 in Zelenograd, Moscow.
Fortress v0.3.2 has been released.
The new release includes the following changes:
- Factory methods to simplify creating NodeValue objects
- Support for creating deep copies of expressions
- Utility classes for generating random values
- Support for a variable number of operands in the expression calculator
- Saving/loading constraints to/from an XML string
- Aborting visiting an expression tree and skipping subtrees
- Basic facilities to calculate the type of an expression
- Extending the functionality of a solver with function templates
- New standard operations: ABS, MIN, MAX, BVANDR, BVNANDR, BVORR, BVNORR, BVXORR, BVXNORR
- Class NodeExpr was renamed to NodeOperation
- XML format was simplified: nodes Expression and Operation were merged together (the new node is called Operation)
- Class ExprUtils that provides a set of useful methods to work with logical expressions
- Expression printers for Verilog and VHDL hardware description languages
- Support for the boolean type in the calculator
The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files
Version 0.16 of Requality has been released, with some new important additions and fixes.
The new features include:
- New version of UniEditor with in-line editors.
- New wizard helping to create a test directly from a requirement (or a test case) it targets to cover to. The new test can be created in another Eclipse project on the base of customized template. Custom 'New Test' wizards can be added via user-specific Eclipse plugin implementing 'testgenerator' extension point.
- New report that shows coverage of requirements (or test cases) by external entities (e.g. tests). Information about external entities (Coverage Source) can be provided
- via xml file in specified format
- using regexp-based wizard collecting data from projects in current workspace
- by custom Eclipse plugin implementing 'coveragesource' extension point
- Type-aware editors for attributes of supported types.
- Improved appearance of "Requirements" report.
- Better report generation in console mode. Custom parameters can be passed to report templates now.
- Filter allowing to filter out comments in Requality Explorer.
- Improvements in reports generation:
- Widely used auxiliary functions are now available in "utils" object (e.g. htmlEscape function).
- There is a new "coverage" object that provides methods to access information about requirements coverage by external entities (see examples in "coverage" template).
- DOM model of documents is now available (see utils.getDocumentNodeModel(qid)).
Also various bugs have been fixed in:
- Properties view.
- Reports generation, especially in predicates handling.
- Marking up of text fragments (e.g. a fix for the problem of space to be not marked up).
A complete list of changes can be found in changelog.
LDV Tools 0.6 includes the following most important changes:
- Compatibility with Linux kernel 3.14-3.16.
- Improvements in 5 existing rule specifications:
- Adding 11 new rule specifications:
- Update the CPAchecker verification tool to version 1.3.4 (r12604).
- Fixing most of memory-related issues, especially memory leaks, in Aspectator and C-backend of the CIF component (now they consume up to 1000 times less memory on large aspect files).
- Optimization of Aspectator that reduces instrumentation time in about 25 times on specific large aspect files.
- Alternative implementation of the script uploading LDV verification reports into databases that operates several dozen times faster.
Results of validation of LDV Tools 0.6 and LDV Tools 0.5 with different verification tools on 41 known bugs in the Linux kernel* are presented in the table below.
| |
LDV Tools 0.6 |
LDV Tools 0.5 |
| |
BLAST |
CPAchecker |
BLAST |
CPAchecker |
| Found bugs |
17 |
13 |
15 |
14 |
| Missed bugs |
Bugs in verification tools |
3 |
2 |
3 |
3 |
| Out of memory (63 gigabytes) |
1 |
2 |
1 |
0 |
| Timeouts (50 minutes) |
0 |
6 |
0 |
4 |
| Unsupported rule specifications |
0 |
0 |
7 |
7 |
| Others |
20 |
18 |
15 |
13 |
Both BLAST and CPAchecker were able to find one more bug thanks to improvements in rule specification SKB allocation in pm_runtime context. Additionally BLAST has found a new bug with one of the new rule specifications. CPAchecker has lost ability to detect 3 bugs due to degradation in analysis time, while it has found a bug that led to an exception before.
The source code repository can be browsed by v0.6 tag. To get and to install LDV Tools see instructions.
* This validation benchmark has many differences from the one used earlier for validating LDV Tools 0.5.
Fortress v0.3.1 has been released.
The new release includes the following changes:
- support for parametric operations with two or more parameters
- support for array operations
- support for the BVEXTRACT operation
The library can be downloaded from the page http://forge.ispras.ru/projects/solver-api/files
The HDL Retrascope tool will be introduced at the University Booth and PhD Forum of the Design Automation Conference (DAC) - the premier conference for design and automation of electronic systems. The conference will take place on June 1-5 in San Francisco, CA, USA.
DAC offers outstanding training, education, exhibits and superb networking opportunities for designers, researchers, tool developers and vendors. The conference is sponsored by the Association for Computing Machinery (ACM), the Electronic Design Automation Consortium (EDA Consortium), and the Institute of Electrical and Electronics Engineers (IEEE), and is supported by ACM's Special Interest Group on Design. Read more...
C++TESK Testing ToolKit will be presented at the IP Track, University Booth and PhD Forum of the Design Automation Conference (DAC) - the premier conference for design and automation of electronic systems. The conference will take place on June 1-5 in San Francisco, CA, USA.
DAC offers outstanding training, education, exhibits and superb networking opportunities for designers, researchers, tool developers and vendors. The conference is sponsored by the Association for Computing Machinery (ACM), the Electronic Design Automation Consortium (EDA Consortium), and the Institute of Electrical and Electronics Engineers (IEEE), and is supported by ACM's Special Interest Group on Design. Read more...