基于概率模型检测的Web服务组合验证

Web服务组合验证对提高软件开发效率、实现服务增值具有重要意义。为了验证服务组合的有效性,提出了一种基于概率模型检测的Web服务组合验证方法。首先采用扩展的有限自动机模型建立Web服务组合模型,并将该模型转换为Markov模型,然后采用概率模型检测器PRISM验证服务组合的可靠性,最后通过实例进一步说明该方法的可行性。

有限精度时间自动机的可达性检测

为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series of delay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.

量子马尔可夫链安全性模型检测

本文定义了量子线性时间属性,包括量子安全性,量子不变性,讨论了它们的关系和性质.结合测量一次、测量多次的单向量子有穷自动机,构建了两类乘积量子马尔可夫链,提出了基于自动机技术的量子正则安全性检测方法.通过验证乘积量子马尔可夫链的可达终状态来判断量子正则安全性的可满足性,并给出了可满足性的概率计算公式.作为应用,分析了广义量子loop程序,将程序终止归结为验证量子正则安全性的可满足性.

面向安全攸关系统中小概率事件的统计模型检测

在开放运行环境中,安全攸关系统的不确定性行为有可能导致小概率事件的发生,而此类事件的可靠性指标往往很高,小概率事件一旦发生就会产生灾难性的后果,严重威胁到人们的生命、财产安全.因此,评估、预测小概率事件发生的概率,对于提高系统的可靠性具有重要意义.统计模型检测是一种基于模拟的模型验证技术,结合了系统的快速模拟及统计分析技术,能够有效提高模型检测的效率,适用于验证、评估安全攸关系统的可靠性,但其面临的挑战性问题之一是在可接受的样本数量下,使用统计模型检测技术难以预测、评估小概率事件发生的概率.因此,提出一种改进的统计模型检测框架,设计和开发基于机器学习的统计模型检测器,实现在相对较少的样本数量下预测和评估小概率事件发生的概率.结合轨道交通控制系统中避碰控制案例分析,进一步证明改进后的统计模型检测器能够有效预测和评估安全攸关系统中小概率事件发生的概率.

基于事件确定有限自动机的UML2.0序列图描述与验证

为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性.

基于DNA计算的线性时序逻辑模型检测方法

该文研究基于脱氧核糖核酸(Deoxyribonucleic Acid,DNA)计算的线性时序逻辑(Linear Temporal Logic,LTL)模型检测问题.为此,该文给出了使用粘贴自动机实现LTL模型检测的方法.首先,使用3′-5′型单链DNA分子对LTL公式的有穷状态自动机(Finite State Automata,FSA)模型进行编码,从而获得实现公式的粘贴自动机;其次,使用5′-3′型单链DNA分子对系统模型进行编码,从而获得粘贴自动机的输入字符串;最后,对表征粘贴自动机的DNA单链分子和表征输入字符串的DNA单链分子实施一系列生化反应,即可判定系统是否满足公式.分子生物学仿真实验结果表明:给出的DNA编码序列能达到99.9%的碱基配对正确率,且新方法成功地对所有4种LTL基本公式与5种LTL常见公式实施了检测;与之对照,已有的方法只能有效检测1种LTL基本公式与0种LTL常见公式.在此基础上,对本实验给出的DNA编码方案直接作位数扩展即可拥有对任意给定LTL一般公式的(理论)检测能力.

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对C程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法.事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性.事件自动机将属性规约与C程序本身隔离,不会改变程序的结构.在事件自动机的基础上,提出了自动机可达树的概念.结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法.最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法.实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约.

采用模型检测器的软件安全模型验证方法

针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化UML模型,采用安全扩展有限自动机创建其形式化模型,并使用线性时序逻辑描述安全属性,将形式化模型与安全属性共同作为模型检测器的输入,得到模型是否满足性质的验证结果,从而实现了软件安全设计与验证技术的有机结合.实验结果表明,该方法能够在软件设计初期对所涉及的安全性进行有效分析与验证.

一种系统安全性的形式化验证方法

随着计算机系统应用的深入和广泛,系统安全性越来越成为人们关注的焦点,形式化模型检验是解决系统特性验证问题的一种有效途径,用有限自动机表示系统的设计和实现,用计算树逻辑CTL(ComputationalTreeLogic)公式表示系统的安全特性,探讨了系统安全性形式化验证的方法。

软件安全分析的有穷自动机模型

目的为在软件设计与开发早期阶段对软件安全模型进行有效分析和验证。方法软件安全分析验证法与形式化建模方法。结果提出了一种安全扩展确定有限自动机(safety extended deterministic finite automata,SEDFA)。在使用UMLsec建立软件安全相关的非形式化模型基础上,通过SEDFA准确的描述能够表达安全交互的序列图。首先创建序列图中单个对象的自动机,其次构造对象积自动机,从而得到表示系统整体交互的SEDFA。结论为系统安全属性的验证提供了基础,可作为下一步生成软件安全测试用例。

基于启发式on-the-fly的扩展TGBA模型检测算法

以广义Büchi自动机为研究对象,对其作判空检测能为解决系统的状态空间爆炸问题提供有效途径.但广义Büchi自动机难以适用于安全苛求计算机系统中,只需满足某个可接受条件子集便可作出非空性判断,进而能判断出系统的安全性的情形.文中提出了基于启发式on-the-fly的扩展TGBA模型检测算法,该算法采用ETGBA模型,通过启发式on-the-fly判空检测方法对ETGBA作判空检测时,加强了对不能构成其可接受运行的结点的处理,节省了内存空间,提高了检测效率,从而能较快地作出非空性判断.通过算法的正确性证明及复杂度分析、实验比较与实例研究验证了所提出算法的正确性与实际可行性.与已有算法相比,该算法的通用性更强,当应用于广义Büchi自动机的判空检测时,其时空性能均优于已有算法.

基于启发式NDFS的模型检测新算法

以带有多个可接受条件的广义Büchi自动机为研究对象,提出基于启发式NDFS的模型检测新算法.该算法结合on-the-fly算法与启发式NDFS算法,能较快地判断出广义Büchi自动机非空性,通过理论证明和实验验证了算法的正确性和可行性.与已有算法相比,在广义Büchi自动机非空的情况下,该算法减少了系统状态空间的搜索,提高了检测效率,且能形成相应反例,为缓解形式化验证中的状态空间爆炸问题提供了有效的解决途径,为安全苛求系统的安全性保障提供了有力支撑,丰富了基于模型的软件形式化开发方法.

业务流程的形式化设计与验证

针对如何保证业务流程设计模型与业务需求的一致性问题,在研究有限自动机模型的基础上,提出了一种业务流程的自动机模型构建和验证方法.采用扩展的带约束条件的确定有限自动机对业务流程设计模型进行形式化描述,使用线性时序逻辑表示业务需求,分别给出业务流程设计模型到自动机模型和自动机模型到Promela描述的转换算法,并通过模型检测技术,使用Spin工具验证设计模型是否满足需求性质.若不满足性质,则能够获得反例执行的路径.实例分析表明,该方法可用于业务流程设计的正确性验证.

UML顺序图与状态图的一致性检查

用户可使用UML从不同角度对系统进行建模,但不同视图间存在信息冗余,可能导致视图不一致问题。该文针对具有多种逻辑语义的顺序图提出分析方法,为复杂层次结构的状态图引入有限状态自动机,利用自动机分解算法得到自动机树。制定新的顺序图和状态图一致性检查准则和Promela代码结构,用模型检验工具SPIN进行顺序图及其相关状态图的一致性检验。

一种基于有限精度时间自动机的模型检测工具

基于有限精度时间自动机模型,实现了一种新的数据结构———SDS,用SDS符号化表示状态空间的实时系统模型检测工具,并进行了初步的实验分析,取得了良好的效果。

基于Yices对时间自动机的有界模型检测

为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法。该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测。实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势。

有限精度时间自动机的时钟表示

简要介绍了有限精度时间自动机(FPTA)的基本概念,重点讨论FPTA状态中时钟的表示。FPTA只记录时钟值的整数部分,而用时钟序的概念来模拟表示时钟值小数部分的大小关系,从而减少生成的状态空间。在FPTA模型中,时钟操作的时空性能主要依赖于时钟序的数据结构和算法。提出了用位矩阵来表示时钟序的数据结构POM(Partial-OrderMatrix)。采用该结构的操作算法具有O(n)复杂度,且无需标准化操作;同时,一切操作均可以通过位运算实现,从而大幅度提高时钟操作的时间效率。

基于UPPAAL的数据关联时序有限自动机模型验证

对数据关联过程建立了时序有限自动机模型,时序有限自动机时钟变量只取整数值,从而减小数据关联过程生成的状态空间。在一定的时间约束下,使用模型检测工具UPPAAL对所建模型的关键性质——关联准确性进行了分析和验证。检测结果验证了利用UPPAAL进行数据关联准确性分析的可行性。

基于FSA的模型检测算法研究

自动机就是描述系统行为的模型,通过它可以检测出系统实际工作时发生的状态,经过反复测试,诊断,以达到理想的模型。在基于自动机的模型检测中,前提是需要把非确定性FSA转化为确定性FSA,本文给出了非确定性自动机转换为确定性自动机的算法,最后分析该算法。