Output details
11 - Computer Science and Informatics
University of Kent
Output title
Checking process-oriented operating system behaviour using CSP and refinement
Type
E - Conference contribution
Name of conference/published proceedings
ACM SIGOPS Operating Systems Review
Volume number
43
Issue number
4
First page of article
45
ISSN of proceedings
01635980
Year of publication
2010
Number of additional authors
1
Additional information
<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.
Interdisciplinary
-
Cross-referral requested
-
Research group
P - Programming Languages and Systems Group
Citation count
0
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
