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