Output details
11 - Computer Science and Informatics
University of Kent
Checking process-oriented operating system behaviour using CSP and refinement
<09> This article brings together a number of different ongoing areas of research, including programming language design, automatic model generation and model-checking. It reports on an automated approach for verifying correctness properties of concurrent device-device drivers, giving either a pass or providing a contradiction, using existing model-checking tools. The techniques described allowed us to uncover errors within OS device-drivers unlikely to be encountered through testing. The paper was originally presented at the PLOS workshop (part of ACM SOSP-2009), and was selected for publication in the SIGOPS-OSR journal.