10-Mar-2014: Linux Verification Center at Embedded World 2014

Vadim Mutilin and Evgeny Novikov have taken part in Embedded World 2014 in cooperation with Open Source Automation Development Lab (OSADL) on February 25-27, Nuremberg, Germany.

At the exhibition Linux Verification Center of ISPRAS presented tools and technologies for verification and testing of software and hardware. For Linux kernel space verification we presented:

• Linux Driver Verification Tools complementing static analysis tools using advanced verification techniques that provide extra precision and depth of source code analysis.
• KEDR framework facilitating dynamic (runtime and post factum) analysis of Linux kernel modules including device drivers, file systems, etc. As a part of framework it includes Leak Checker and Fault Simulator tools.
• Race Hound - a run-time race condition detection tool for the Linux kernel.
• Linux File System Verification project providing exhaustive test suites for Linux file system drivers.

For testing hardware models we presented:

• C++TESK - an open-source C++-toolkit aimed to facilitate functional verification of Register-Transfer-Level hardware designs.
• MicroTESK - a reconfigurable (retargetable and extendable) model-based test program generator for microprocessors and other programmable devices.

Also we demonstrated the following test suites:

• Test suite for APEX interfaces of ARINC-653 real-time operating systems.
• "Mathematics" test suite for mathematical functions of POSIX/IEEE-754/ISO 60559:2011 standards.
• LSB certification tests aimed to check if system libraries meet the requirements of Linux Standard Base.