基于迁移系统分析的线性混成系统安全验证

混成自动机行为中既包含离散行为又包含连续行为,非常复杂。其安全性验证问题难以解决,即使是线性混成自动机,它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集,复杂度高,可处理问题规模非常有限。为了避免这类问题,实现了一种新的工具。该工具将线性混成自动机表达为等价的迁移系统,并利用迁移系统上不变式生成相关工作对混成自动机进行验证。实验数据表明,方法有效可行,工具具有良好的性能。     

基于算法框架的可重用部件设计与实现

对算法程序的功能规约进行等价变换,可以自然而且方便地得到求解问题设计思想的精确表达,即循环不变式。抽象算法又可以通过循环不变式获得。对算法程序中的算子进行提取、抽象就可以得到算法框架,而算法框架可以设计出可重用部件。文章通过对数组段极值问题的求解,展示了形式化推导不仅可以得到正确、高效的算法程序,而且具有软件重用的功能,并进一步给出了利用可重用部件求解数组段极值问题的C++实现。     

基于DISCOVERER的Petri网不变式自动生成*

在Petri网的验证中,代数不变式起着非常重要的作用。将Petri网建模为半代数变迁系统,提出了自动生成不变式的算法,该不变式有助于更好地分析Petri网可达空间。算法首先将Petri网的不变式假定为一个含参数系统,然后通过求解半代数系统来求解不变式中的参数;最后,基于DISCOVERER和QEPCAD等Maple软件包实现了该算法,并通过实例说明了算法的有效性。     

逐步求精的一种模型

提出一种支持程序开发的结构化方法．该方法以一种简单的问题分解策略为基础，比Ｗｉｒｔｈ－Ｄｉｊｋｓｔｒａ的自顶向下逐步求精方法更利于面向目标的程序设计．由该方法可知，一个程序可经一系列求精而开发出来，每一步求精都能为相应的最弱前置条件序列建立后置条件．这种策略使情况分析减少到极限，简化了结构化程序的证明，并保证了程序结构和数据结构之间的对应．     

用Petri网描述程序精化中的循环不变式

形式化方法把程序看成规范,形式化开发方法包括形式规范和规范(程序)的精化.精化演算方法能够通过演算的方式,把规范逐步精化为程序.然而,演化的过程依赖于开发人员的经验,整个过程全部都是手动的.形式化方法的最高目标是软件自动化,使得能从规范自动开发出正确的程序.因而用Petri网来描述程序精化中的循环不变式,希望以此作为软件自动化的一个探索.     

形式化开发非递归Koch曲线算法

形式化方法是构建可信软件的重要途径。Koch曲线是典型的分形图形。基于形式化方法PAR及循环不变式开发策略,开发了Koch曲线非递归算法,并对其进行了形式化的正确性证明。在得到求解Koch曲线算法的循环不变式的同时,直接得到易读、高效且可靠的非递归算法。对使用形式化方法及循环不变式开发策略开发分形程序非递归算法作了较深入的实践和探讨。     

循环不变式开发技术研究

高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。本文研究了众多现有循环不变式开发方法中较为典型的几种方法,指出了它们的基本原理、技术难点、特点及效果,旨在探寻循环不变式本质特征,从而为研究更简单、有效的生成方法提出指导。     

Hanoi塔非递归算法的形式化推导和正确性验证

关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性.     

基于不变式生成的循环停机性验证

循环的停机性验证是程序验证中的一个难点。程序不变式用来描述程序变量的取值关系,其中线性不变式可以帮助描述程序变量间的线性关系,循环不变式能够有效刻画循环中的变量关系。本文基于线性不变式和多项式循环不变式的生成,将循环的停机性验证转化为求解一个最优化问题,给出了一个实用的程序停机性验证框架。基于该框架可以自动地验证程序的停机性,并给出循环的复杂度上界。实验结果说明了该方法的实用性。     

PAR方法在组合游戏上的应用

简述了薛锦云教授所创的PAR方法和组合游戏(Nim)之后,本文运用PAR方法详细推演出解决组合游戏中的一个典型例子(Nim)的算法的数学模型。在此数学模型的基础之上,再次运用PAR方法推演出解决Nim的简短的核心算法。