Technologies and Tools of the Linux Verification Center
UniTESK: Model-Driven Automated Testing Technology
To develop test suites, Linux Verification Center uses UniTESK technology and, in particular, CTesK tools. UniTESK is an automated model-driven technology for test development that has proved itself in various industrial projects. The key point of the technology is automatic generation of tests based on formal requirement specifications and corresponding test scenarios. UniTESK gives the following to the OLVER project:
- Thorough testing is achieved relatively easy by making sophisticated computer algorithms responsible for test sequences generation based on high level scenario descriptions in SeC language.
- Separating specifications and test scenarios allows independently changing the tests as requirements evolve and improve test coverage thoroughness as resources appear.
- Automatic test generation allows smooth parameterization and customization thus facilitating adaptation of the tests for various usage conditions (e.g. for pared-down embedded Linux systems or extended enterprise requirements).
CTesK: UniTESK Technology Support Tools for C Language
The detailed description of the CTesK tools can be found in the following documents:
- CTesK 2.2: User's Guide
- CTesK 2.2: SeC Language Reference
- Using CTesK 2.2 with GCC: Getting started
- CTesK 2.2: Installation Instructions
The tools can be downloaded from the site unitesk.com.
Requirements Formalization and Test Suite Production Process
The production process used at the Linux Verification Center to develop tests includes the following main stages:
- Decomposition of the standard into groups of related functions.
- Analysis of the standard and extracting requirements for every group of functions.
- Formalization of the requirements to check for.
- Development of the test action scenarios for every group of functions.
- Automatic generation of tests by CTesK tools.