%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.