Designing a Mathematically Verified I~2C Device Driver Using ASD

摘要

This paper describes the application of the Analytical Software Design methodology to the development of a mathematically verified I~2C device driver for Linux. A model of an I~2C 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 runtime, provides a complete defect-free Linux device driver. The performance and footprint are comparable to handwritten code.