[发明专利]一种同步语言程序多属性增量模型检测方法在审
申请号: | 202211523760.1 | 申请日: | 2022-11-30 |
公开(公告)号: | CN116089264A | 公开(公告)日: | 2023-05-09 |
发明(设计)人: | 陈哲;方雨瑶 | 申请(专利权)人: | 南京航空航天大学 |
主分类号: | G06F11/36 | 分类号: | G06F11/36;G06F8/72;G06F9/54 |
代理公司: | 南京经纬专利商标代理有限公司 32200 | 代理人: | 王慧 |
地址: | 210016 江*** | 国省代码: | 江苏;32 |
权利要求书: | 查看更多 | 说明书: | 查看更多 |
摘要: | 本发明公开了一种同步语言程序多属性增量模型检测方法,包括步骤:S1,对同步语言程序进行词法和语法分析,得到抽象语法树,然后将复杂程序转化为仅包含唯一节点、内存深度为1的简单程序;S2,使用程序切片算法删除与待验证属性无关的数据流,删除与待验证属性无关的等式,得到一个化简后的程序;S3,为有界模型检测引擎线程构建基础公式,为归纳法引擎线程构建归纳公式;S4,并行执行有界模型检测引擎线程、归纳法引擎线程和程序抽象引擎线程,并通过消息传递机制控制这些线程之间的同步。本发明能够加快验证速度,从而缓解现有模型检测技术验证速度较慢的问题。 | ||
搜索关键词: | 一种 同步 语言 程序 属性 增量 模型 检测 方法 | ||
【主权项】:
暂无信息
下载完整专利技术内容需要扣除积分,VIP会员可以免费下载。
该专利技术资料仅供研究查看技术是否侵权等信息,商用须获得专利权人授权。该专利全部权利属于南京航空航天大学,未经南京航空航天大学许可,擅自商用是侵权行为。如果您想购买此专利、获得商业授权和技术合作,请联系【客服】
本文链接:http://www.vipzhuanli.com/patent/202211523760.1/,转载请声明来源钻瓜专利网。