Automatic device driver synthesis with termite
Automatic device driver synthesis with termite
复制标题
使用白蚁自动合成设备驱动程序
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Gernot Heiser
中科院分区：
文献类型：
--
作者：
L. Ryzhyk;P. Chubb;I. Kuz;Etienne Le Sueur;Gernot Heiser
有故障的设备驱动程序会因停机时间和数据丢失造成重大损害。通过改进驱动程序开发流程，从构建上保证其正确性，这一问题可以得到缓解。我们通过根据设备接口的形式化规范自动合成驱动程序来实现这一点，从而减少人为错误对驱动程序可靠性的影响，并有可能降低开发成本。
我们提出了一种具体的驱动程序合成方法和名为Termite的工具。我们讨论了驱动程序合成的方法、技术和实际限制，并对使用我们的工具为Linux生成的重要驱动程序进行了评估。我们表明，生成的驱动程序的性能与同等的手动开发的驱动程序相当。此外，我们通过根据用于Linux的相同规范为FreeBSD生成驱动程序，证明了设备规范可以在不同的操作系统中重复使用。
Faulty device drivers cause significant damage through down time and data loss. The problem can be mitigated by an improved driver development process that guarantees correctness by construction. We achieve this by synthesising drivers automatically from formal specifications of device interfaces, thus reducing the impact of human error on driver reliability and potentially cutting down on development costs.
We present a concrete driver synthesis approach and tool called Termite. We discuss the methodology, the technical and practical limitations of driver synthesis, and provide an evaluation of non-trivial drivers for Linux, generated using our tool. We show that the performance of the generated drivers is on par with the equivalent manually developed drivers. Furthermore, we demonstrate that device specifications can be reused across different operating systems by generating a driver for FreeBSD from the same specification as used for Linux.