软件系统的自动验证

摘要

软件系统(例如，软件栈)的软件代码可以被验证为符合规范。可以使用编译器来编译软件系统的高级语言实现以创建汇编语言实现。对应于软件系统的高级规范可以被转换为低级规范。验证器可以验证汇编语言实现功能上符合在低级规范中所描述的属性。以这种方式，软件系统(例如，包括操作系统、(一个或多个)设备驱动程序、软件库以及一个或多个应用的完整软件系统)可以在低级(例如，汇编语言级)上被验证。