基于定理证明器Coq的形式语义验证研究

发布时间：2021-01-26 02:34

　　随着现代计算机系统的规模越来越大、复杂性越来越高,如何开发可信的软硬件系统已经成为计算机科学发展的巨大挑战。形式化方法是以数学理论为基础,对计算机系统进行严格地规约、建模与验证,实现系统的可信验证。形式化方法已经成为软件开发过程中不可或缺的一个环节,如何使用交互式的定理证明器对软件系统进行机械定义与验证是其中的一个研究重点。通过机械证明模型中的定理可以找出模型中存在的问题和漏洞,从而进一步提高模型的可靠性。本文的工作致力于研究软件开发过程中不同层次的形式语义验证,以代码层面的多线程离散事件仿真语言和系统建模层面的统一建模语言为研究对象,提出了将基于定理证明器Coq的机械验证引入到形式语义验证的研究中,使得基于Coq的机械验证涵盖整个软件开发生命周期。多线程离散事件仿真语言MDESL是一种类似于Verilog的底层硬件描述语言,在定理证明器Coq中实现了从MDESL代数语义中机械生成操作语义的过程,并且机械验证了生成操作语义的正确性和完备性。基于程序统一理论（UTP）,使用Coq中的高阶逻辑特性对MDESL的指称语义进行机械刻画,对代数定律的正确性进行机械验证。统一建模语言UML是一种通... 

【文章来源】：华东师范大学上海市 211工程院校 985工程院校 教育部直属院校

【文章页数】：189 页

【学位级别】：博士

【部分图文】：

查找当前活动子进程的示例

UML的发展历史[5]

CoqIDE中的交互式证明会话

【参考文献】：
期刊论文
[1]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明.  软件学报. 2019(01)

博士论文
[1]移动分布式系统的进程演算BigrTiMo及其形式语义研究[D]. 谢宛玲.华东师范大学 2019
[2]UML动态行为图的机械语义形式验证与精化研究[D]. 窦亮.华东师范大学 2015

硕士论文
[1]UML模型一致性检测的研究与设计[D]. 朱晨.上海交通大学 2007



本文编号：3000318