You are here: Home / RTLWS 1999-2017 / RTLWS Submitted Papers / 
2022-08-20 - 07:10

Real Time Linux Workshops

1999 - 2000 - 2001 - 2002 - 2003 - 2004 - 2005 - 2006 - 2007 - 2008 - 2009 - 2010 - 2011 - 2012 - 2013 - 2014 - 2015

15th Real Time Linux Workshop, October 28 to 31, 2013 at the Dipartimento Tecnologie Innovative, Scuola Universitaria Professionale della Svizzera Italiana in Lugano-Manno, Switzerland

Announcement - Call for participation (ASCII)Hotels - Directions - AgendaPaper Abstracts - Presentations - Registration - Abstract Submission - Sponsors - Gallery

Verification of Safety Properties with Open Source Software Model Checkers

Alexey Khoroshilov, Linux Verification Center, ISPRAS, Russia

Static analysis tools allow to check properties of a program looking at its source/binary code without executing the program. The main potential benefit of the approach is a possibility to check all possible execution paths at once without choosing test inputs and without a need to access physical hardware. As tools are maturing, static analysis is gaining adoption in software industry. Meanwhile, application of the tools in safety-critical domain has some specifics. Soundness of the analysis becomes a vital property as far as otherwise it is not possible to use the results of the analysis as an evidence in a certification process. Model checking is a very promising approach to code analysis in this respect.

The talk considers state of the art of open source model checkers for C programs on top of our experience of their usage within Linux Driver Verification program. The conventional characteristics such as time/memory efficiency and false positive rate are discussed as well as possible approaches to use them in safety critical domain.