Premium
Towards automatic software model checking of thousands of Linux modules—a case study with Avinux
Author(s) -
Post Hendrik,
Sinz Carsten,
Küchlin Wolfgang
Publication year - 2009
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.399
Subject(s) - computer science , operating system , plug in , programming language , source code , model checking , process (computing) , software , code (set theory) , embedded system , software engineering , set (abstract data type)
Modular software model checking of large real‐world systems is known to require extensive manual effort in environment modelling and preparing source code for model checking. Avinux is a tool chain that facilitates the automatic analysis of Linux and especially of Linux device drivers. The tool chain is implemented as a plugin for the Eclipse IDE, using the source code bounded model checker CBMC as its backend. Avinux supports a verification process for Linux that is built upon specification annotations with SLICx (an extension of the SLIC language), automatic data environment creation, source code transformation and simplification, and the invocation of the verification backend. In this paper technical details of the verification process are presented: Using Avinux on thousands of drivers from various Linux versions led to the discovery of six new errors. In these experiments, Avinux also reduced the immense overhead of manual code preprocessing that other projects incurred. Copyright © 2008 John Wiley & Sons, Ltd.