Software Model Checking of Linux Device Driversстатья
Информация о цитировании статьи получена из
Web of Science
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 22 февраля 2019 г.
Аннотация:The talk presents experience of Linux Verification Center of ISPRAS in verification of Linux device
drivers with software model checking tools. Software model checkers solve reachability problems,
i.e. they prove that error locations in a program cannot be reached by any execution starting from
an entry point. Linux device drivers have neither a traditional entry point no labeled error locations.
We present our approach to bridge the gap. The key element of the approach is generation a model
environment that tries to reproduce the same scenarios of interactions with the driver as the actual
kernel does as well as it tries to be simple enough to be analyzable by existing tools. The results are
quite positive. So far, there are more than 250 problems found, reported and already fixed in Linux
device drivers by our project. But still many open problems remain to be solved. Another aspect to
be discussed is lessons learned in application of academic tools to solve industrial tasks.