Abstract:

Embedded systems are electronic systems designed for dedicated applications. Modern embedded systems have many peripherals that enable the systems to communicate with the outside world. These peripherals are manipulated by specific software components, termed device drivers, which provide a stable software interface to the other components of the embedded system software. Because of their strong dependence on hardware and the underlying operating system, any change in either of these parts of the underlying platform requires a change in the device drivers. Further, device driver development has low productivity as it requires an in-depth understanding of both the hardware and software details and there is a lack of easy-to-use debugging tools. To meet the tight time-to-market design needs for embedded systems in light of these challenges, an effective correct-by-construction device driver development methodology is needed. This thesis proposes a formal model based device driver development methodology to solve this problem. The device access behavior is abstracted by an extended event driven finite state machine based model and specified using a domain specific specification. Linux device driver kernel modules are synthesized from this specification. This operating system based synthesis technique leverages Linux kernel properties and the synthesized drivers integrate seamlessly with Linux, the hosting operating system.

The application of the formal model and the synthesizer enables correct-by-construction device driver development. This thesis demonstrates that the concurrency bugs found in real-world Linux device drivers are prevented by using this methodology. Moreover, this driver specification is significantly smaller than the corresponding Linux device driver. The thesis also shows that the interrupt response time and data exchange speed of the synthesized drivers is similar to or even faster than that of the existing Linux device drivers. This demonstrates that the device driver synthesized by the proposed methodology is practically usable in real-world applications.