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 - Agenda - Paper 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.