Proceedings of ISP RAS


Linux Driver Verification Architecture.

A.V. Khoroshilov, V.S. Mutilin, E.M. Novikov, P.E. Shved, A.V. Strakh.

Abstract

The paper discusses requirements to a twofold verification system that should be an open platform for experimentation with various verification techniques as well as an industrial-ready domain specific verification tool for Linux device drivers. An architecture of a verification system implementing the requirements is presented and its components are described in details. Finally, we discuss the first experience of usage of the system and evaluate directions for its further development.

Keywords

static analysis; safety rule; device driver verification; driver environment model; aspect oriented programming; domain specific verification; reachability verifier; error trace visualizer

Edition

Proceedings of the Institute for System Programming, vol. 20, 2011, pp. 163-187.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

Full text of the paper in pdf (in Russian) Back to the contents of the volume