Project

General

Profile

News

Klever: Klever 3.0

Added by Evgeny Novikov about 2 months ago

Let’s start the new year 2021 with new Klever 3.0!

Among a lot of improvements and bug fixes, most significant changes in Klever 3.0 are as follows:
  • Support for verification of kernel loadable modules of Linux 5.5.
  • Support for verification of Linux kernel loadable modules on the ARM architecture.
  • Fixing and developing specifications for verification of Linux kernel loadable modules:
    • Fixing specifications for checking usage of clocks in drivers.
    • Support for checking usage of the RCU API.
    • Developing detailed specifications for USB serial drivers.
    • Improving environment models for runtime power management callbacks.
    • Using device identifiers from the driver tables.
    • Developing models for devm memory allocating functions.
    • Fixing framebuffer_alloc/release models.
    • Adding models for request/release_firmware(), v4l2_i2c_subdev_init() and i2c_smbus_read_block_data().
  • More user-friendly configuration for target program fragments and requirement specifications.
  • Development of preset tags for assessing most common false alarms.
  • Support for new internal data formats for enhancing and optimizing representation and assessment of verification results.
  • Support for cross-references for original program source files and models.
  • Update of all variants of the CPAchecker verification back-end.
  • Switching to a special version of Frama-C developed within project Deductive Verification Tools for Linux Kernel from outdated and unmaintained CIL. Both tools are used for merging source files and optimizations like removing unused functions.
  • Using systemd scripts instead of init.d ones for Klever services.
  • Development of Tutorial

Klever 3.0 is not backward compatible with former versions of Klever, so, you need to remove existing instances if so and deploy Klever from scratch.

As usual many thanks are to everyone who participated in this release of Klever!

Requality: Requality 1.2 released

Added by Alexey Khoroshilov 4 months ago

Version 1.2 of Requality has been released with many scalability and usability improvements:
  • Requirements HTML editor:
    • support for preformatted text and indents;
  • Properties view:
    • search in history properties page and “Switch to…” dialog;
    • highlighting of current revision in history tab and revision selection in “Switch to...”;
    • speedup of history properties page loading;
    • asynchronous operations with attributes.
  • Reporting:
    • refactoring of reports hierarchy from plain to tree-like with unification of reports naming;
    • header with description of revisions in “compare versions“ report;
  • Requality interface:
    • message box after “Switch to old version“ operation;
    • asynchronous loading of requality projects;
    • better interface for Checker Rules editor;
    • better interface of Requality References.
Experimental features:
  • reference versioning with tracking if referenced elements are updated;
  • new report for debugging checker rules;
  • persisted ”show description on elements” flag.
Also various bugs have been fixed in:
  • “compare versions” report;
  • git operations — “Switch to ...“, “Reset ...“, etc.
  • internal caches;
  • attributes panel;
  • “mandatory attributes” functionality.

A complete list of changes can be found in changelog.

Castle: Castle 0.1.5 released

Added by Sergey Smolov 5 months ago

What's new?
  • AST: new getName method at RangedVariable class
  • AST: Assignment class fields are renamed
  • Bug fixes and general improvements

Verilog Translator: Verilog Translator 0.1.3 released

Added by Sergey Smolov 5 months ago

The release includes the following changes:

  • Build system: use Gradle 5.0;
  • Documentation: changelog and readme are rewritten into Markdown format;
  • Language: support for macro with parameters;
  • Language: support for SystemVerilog Assertions;
  • Options: `--library-file` option to include function library files;
  • Tests: test cases for QUIP and IWLS'2005 benchmarks;
  • Tool: bug fixes and general improvements;
  • Tool: error diagnostics is improved;
  • Tool: migration to Java 11.

The tool can be downloaded from here
The list of resolved issues can be found here

Requality: Requality 1.1 released

Added by Alexey Khoroshilov 9 months ago

Version 1.1 of Requality has been released with better git integration and usability improvements.

The new features include:
  • Reports gets meta information header including:
    • information about git revision of the project;
    • information about local changes regarding git;
    • user initiated report generation;
    • tool version;
    • time of report generation.
  • Support for switching project to a particular revision from git repository history.
  • Support for “Local only” flag allowing to ignore some folders in repository.
  • Search dialog keeps last settings during working session.
  • Better support for term definition-usage relation.
  • Report export operation ends with modal dialog message.
  • All eclipse plugins are moved to a single category.
Also various bugs have been fixed in:
  • terms handling;
  • repository operations;
  • versioning;
  • report generation;
  • undo-redo.

A complete list of changes can be found in changelog.

MicroTESK: MicroTESK 2.5.1 released

Added by Alexander Kamkin about 1 year ago

What's new?

  • Fixed the TokenSourceStack class and moved it to the Castle 0.1.4 library (see https://forge.ispras.ru/projects/castle)
  • Rearranged the documentation
  • Modified the mmuSL code generation scheme
  • Added a boot section to the miniMIPS test templates
  • Fixed a number of long-lived bugs
  • Used the QEMU4V 0.3.5 simulator for running tests

Download: http://forge.ispras.ru/projects/microtesk/files

(1-10/341)

Also available in: Atom