Automatic verification of active device drivers
Automatic verification of active device drivers
复制标题
自动验证活动设备驱动程序
DOI：
10.1145/2626401.2626424
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Amani S
中科院分区：
文献类型：
--
作者：
Amani S
我们开发了一个实用的解决方案，自动验证设备驱动程序和操作系统之间的接口的问题。我们的解决方案依赖于改进的驱动程序架构和验证工具的组合。与以前的建议，验证友好的驱动程序，我们的方法支持驱动程序编写的C语言，可以在任何现有的操作系统。我们基于Linux的评估表明，这种方法放大了现有的模型检查工具的力量，在检测驱动程序的错误，使其有可能验证的属性是超出了传统技术的范围。
We develop a practical solution to the problem of automatic verification of the interface between device drivers and the operating system. Our solution relies on a combination of improved driver architecture and verification tools. Unlike previous proposals for verification-friendly drivers, our methodology supports drivers written in C and can be implemented in any existing OS. Our Linuxbased evaluation shows that this methodology amplifies the power of existing model checking tools in detecting driver bugs, making it possible to verify properties that are beyond the reach of traditional techniques.
登录
查看更多内容
satabs：C 程序的位精确验证器 -（竞赛贡献）
DOI：
--
发表时间：
2012
期刊：
International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子：
--
作者：
Gérard Basler;Alastair F. Donaldson;A. Kaiser;D. Kroening;Michael Tautschnig;T. Wahl
通讯作者：
T. Wahl
使用 CSP 和细化检查面向流程的操作系统行为
DOI：
10.1145/1713254.1713265
发表时间：
2010
期刊：
ACM SIGOPS Operating Systems Review
影响因子：
--
作者：
Barnes F
通讯作者：
Barnes F
Boom：布尔程序模型检查更进一步
影响因子：
0.8
作者：
Gérard Basler;M. Hague;D. Kroening;C. Ong;T. Wahl;Haoxian Zhao
通讯作者：
Haoxian Zhao
奇点操作系统中快速可靠的基于消息的通信的语言支持
DOI：
10.1145/1217935.1217953
发表时间：
2006
期刊：
Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006
影响因子：
--
作者：
M. Fähndrich;Mark Aiken;C. Hawblitzel;O. Hodson;G. Hunt;J. Larus;Steven P. Levi
通讯作者：
Steven P. Levi
两年基于 μ-Kernel 的操作系统的经验
DOI：
--
发表时间：
1991
期刊：
OPSR
影响因子：
--
作者：
J. Liedtke;U. Bartling;U. Beyer;D. Heinrichs;R. Ruland;G. Szalay
通讯作者：
G. Szalay