基于Petri网的位置敏感工作流建模与正确性验证方法

针对移动业务过程中对位置信息建模和分析的需求,结合目前已有的工作流建模方法,提出一种针对位置敏感工作流进行建模和正确性验证的方法。该模型以工作流网为基础,结合6种描述位置之间关系的原语,以位置约束的形式定义业务流程中的位置信息及其与活动之间的关系,然后基于Petri网的状态可达图得出对所建立模型进行正确性检查的方法。基于ProM平台开发了一个位置敏感工作流的建模工具,验证了所提建模方法的可行性和算法的正确性。

屈服准则在有限元软件中实现的正确性验证

基于向后欧拉完全隐式积分方法,采用回映算法将Yld2000-2d屈服准则嵌入ABAQUS商业有限元软件.基于严格的力学推导,提出了能够有效验证屈服准则嵌入工作的正确性的方法.针对5754O铝合金板,采用上述方法验证了Yld2000-2d屈服准则在ABAQUS有限元软件中的嵌入工作的正确性.

基于静态分析的强制访问控制框架的正确性验证

现阶段对操作系统的强制访问控制框架的正确性验证的研究主要集中于对授权钩子放置的验证.文中基于TrustedBSD MAC框架对强制访问控制框架的正确性验证问题进行了研究,在授权钩子放置验证的基础上,提出了安全标记的完全初始化验证和完全销毁验证.为了实现上述验证,文中提出了一个路径敏感的、基于用户自定义检查规则的静态分析方法.该方法通过对集成于编译器的静态分析工具mygcc进行扩展来验证强制访问控制框架的钩子放置的准确性和完备性.该方法具有完全的路径覆盖性,且具有低的误报率和时间开销.

基于模型检测的服务规则路由正确性验证方法

基于模型检测技术,提出了一种适用于集成了规则引擎的企业服务总线中的消息规则路由的正确性验证方法。首先将基于规则的消息路由转换为服务模型六元组,然后再将服务模型六元组转换为NuSMV输入程序,最后通过NuSMV工具实现自动化验证。给出了一个贷款审批业务的服务规则。路由的正确性验证实例证明了该方法的可行性。

Web服务过程建模及其逻辑正确性验证

为研究Web服务过程的逻辑正确性及其形式化验证方法,提出一种基于着色Petri网的Web服务过程模型,给出了逻辑正确性的形式化定义。为验证其正确性,提出通信可达树的概念,借助通信可达树的某些性质来验证服务的逻辑正确性,并给出了正确性判定定理。另外,为了简化组合服务逻辑正确性的验证过程,阐述了组合服务与其子服务之间的内在关系。最后,通过一个应用实例验证了方法的可用性。

基于语法树的程序正确性验证模型及算法设计

基于语法树的程序正确性验证方法是目前程序正确性验证全新的研究领域,该方法以程序的语法树作为程序正确性的检验对象,运用适当的树匹配算法,来验证目标程序的正确性。该文在介绍基于语法树的程序正确性验证方法的基础上,借鉴无序标签树匹配的相关研究成果,结合软件构件的查询技术,提出一种新的XML路径查询模型和树匹配算法,并展示了STM在程序正确性验证方面的前景。

防火墙包过滤规则正确性验证

随着网络技术的迅速发展,应用网络技术和共享网络资源已经成为我们日常学习、工作中必不可少的部分。只要网络存在,安全问题就会作为一个极其重要和极具威胁性的问题存在。目前市场上有各种各样的安全工具,技术最成熟、最早产品化的就是防火墙,防火墙是安全策略的技术实现,包过滤系统是防火墙最基本、最重要、最核心部分。防火墙的包过滤规则是根据实际需要的安全策略来制定的,对规则集应该考虑整体是否有效、规范,而不应该是规则集中的每条规则是否有效、规范。本文实现了包过滤规则在应用之前能够进行规则的冲突检测,避免规则之间出现矛盾、冗余,便于规则的管理和维护,也便于制定较为完备的安全策略。

基于XYZ/SE的软件部分正确性验证

针对软件形式化描述和正确性验证研究中存在的问题,提出了基于XYZ/SE的统一框架研究该问题。在该框架下,基于逐步求精思路对软件进行抽象;对软件整体进行形式化描述和部分正确性验证;对抽象得到的软件各部分进行形式化描述和部分正确性验证;进行调整和验证,即:如果推导结果与预期不一致,则需要重写相关程序或者回溯检查推导过程是否存在错误,直至程序部分正确性得到验证为止。以国库信息处理系统为对象,分析了基于XYZ/SE的统一框架性能。分析表明,基于该框架能够对软件的不同抽象层次进行规范描述,实现从抽象(静态语义)到具体(动态语义)的平滑过渡。同时,基于XYZ/SE的统一框架也可以表示Hoare逻辑推演规则。

基于语法树和程序正确性验证研究

提出了一种新的基于语法树的程序正确性验证方法(STM方法)。在理论和算法上对方法的实现进行了初步探讨,并结合XML技术提出了一套实现这一方法的切实可行的解决方案。

基于抽象解释的函数不变量正确性验证

函数不变量检测是提高软件质量的一种有效方法.针对检测方法可能带来无效的函数不变量的缺陷,提出一种以抽象解释理论为基础的函数不变量的正确性验证方法.首先将函数不变量转化成多项式关系;其次结合多项式程序与最弱前置条件抽象解释分析多项式关系正确性的判断依据;最后构造多项式关系算法,凭借得到的结果验证函数不变量正确与否.同时通过一个C程序中的函数不变量为例对该验证方法进行说明.

Web服务质量建模及其正确性验证

针对现有的Web服务质量模型主要考虑的都是通用的服务质量属性,没有考虑特定的Web服务属性在评价中的作用,提出了一个新的Web服务质量模型,它引入了一个特定领域的服务质量属性,该模型包括三个子模型。模型中建立了相关的服务质量树和目标对象树,通过量化指标子模型对目标对象进行量化,形成相应的服务权重树。该模型既可适应用于单个的Web服务请求,也可以用于多个服务组合而成的请求。通过一个应用实例验证了模型的正确性和可用性。

RGPS服务层元模型正确性验证

随着网络式软件复杂程度的日益增加,如何确保网络式软件功能和性能的正确性越发重要。根据网络式软件的特点,在RGPS需求元建模框架的指导下,提出RGPS服务层元模型正确性验证。首先用BPEL语言和WSDL语言把RGPS服务层元模型描述成BPEL模型,再用Promela语言实现BPEL模型的建模,最后输入LTL公式对RGPS服务层元模型进行安全性和活性验证分析。以城市交通出行系统为例,采用RGPS需求元模型为框架,构建城市交通出行系统服务层元模型。

一种比较器排序网络正确性验证方法

比较器排序网络[1](CSN)是一种执行并行排序的专用并行结构,验证一个CSN的正确性非常必要,本文基于[0,1]原理,给出一个验证排序网络的方法并用Java语言进行了实现。第1节介绍CSN及[0,1]原理,第2节介绍验证给定排序网络正确性的算法及实现,第3节总结全文。1比较器网络和[0,1]原理[1]定义1。给定n个数的序列a1,a2,..an,找出一种置换,能将该序列映射到一个非降的序列,此过程称为排序(Sorting)。

工作流模型正确性验证过程中的模型简化问题

将工作流概念映射到Petri网后得到的工作流网的合理性验证过程比较复杂,容易出现状态空间爆炸的问题,需要对工作流模型进行简化。文章将工作流模型的简化过程分为两个步骤,首先将工作流模型转化为经典Petri网,再对经典Petri网进行简化。对于自由选择网可以采用自由选择语义的规约方法进行简化,而对于非自由选择网可以结合自由选择语义的规约方法和标准的Petri网简化方法进行简化。

智能CAA中基于语法树的程序正确性验证研究

基于语法树的程序正确性验证方法是目前程序正确性验证方面全新的研究领域,该方法以程序的语法树作为程序正确性的检验对象,运用适当的树匹配算法,来验证目标程序的正确性.文章在介绍基于语法树的程序正确性验证方法的基础上,借鉴了无序标签树匹配的相关研究成果,结合软件构件的查询技术,提出了一种新的XML路径查询模型和树匹配算法,在理论和方法上对这个方法的实现进行了初步探讨,并结合XML技术提出了一套实现这一方法切实可行的解决方案.

三维几何公差标注正确性验证技术及软件实现

提出基于实体模型的三维几何公差标注正确性自动验证方法。介绍了基于几何要素自由度分析的公差标注正确性验证的原理,讨论了三维公差标注可能存在的错误及相应的验证规则。提出了基于SolidWorks软件的三维公差标注正确性验证软件的总体设计架构,研究了相关程序算法,并给出了基于三维实体模型的几何信息和公差标注信息的数据提取方法。通过设计实例零件和错误标注案例,验证了软件的设计思想和算法的正确性。

基于静态分析的XSM正确性验证

XSM(Xen Security Module)是虚拟机Xen的安全模型框架,对系统的安全性具有决定性的作用。目前,对类似的强制访问框架的正确性验证研究主要集中于对钩子函数放置的验证。现有检测方法通常路径覆盖不够完整,或者有较高的误报率。对XSM框架的正确性验证问题进行分析,提出一种过程间流敏感、过程内路径敏感的,适用于XSM框架的静态分析方法。该方法通过扩展静态分析工具Saturn,实现了对XSM框架的钩子函数设置的正确性和完备性的验证。经实验验证,该方法具有完全的路径覆盖性,并且具有较高的精确度。

基于TLA的正确性验证方法

随着面向服务的体系结构的发展,有效地组合单个分布的web服务以提供更有价值的服务成为新的热点问题。然而,在这一研究领域还存在诸多问题,比如web服务用哪种方式组合,能否实现自动组合,对组合服务进行正确性验证等等。文中主要是针对组合服务的正确性验证问题,引入时序逻辑TLA。通过把组合服务的BPEL描述转换为TLA可以理解的自动机的形式,这种方法可以很好地验证组合逻辑的正确性以及快速发现死锁等问题。

基于符号约束的PLC程序正确性验证

符号约束描述了程序中的变量关系,被广泛运用于模型检测、符号执行等程序的静态分析方法中。将符号约束应用于可编程逻辑控制器(PLC)程序的正确性验证,能够发现程序中的逻辑错误。人工计算符号约束不仅冗杂枯燥,而且错误率高。针对语句表形式的PLC程序,提出一种基于符号约束的正确性验证方法,通过分析PLC源代码的控制流及数据流,构造程序的控制流图并将其转换为静态单赋值形式的三地址码,最后使用迭代计算的方法求出每个变量的符号约束。

基于Petri网的工作流结构正确性化简验证方法

工作流技术是近年来在计算机应用领域发展最为迅速的新技术之一,但基于覆盖图的工作流网的结构正确性检查的实现过于复杂.本文在Aalst提出的基于Petri网的工作流网的控制流的正确性理论的基础上,提出了工作流网的正确性检查的化简规则及相应的化简算法,实现了对于正确结构的工作流网直接验证;对于错误结构的工作流网,输出其包含问题节点在内的子网结构,可以进一步通过覆盖图的方法确认问题节点,从而降低了工作流网正确性检查的复杂性.