Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397

Issue N8 2012 year

Development of Synchronization Objects verifier for Linux Device Drivers Based on Process Semantics
Yu. P. Korablin , e-mail: y.p.k@mail.ru, E. G. Pavlov , e-mail: lucenticus@gmail.com

This article describes the tool for finding problem with synchronization of drivers in Linux. This tool uses a method of detecting error basis on semantic models and allows you to detect such synchronization errors as infinity loops, deadlocks, and double locks. In addition, describe the process semantics of synchronization objects of Linux kernel in the language of asynchronous functional schemes

Keywords: verification, device drivers, communicating sequential processes, equational characterization, algebraic semantics
pp. 2–9