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 elementary 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.

OLVER tests have been included into official LSB certification test suite and are maintained under management of the Linux Foundation.

OLVER Core Binaries and Sources

The main source code repository of the OLVER test suite is here.

Binary builds are available from the FTP server of the Linux Foundation.

The recommended way to run OLVER tests on typical Linux distributions is Linux Distribution Checker. For embedded systems other approaches may be more appropriate. For example, there is an Eclipse plugin developed by ETRI that automates launching OLVER tests on embedded systems using advanced features of distributed OLVER architecture.

OLVER Core Documentation

File Version Description
OLVER Readme 1.4 OLVER Readme file contains brief information on how to install, build and execute OLVER tests.
OLVER Reports: Reference Guide PDF 1.0 Description of the various test reports generated by the OLVER Core test suite.
math.integer: Getting Started PDF 1.1 Description of the test suite architecture and some technical aspects of requirements formalization and specifications development by the example of math.integer functions.
»