[发明专利]软件系统的自动验证有效
| 申请号： | 201580053927.4 | 申请日： | 2015-10-01 |
| 公开（公告）号： | CN107111713B | 公开（公告）日： | 2020-02-07 |
| 发明（设计）人： | C·霍布利泽尔;B·帕诺;J·R·洛奇;J·R·豪厄尔;B·D·齐尔 | 申请（专利权）人： | 微软技术许可有限责任公司 |
| 主分类号： | G06F21/52 | 分类号： | G06F21/52 |
| 代理公司： | 11256 北京市金杜律师事务所 | 代理人： | 王茂华;丁君军 |
| 地址： | 美国华*** | 国省代码： | 美国;US |
| 权利要求书： | 查看更多 | 说明书： | 查看更多 |
| 摘要： | 软件系统(例如，软件栈)的软件代码可以被验证为符合规范。可以使用编译器来编译软件系统的高级语言实现以创建汇编语言实现。对应于软件系统的高级规范可以被转换为低级规范。验证器可以验证汇编语言实现功能上符合在低级规范中所描述的属性。以这种方式，软件系统(例如，包括操作系统、(一个或多个)设备驱动程序、软件库以及一个或多个应用的完整软件系统)可以在低级(例如，汇编语言级)上被验证。 | ||
| 搜索关键词： | 软件 系统 自动 验证 | ||
【主权项】：
1.一种计算机实现的方法，包括：/n接收以高级语言编写的软件代码，所述软件代码包括多个组件，所述多个组件包括操作系统和至少一个应用；/n编译所述软件代码以创建与所述软件代码相对应的汇编语言代码；/n接收高级规范，所述高级规范指定由所述软件代码执行的一个或多个功能；/n至少部分地基于所述高级规范，生成低级规范；/n验证所述汇编语言代码的输出不支持秘密数据被确定，所述秘密数据包括一个或多个私钥；/n验证所述汇编语言代码根据所述低级规范表现以执行由所述高级规范制定的所述一个或多个功能；以及/n提供所述汇编语言已经被验证执行所述一个或多个功能的指示。/n
下载完整专利技术内容需要扣除积分，VIP会员可以免费下载。
该专利技术资料仅供研究查看技术是否侵权等信息，商用须获得专利权人授权。该专利全部权利属于微软技术许可有限责任公司，未经微软技术许可有限责任公司许可，擅自商用是侵权行为。如果您想购买此专利、获得商业授权和技术合作，请联系【客服】
本文链接：http://www.vipzhuanli.com/patent/201580053927.4/，转载请声明来源钻瓜专利网。
