Partial abstract: “This thesis details such a device driver synthesis and verification tool chain under the Linux operating system. We make the following contributions. First, we present an approach for automatically synthesizing driver code based on Model Integrated Computing (MIC) concepts. Second, we define a formal graph based Domain Specific Modeling Language (DSML) for specifying a device driver model and its environment. Third, we use model checking techniques for verifying that the resulting device driver constitutes a faithful device behavior while eliminating errors introduced during manual abstractions.

“…the user-defined driver model is the input and the output is the resulting driver. The input model includes the software behavior of the hardware device and the I/O interface between user programs, low level device control and the driver, which is defined formally by the programmer with our DSML. Finally, this information will be converted into the implementation of the driver by the code generator.”