论文摘要
目前软件工业界面临着产品功能越来越复杂和推出产品周期越来越短的双重压力。软件工程的一个主要目标就是在复杂性增加的情况下仍能构造正确可靠的系统。为了达到上述目标,形式化方法在软件开发中得到了广泛的应用,特别是模型检查技术。本文提出了一种基于SPIN的命题投影时序逻辑的模型检查方法。在此方法中,系统的性质用命题投影时序逻辑公式来描述,随后这个公式被转换为其永非断言;然后系统模型用Buchi自动机来刻画;最后通过SPIN完成模型检查,即检查系统是否满足期望的性质。为了实现这一目的,文中设计并实现了命题投影时序逻辑公式的解释转换器,以便将命题投影时序逻辑公式自动转换为Promela形式的永非断言。该转换器首先将待验证的命题投影时序逻辑公式转换为其正则式以及正则图,然后通过正则图可以得到所需的永非断言。将该转换器与模型检查器SPIN相结合,使用命题投影时序逻辑公式来在SPIN中描述系统的性质,这样基于命题投影时序逻辑的模型检查就能在SPIN中完成。
论文目录
相关论文文献
- [1].The MathWorks为安全关键系统提供自动化模型检查支持[J]. 电信科学 2008(05)
- [2].有界模型检查可执行文件的安全属性[J]. 小型微型计算机系统 2008(09)
- [3].基于模型检查的货运飞船推进剂在轨补加任务故障树分析方法研究[J]. 质量与可靠性 2018(06)
- [4].面向模型检查的NuSMV统一建模方法[J]. 系统工程与电子技术 2018(07)
- [5].一种基于模型检查的嵌入式软件验证方法[J]. 单片机与嵌入式系统应用 2009(05)
- [6].程序模型检查器综述[J]. 计算机科学 2009(04)
- [7].基于限界模型检查的Web服务行为失配检测[J]. 计算机科学 2012(06)
- [8].时态认知逻辑CTL*K的符号化模型检查算法[J]. 计算机科学 2009(05)
- [9].基于规则设定的全方位碰撞检查技术[J]. 建筑与文化 2014(08)
- [10].面向对象的CAD模型检查方法研究[J]. 制造业自动化 2009(04)
- [11].异构多智能体系统模型检查[J]. 软件学报 2018(06)
- [12].基于CATIA二次开发技术的模型质量检查[J]. 新技术新工艺 2015(01)
- [13].SOC的形式化验证方法[J]. 武汉大学学报(工学版) 2008(06)
- [14].BIM模型智能检查工具研究与应用[J]. 土木建筑工程信息技术 2018(02)
- [15].基于STP方法的SCADE模型形式化验证框架[J]. 计算机工程 2019(10)
- [16].PROMELA语义引擎执行研究[J]. 电脑知识与技术 2008(35)
- [17].RPKI增量同步Delta协议的形式化检测与实现[J]. 计算机系统应用 2018(11)
- [18].基于模型检查的嵌入式软件构件化分析与验证[J]. 现代电子技术 2016(24)
- [19].模型检查在测试用例生成中的应用[J]. 常熟理工学院学报 2008(10)
- [20].SMV的观察迁移系统的模型检测分析[J]. 计算机工程与设计 2008(18)
- [21].区间时序逻辑的模型检查[J]. 西安电子科技大学学报 2009(02)
- [22].SPIN语义引擎执行方式研究[J]. 计算机与现代化 2009(11)
- [23].基于并行环境的模型检查技术研究与实现[J]. 太原师范学院学报(自然科学版) 2012(02)
- [24].程序切片技术在并发程序模型检查中的应用[J]. 计算机技术与发展 2008(11)
- [25].一种新的Statechart模型验证方法[J]. 计算机科学 2011(02)
- [26].BIM系列软件在建筑碰撞检查时的应用[J]. 山东工业技术 2019(03)
- [27].一种基于System C语言的模型检测方法[J]. 广西民族大学学报(自然科学版) 2016(03)
- [28].XML Schema特征提取算法[J]. 计算机科学 2015(S2)
- [29].多速率混合系统的模型检查[J]. 西安电子科技大学学报 2008(01)
- [30].业务过程模型的Petri网形式化检查方法[J]. 计算机集成制造系统 2011(05)