Paper Details

Communicating Process Architectures (CPA)
 Title: Formal Analysis of Concurrent OS (RMoX) Device Drivers
 Conference: Communicating Process Architectures 2011
 Authors: Martin Ellis
School of Computing, University of Kent
 Abstract: Many tools exists for writing safe and correct device drivers for conventional operating systems, from runtime driver management layers (that try to detect errors and recover from them) to static analysis systems like SLAM. Unfortunately, these tools do not map well to the concurrent drivers we write for RMoX. This presentation will look at how we can build safe and correct device drivers, using traditional occam analysis approaches (such as CSP) and tools (such as FDR). Experiments in generating formal models of hardware/driver interfaces from our occam implementations will be described, along with how we intend to use these models to prove correctness properties for our drivers. 
Files:


BibTeX Entry


Presentation