Paper Details

%T Formal Analysis of Concurrent OS (RMoX) Device Drivers
%A Martin Ellis
%E Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X 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.

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.