Go back to the main GSoC Linux Foundation page
Mailing list: lsb-discuss at lists dot linux-foundation dot org
IRC: #lsb on irc.freenode.net
Code License: GPL/BSD, specs: GNU FDL
Mentors: Alexey Khoroshilov (alexey dot khoroshilov at gmail dot com), Jeff Licquia, Vladimir Rubanov, Denis Silakov (dsilakov at gmail dot com).
It is required to capture data of C11 ABI for [[http://ispras.linuxbase.org/index.php/LSB_Database_Home , SQL databases, Perl
Mentors: Alexey Khoroshilov, Denis Silakov
Linux Driver Verification (LDV) program is devoted to developing an integrated framework for device drivers verification and adopting leading edge research results to enhance quality of verification tools. Currently LDV tools are used to check Linux device drivers against several safety rule specifications, each of them formally defines what is correct usage of a particular part of kernel core API. Another way of looking at the safety rules is that a rule represents one or more typical misuse of kernel core API.
By the moment, the framework contains around 30 rule specifications that has already helped to find and fix more than 250 issues in device drivers of vanilla Linux kernel.
This project (or several ones) is aimed at extending number of rules supported by the framework.
We have a collection of several dozens rules written in informal way, but other rules can be used as well. Formalization process usually includes the following steps:
Rule specifications are written in a mix of C code and AspectJ-like notation that allows to merge the model code with original source code of device driver.
More than one application can be approved. Formalization of ~5 rules is expected from each student.
Desired knowledge: C, aspect-oriented programming, Linux kernel space API
Mentors: Alexey Khoroshilov, Vadim Mutilin, Eugeny Novikov
LSB Core tests [1,2] is the main part of LSB certification tests. Originally they were developed for POSIX (IEEE Std 1003.1-1990) and LSB 3.1. LSB specification was expanded since that time (http://linuxbase.org/navigator/browse/status.php). The goal of the project is to fix open issues in the tests, i.e. to fix issues appearing on modern Linux distributions and to accomodate all relevant changes in text of specifications, as well as to expand coverage of the test suite to newly added LSB Core interfaces.
VSX-PCTS was implemented using TET/VSXgen test harness. The OLVER test suite was developed using model-based testing technology UniTESK. The technology follows well-known Design by Contract approach to represent formal specifications. Program contracts consist of preconditions and postconditions of interface operations and data type invariants. The main advantage of program contracts is that they enable automatic construction of test oracles that check the conformance of the target system behavior to the specifications.
Traceability of formal specifications to text of original LSB/POSIX specifications is supported using the following ideas:
[1] http://bzr.linuxfoundation.org/loggerhead/lsb/devel/olver-core-tests/files
[2] http://bzr.linuxfoundation.org/loggerhead/lsb/devel/runtime-test/files
Desired knowledge: C, SEC, model based testing
Mentors: Alexey Khoroshilov, Roman Zybin
LSB Desktop tests [1,2] is a part of LSB certification tests. Existing tests do not cover all interfaces included into LSB and LSB specification continues to grow (http://linuxbase.org/navigator/browse/status.php). The goal of the project is to develop tests for newly included libraries and for interfaces that have no tests yet (http://linuxbase.org/navigator/coverage/cov2.php).
Gtk3/Gdk3 and friends are at the moment very high on our list of untested items. The test development ideally should be coordinated with upstream projects so the tests can be useful for them as well.
[1] http://bzr.linuxfoundation.org/loggerhead/lsb/devel/desktop-test/files
[2] http://bzr.linuxfoundation.org/loggerhead/lsb/devel/t2c-desktop-tests/files
Desired knowledge: C, Testing
Mentors: Alexey Khoroshilov, Roman Zybin