Open Linux VERification (OLVER) Project

The Open Linux VERification (OLVER) project was the flagship activity of the Center in 2005-2006. The general purpose of the project is to strengthen Linux Standard Base (LSB) Core standard by clarifying its requirements through formal specifications and improving conformance and functional tests for LSB Core 3.1. The specific technical goals were:

  • Analyze the Linux Standard Base (LSB) Core 3.1 (ISO/IEC 23360-1) standard to extract atomic requirements on behavior of the main system libraries (sections III.Base Libraries and IV.Utility Libraries – total 1532 interface functions).
  • Reveal and report any deficiencies and ambiguities in the text of the standard to allow fixing them in the future LSB (and underlying standards) versions.
  • Elaborate formal specifications in SeC language (Specification Extension of C) that reflect the requirements of LSB Core 3.1 standard in machine-readable form (for the 1532 system interface functions).
  • Develop an open source test suite for functional and conformance testing of various Linux-based systems against the requirements of the LSB standard with regard to behavior of application programming interfaces (see System Under Test). The test suite should be based on automatic test generation from formal specifications of the requirements and corresponding test scenarios (see UniTESK Technology).
  • Develop a configuration and execution control system. The purpose of such a system is to provide convenient customization of the test suite by a number of parameters (for example, thoroughness of testing, options of the target system, choosing specific variant of behavior, etc.) and visualization of the test results pointing out discrepancies with particular requirements of the standard. Using this system should leverage the UniTesK technology and allow easy adaptation of the tests for various usage conditions (e.g. for pared-down embedded systems or extended enterprise requirements).

The results (specifications, the test suite and tools for generating and using tests) are published on the web-site of the Center and distributed under the free license - Apache License 2.0.

Since 2007, OLVER project is in the maintenance stage.