Paper Details

Communicating Process Architectures (CPA)
 Title: Designing a Mathematically Verified I2C Device Driver using ASD
 Conference: Communicating Process Architectures 2009
 Authors: Arjen Klompa, Herman Roebbersb, Ruud Derwigc, Leon Bouwmeestera
(a) Verum B.V.
(b) Philips TASS
(c) NXP
 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. 

BibTeX Entry

Full paper