Technical FAQ

If you have not found an answer to your question, please, contact us, and we will be glad to help you.

1. What is tested in the OLVER project?
   
2. How are specification based tests produced?
   
3. What is the difference between the tests of the Center and the existing tests for Linux?
   
4. Where to start learning UniTESK technology?
   
5. Where can I find a description of the SeC specification language?
   

1. What is tested in the OLVER project?
   The main testing focus of the OLVER project is on the Linux system libraries defined in the LSB Core 3.1 standard. We test behavior of 1532 interfaces of these libraries (the list can be viewed at Specifications). Meanwhile, many of these interfaces use Linux kernel calls. Also, hardware can affect the behavior. So the whole Linux configuration is actually involved in OLVER testing, which means checking the joint work of the libraries, the kernel and hardware. The tests simulate an application that calls library APIs in different combinations and with various parameters. But the tests differ from applications in that the tests "know" how the interfaces should work (which is defined by specifications) and thus they can check the correctness of return values, resulting system states, reaction sequences, etc. See System Under Test for details.
2. How are specification based tests produced?
   Requirements in the form of formal specifications supplemented with test scenarios allow automatically producing tests that verify conformance to these requirements. For creating tests, Linux Verification Center uses CTesK tools that implement C language binding for the general UniTESK technology. Detailed description of our test production process can be found here.
3. What is the difference between the tests of the Center and the existing tests for Linux?
   The existing Linux tests use a traditional approach when requirements of a standard are manually transformed into several cases and for each of them a separate test is prepared, usually as an independent program. The mapping between the requirements and the tests as well as the tests itself are created "ad hoc" - as developer supposes them to be convenient or correct. The quality of such tests is determined by the experience of particular developer and his advertence when doing this work. We construct the tests in a more organized manner that minimizes personal impact: firstly, we divide the text of the standard into atomic requirements for each function, write these requirements in the form of formal specifications, and then analyze them for several functions at once to find out which different situations may occur in the work of the system. This information is also written formally and allows checking all the requirements in all the situations found. The tests themselves are generated automatically from these two descriptions that tell how to check and in which cases. Systematic enumeration of possible situations is performed by an algorithm that is similar to a robot that tries to pass a labyrinth without a plan, but by writing the information about the sections he passed, he is creating the full map of the labyrinth. The path he built (the chain of calls of separate functions) turns out to be the test that covers all the situations needed. More detailed information about our process of test production can be found here.
    
   Of course, thoughtful and accurate developer is able to manually write tests of similar quality. However, we make the computer to perform most part of the work automatically and thus obtain the tests with less effort. With the same effort for creating the tests manually, it is nearly impossible to get the result of the same quality.
4. Where to start learning UniTESK technology?
   The most efficient way to study UniTESK technology and its particular tools is attending the special trainings at the Institute for System Programming of RAS. But it is possible to use documentation from the website of UniTesK. Also please refer to the Technologies and Publications sections of this site.
5. Where can I find a description of the SeC specification language?
   The documentation on the SeC language can be downloaded from http://unitesk.com/. The site also contains additional information on using CTesK tools.