Open-Source Projects

The new release includes the following bugfix:

• Aarch64: increase size of internal string buffer

The source code can be downloaded from here

The new release is based on QEMU 3.1.0 and includes the following features:

• Basic support for PowerPC programs emulation
• Trace generation for PowerPC (32bit) programs

The complete list of resolved issues is available here

The source code can be downloaded from here

MicroTESK for RISC-V 0.0.7 has been released:

• Specifications: Vector extension

MicroTESK for RISC-V can be downloaded from https://forge.ispras.ru/projects/microtesk-riscv/files

The new release contains the following changes:

• Support for separate-file sections (useful for boot generation)
• Support for the 'decode' attribute of nML primitives (experimental)
• Decoder generator: enabling bit selection for non-immediate arguments
• Bug fixes and code improvements

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

The new release includes the following features:

• Trace generation for MIPS (MIPS64) programs

The complete list of resolved issues is available here
The source code can be downloaded from here

We are happy to announce that Klever 2.0 is released!

Klever 2.0 implements ideas suggested in [1]. In general we added support for verification of software written in the GNU C programming language. First examples of using Klever for software that differs from Linux device drivers are verification of Linux kernel subsystems [2] and BusyBox applets. We are looking forward for more success stories!

Most important changes in Klever 2.0 are the following:

• Klever does not build programs under verification anymore. Instead it takes as input build bases that should be prepared with Clade in advance. This considerably speed ups verification when verifying the same software within different verification jobs. Also, this provides a more natural way to integrate Klever within a standard development life cycle.
• The generator of program fragments (former verification objects) includes abstract means suitable for various software as well as means for particular kinds of programs that allow to avoid considerable efforts for configuring program decomposition.
• The environment models generator consists of a number sub-generators that take specifications in suitable specific formats. This allows to simplify development of such the specifications very much. Besides, we fixed many existing and developed new environment model specifications both for new kinds of interactions between Linux kernel and BusyBox components and for new versions of the Linux kernel.
• The Klever interface provides users with a extremely useful online editor that enables changing configuration and specification files directly within the interface.

As usual many minor improvements and bug fixes were included in Klever 2.0.

Klever 2.0 differs too much from previous versions of Klever. Therefore, we recommend to deploy it from scratch rather than to update existing deployments.

We would like to thank everybody who participated in development, testing and using of Klever!

References

1. Novikov E., Zakharov I. (2018) Towards Automated Static Verification of GNU C Programs. In: Petrenko A., Voronkov A. (eds) Perspectives of System Informatics. PSI 2017. Lecture Notes in Computer Science, vol 10742. Springer, Cham.
2. Novikov E., Zakharov I. (2018) Verification of Operating System Monolithic Kernels Without Extensions. In: Margaria T., Steffen B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science, vol 11247. Springer, Cham.

After more than 10 years of development we are happy to announce the release of Requality 1.0.

The new version emphasizes the readiness of the tool to support requirements management process of safety-critical software development.
There are ongoing projects aimed to develop avionics software according to DO-178C Level A that uses the Requality as the main requirements management tool.

The main new features of Requality 1.0 in comparison with version 0.20 includes:

• Server repository for storing history of development of requirements catalogue and team collaboration with explicit operations:
  • for storing local version of requirements catalogue into the repository;
  • for checking out requirements from the repository for local edit/review.
• Presentation of history of modifications of requirements catalogue.
• Presentation of differences between particular versions of requirements catalogue.
• Automatic per-object versioning:
  • Each element of requirements catalogue gets an individual version that is incremented automatically when one of internal attributes is modified and the modification is committed to the repository.
  • Which attributes are considered as internal is configured on per project basis.
• Support for cross-project references.
• Explicit support for "define term"-"use term" relation between objects.
• Search through requirements catalogue:
  • Search in Requality project for elements by any attribute including all kind of identifiers.
  • All editors get support for search of specific string in text.
• New report template "Table View" that represents requirements specification in the form convenient for formal review as far as:
  • it includes references to related objects (including definition of terms used);
  • it allows to generate report for several related projects (e.g. high-level requirements and low-level requirements) with HTML cross-references between them.
• Export/import requirements to LibreOffice Writer for editing in office suite environment.
• Mass operations support:
  • Attribute Value change.
  • Attribute Type/Name change.
• Support for ReqIF export and import (in the form compatible with IBM DOORS 9.4).
• WebAPI provided to simplify integration with external tools.
• The speed of report generation is significantly increased.

The new release is based on QEMU 3.0.0

The functionality is left unchanged.

The complete list of resolved issues is available here

The source code can be downloaded from here

Klever 1.1 includes quite many high demanded features and fixes of the most annoying bugs:

• Improving coverage calculation and visualization. Now one can easily navigate through covered and uncovered functions.
• Updating CPALockator used for finding data races.
• Proper processing of wall timeouts that is especially important for highly overloaded machines.
• Advanced verification tasks scheduling allows:
  • Solving verification tasks faster by means of adaptation of computational resource limits.
  • Solving more verification tasks when having free computational resources after ensuring a minimally required quality of service.
• Getting rid of some database caches helps to avoid unpleasant bugs in various statistics.
• Considerable fixing and improving local and OpenStack deployments.
• Numerous minor bug fixes, optimizations and improvements.

MicroTESK for RISC-V 0.0.6 has been released:

• Specifications: Bug fixes in floating-point instructions
• Tool Functions: Updated MicroTESK core

MicroTESK for RISC-V can be downloaded from http://forge.ispras.ru/projects/microtesk-riscv/files