@InProceedings{Klomp09,
  title =        "{D}esigning a {M}athematically {V}erified {I}2{C} {D}evice {D}river using {ASD}",
  author=        "Klomp,  Arjen and Roebbers,  Herman and Derwig,  Ruud and Bouwmeester,  Leon",
  editor=        "Welch, Peter H. and Roebbers,  Herman and Broenink,  Jan F. and Barnes,  Frederick R. M. and Ritson,  Carl G. and Sampson,  Adam T. and Stiles,  G. S. and Vinter,  Brian",
  pages =        "105--116",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn=          "978-1-60750-065-0",
  year=          "2009",
  month=         "nov",
  abstract=      "This paper describes the application of the Analytical
     Software Design
methodology to the development of a
     mathematically verified I2C device
driver for Linux. A model
     of an I2C controller from NXP is created,
against which the
     driver component is modelled.  From within the ASD
tool the
     composition is checked for deadlock, livelock and
     other
concurrency issues by generating CSP from the models
     and checking
these models with the CSP model checker FDR. 
     Subsequently C code is
automatically generated which, when
     linked with a suitable Linux
kernel run-time, provides a
     complete defect-free Linux device driver.
The performance
     and footprint are comparable to handwritten code."
}