基于模型转换的Dafny程序生成与验证研究
发布时间：2021-01-23 04:49
当今世界是一个软件定义一切的时代,尤其在安全攸关领域,需要保证计算机程序的可靠运行。这种可靠性可以通过向程序传递所有可能的测试用例的方法来实现,但该方法难以保证一些输入范围无限的复杂程序的正确性。形式验证的目的是构建程序正确性的数学说明,但所需验证工作是繁琐的,而且容易出错,使用自动验证工具使证明过程自动化是目前形式验证的一种趋势。Dafny是微软研究院创建的一种内置规约结构的编程语言和静态程序证明器,其目的是验证程序的功能正确性并可将程序验证过程完全自动化。这大大减少了繁琐的程序验证过程,极大提高了软件的可靠性。必须认识到,现阶段Dafny程序的生成没有特定的方法和工具,很多问题的Dafny程序都是基于开发者的经验,而且Dafny程序中循环不变式都是从天而降的,基于开发者对算法设计的熟练程度。本文结合算法程序设计方法PAR方法和程序证明器Dafny提出了一个模型驱动的Dafny程序生成与验证方法,通过该方法对一些经典问题进行了算法形式化开发与自动验证,大幅提高了所开发算法程序的可靠性。本文的主要工作包括:一、对Dafny自动验证机理进行了深入剖析并给出示例说明。二、探索出一种模型驱动...
【文章来源】：江西师范大学江西省
【文章页数】：61 页
【学位级别】：硕士
【部分图文】：
软件可信属性图
硕士学位论文4模型的的软件开发三个发展阶段。“模型驱动”最早由OMG(对象管理组织)提出的MDA（model-drivenarchitecture）架构而被人们熟知，MDA是一种基于UML和一系列标准的以模型为中心的开放框架，很好地支持不同应用领域和技术平台。模型驱动的软件开发是软件工程一个重要研究方向，它开放性的理念和模式得到学术界和工业界的广泛关注，而且它的优点很多，包括有效提高软件开发效率，增强软件的可移植性，以及协同工作的能力和可维护性。下图是各种开发技术的比较：图1-2：软件开发技术比较模型驱动的软件开发是当前的研究热点，已经具备了相关技术基矗OMG推出了关于MOF(MetaObjectFacility,元对象机制)和MDA的规范，但MDA的可操作性研究还需进一步发展。目前MDA开发工具市场现状有：SDK开发商如Borland也推出了基于MDA的开发平台，微软也将MDA概念纳入.NET开发平台，但它们的开发期模型都是向自己的平台映射。目前模型驱动还有待研究的问题有：元模型和模型映射方法论研究、领域元模型的建立、模型映射技术的开发等[15]。1.2.2基于定理证明器的形式验证通过纯手工形式结合一种形式验证方法(如Floyd断言[16]、Hoare公理[17]等)对程序的正确性进行验证的过程因为过于繁琐复杂，很容易产生人为性错误。形式验证通过定理证明和模型检测两种方法来提高用户对规约和系统的可信度，定理证明以程序逻辑为基础通过演绎推理的方式对命题开展证明。典型的基于定理证明的形式验证方法有Floyd-Hoare逻辑验证系统、Owicki和Gries的并发程序验证方法、Jones的Rely-Guarantee方法和并发分离逻辑[18]。因此对一些手工验证工作机械证明就有了定理证明器，它们在硬件和软件验证上发挥了很大作用，通过将构造证明过程转换为编写程序的过
硕士学位论文8图2-1：最弱前置谓词由图可知，最弱的前提条件WP(c，B)任何状态q都成立，q中的所有c后继状态均满足B。用式子表示就是：qWP(c,B)iffq′∈Q.qC→q′q′B然后根据程序P的结构递归的计算WP(P,B)。本文第三章在说明Dafny程序的内在机理的时候将程序转换为了GC程序，然后通过对GC程序应用最弱前置谓词规则一步步得到验证条件VC。具体的规则有以下这些：WP(assumeb,B)=bBWP(assertb,B)=b∧BWP(havocx,B)=B[a/x]WP(c1;c2,B)=WP(c1,WP(c2,B))WP(c1||c2,B)=WP(c1,B)∧WP(c2,B)2.2模型驱动软件开发方法随着互联网扩展到社会的每个角落，由于平台和技术工具的变革加快，出现了许多新的问题，如新平台和应用程序怎么与遗留系统互操作等，这些都是互联网正面临的新的挑战。新技术不断出现在新的应用领域，组织如何确保其关键任务信息系统植根于适应新硬件功能和软件平台的标准是研究的难点[26]。OMG（ObjectManagementGroup，即对象管理组织）通过模型驱动架构的MDA（ModelDrivenArchitecture）架构解决了这一现实问题，MDA[20]是一种新的软件系统开发的设计方法，核心是将系统应用与其实现的技术平台解耦。MDA方法的提出主要有三个目标：一是改变以代码为中心的软件开发方法；二是解决不同平台和技术路线之间的集成和互操作问题；三是适应未来出现的新技术和新平台。该架构涉及的模型主要有计算无关的模型CIM（ComputationIndependentModel）、平台无关模型PIM（PlatformIndependentModel）、平台相关模型PSM（PlatformSpecificModel）和代码[27]。从CIM、PIM、PSM到代码，是一个从抽象到具体的过程。MDA的特点是将PIM到PSM的转换自动化了，然后PSM经由MDA工具自动生成代码，极大提升了开发
【参考文献】：
期刊论文
[1]软件形式化验证专题前言[J]. 贺飞,张立军. 软件学报. 2019(07)
[2]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明. 软件学报. 2019(01)
[3]算法的形式化推导与基于Isabelle的自动化验证[J]. 齐蕾蕾,杨庆红,游颖. 江西师范大学学报(自然科学版). 2018(04)
[4]WSDL→Radl-WS生成方法及自动转换系统[J]. 张琦,王昌晶,罗海梅,左正康,石海鹤,郭帆. 江西师范大学学报(自然科学版). 2018(03)
[5]“可信软件基础研究”重大研究计划结题综述[J]. 何积丰,单志广,王戟,蒲戈光,房毓菲,刘克,赵瑞珍,张兆田. 中国科学基金. 2018(03)
[6]PAR平台中若干软件构件形式化验证技术研究[J]. 胡启敏,薛锦云,游珍,程着. 计算机工程与科学. 2018(02)
[7]SMT求解技术的发展及最新应用研究综述[J]. 王翀,吕荫润,陈力,王秀利,王永吉. 计算机研究与发展. 2017(07)
[8]基于模型的自适应方法综述[J]. 赵天琪,赵海燕,张伟,金芝. 软件学报. 2018(01)
[9]基于分离逻辑的程序验证研究综述[J]. 秦胜潮,许智武,明仲. 软件学报. 2017(08)
[10]基于KeY的程序分析和验证[J]. 夏新凯,陈冬火. 软件. 2016(03)
硕士论文
[1]基于模型驱动的WSDL→Radl-WS生成方法及自动转换系统[D]. 张琦.江西师范大学 2018
[2]递推技术在算法设计中的应用研究[D]. 张园.江西师范大学 2012
[3]基于PAR平台的最弱前置谓词生成器的设计与实现[D]. 杨晨.江西师范大学 2010
[4]PAR方法在组合数学问题中的应用研究[D]. 孙凌宇.江西师范大学 2005
本文编号：2994583
【文章来源】：江西师范大学江西省
【文章页数】：61 页
【学位级别】：硕士
【部分图文】：
软件可信属性图
硕士学位论文4模型的的软件开发三个发展阶段。“模型驱动”最早由OMG(对象管理组织)提出的MDA（model-drivenarchitecture）架构而被人们熟知，MDA是一种基于UML和一系列标准的以模型为中心的开放框架，很好地支持不同应用领域和技术平台。模型驱动的软件开发是软件工程一个重要研究方向，它开放性的理念和模式得到学术界和工业界的广泛关注，而且它的优点很多，包括有效提高软件开发效率，增强软件的可移植性，以及协同工作的能力和可维护性。下图是各种开发技术的比较：图1-2：软件开发技术比较模型驱动的软件开发是当前的研究热点，已经具备了相关技术基矗OMG推出了关于MOF(MetaObjectFacility,元对象机制)和MDA的规范，但MDA的可操作性研究还需进一步发展。目前MDA开发工具市场现状有：SDK开发商如Borland也推出了基于MDA的开发平台，微软也将MDA概念纳入.NET开发平台，但它们的开发期模型都是向自己的平台映射。目前模型驱动还有待研究的问题有：元模型和模型映射方法论研究、领域元模型的建立、模型映射技术的开发等[15]。1.2.2基于定理证明器的形式验证通过纯手工形式结合一种形式验证方法(如Floyd断言[16]、Hoare公理[17]等)对程序的正确性进行验证的过程因为过于繁琐复杂，很容易产生人为性错误。形式验证通过定理证明和模型检测两种方法来提高用户对规约和系统的可信度，定理证明以程序逻辑为基础通过演绎推理的方式对命题开展证明。典型的基于定理证明的形式验证方法有Floyd-Hoare逻辑验证系统、Owicki和Gries的并发程序验证方法、Jones的Rely-Guarantee方法和并发分离逻辑[18]。因此对一些手工验证工作机械证明就有了定理证明器，它们在硬件和软件验证上发挥了很大作用，通过将构造证明过程转换为编写程序的过
硕士学位论文8图2-1：最弱前置谓词由图可知，最弱的前提条件WP(c，B)任何状态q都成立，q中的所有c后继状态均满足B。用式子表示就是：qWP(c,B)iffq′∈Q.qC→q′q′B然后根据程序P的结构递归的计算WP(P,B)。本文第三章在说明Dafny程序的内在机理的时候将程序转换为了GC程序，然后通过对GC程序应用最弱前置谓词规则一步步得到验证条件VC。具体的规则有以下这些：WP(assumeb,B)=bBWP(assertb,B)=b∧BWP(havocx,B)=B[a/x]WP(c1;c2,B)=WP(c1,WP(c2,B))WP(c1||c2,B)=WP(c1,B)∧WP(c2,B)2.2模型驱动软件开发方法随着互联网扩展到社会的每个角落，由于平台和技术工具的变革加快，出现了许多新的问题，如新平台和应用程序怎么与遗留系统互操作等，这些都是互联网正面临的新的挑战。新技术不断出现在新的应用领域，组织如何确保其关键任务信息系统植根于适应新硬件功能和软件平台的标准是研究的难点[26]。OMG（ObjectManagementGroup，即对象管理组织）通过模型驱动架构的MDA（ModelDrivenArchitecture）架构解决了这一现实问题，MDA[20]是一种新的软件系统开发的设计方法，核心是将系统应用与其实现的技术平台解耦。MDA方法的提出主要有三个目标：一是改变以代码为中心的软件开发方法；二是解决不同平台和技术路线之间的集成和互操作问题；三是适应未来出现的新技术和新平台。该架构涉及的模型主要有计算无关的模型CIM（ComputationIndependentModel）、平台无关模型PIM（PlatformIndependentModel）、平台相关模型PSM（PlatformSpecificModel）和代码[27]。从CIM、PIM、PSM到代码，是一个从抽象到具体的过程。MDA的特点是将PIM到PSM的转换自动化了，然后PSM经由MDA工具自动生成代码，极大提升了开发
【参考文献】：
期刊论文
[1]软件形式化验证专题前言[J]. 贺飞,张立军. 软件学报. 2019(07)
[2]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明. 软件学报. 2019(01)
[3]算法的形式化推导与基于Isabelle的自动化验证[J]. 齐蕾蕾,杨庆红,游颖. 江西师范大学学报(自然科学版). 2018(04)
[4]WSDL→Radl-WS生成方法及自动转换系统[J]. 张琦,王昌晶,罗海梅,左正康,石海鹤,郭帆. 江西师范大学学报(自然科学版). 2018(03)
[5]“可信软件基础研究”重大研究计划结题综述[J]. 何积丰,单志广,王戟,蒲戈光,房毓菲,刘克,赵瑞珍,张兆田. 中国科学基金. 2018(03)
[6]PAR平台中若干软件构件形式化验证技术研究[J]. 胡启敏,薛锦云,游珍,程着. 计算机工程与科学. 2018(02)
[7]SMT求解技术的发展及最新应用研究综述[J]. 王翀,吕荫润,陈力,王秀利,王永吉. 计算机研究与发展. 2017(07)
[8]基于模型的自适应方法综述[J]. 赵天琪,赵海燕,张伟,金芝. 软件学报. 2018(01)
[9]基于分离逻辑的程序验证研究综述[J]. 秦胜潮,许智武,明仲. 软件学报. 2017(08)
[10]基于KeY的程序分析和验证[J]. 夏新凯,陈冬火. 软件. 2016(03)
硕士论文
[1]基于模型驱动的WSDL→Radl-WS生成方法及自动转换系统[D]. 张琦.江西师范大学 2018
[2]递推技术在算法设计中的应用研究[D]. 张园.江西师范大学 2012
[3]基于PAR平台的最弱前置谓词生成器的设计与实现[D]. 杨晨.江西师范大学 2010
[4]PAR方法在组合数学问题中的应用研究[D]. 孙凌宇.江西师范大学 2005
本文编号：2994583
本文链接：https://www.wllwen.com/shoufeilunwen/xixikjs/2994583.html
