基于抽象状态机的网格系统设计和分析

基于可执行规范的实现 测试同步开发模式可以将错误尽早消灭在各个开发阶段的初期 .其理论基础是抽象状态机ASM ,实现工具是支持 .NET的AsmL .本文首先介绍了基于可执行规范的实现 测试同步开发模式、ASM起源和定义 ,然后采用ASM描述了网格高层次系统语义 ,并举例说明了采用AsmL生成有限状态机分析模型语义的方法步骤 .

Chord协议的抽象状态机模型

P2P是构筑于互联网的大规模分布计算协议,采用形式化方法对P2P协议的本质原理进行分析,将有助于P2P协议的优化和改进。本文采用抽象状态机(ASM)对经典P2P协议Chord进行分析,用基于抽象状态机语言(Asml)对其建模,设计了核心运行规则,并得到了该协议的有限状态机模型。本文的工作有助于分析、优化P2P协议。

网构软件模型中的抽象状态机设计

为了更好地支持和实现网构软件的自动化,提出在网构软件模型中使用抽象状态机(ASM).在Internet的计算环境下,采用peer-to-peer(P2P)拓扑结构作为网构软件模型的支撑网络环境,使用ASM的方法从较高的抽象层次(概念层)描述整个系统的行为与状态变迁,使系统特征易于把握.分析网构软件模型中ASM的架构,详细阐述ASM的运行规则,说明了系统状态特征的变迁情况.根据ASM方法所涉及到的各种状态、事件、方法、数据、规则等进行相应的设计和实现,已经初步形成一个网构软件设计和运行的支撑平台,证明了ASM在网构软件模型中的可行性以及ASM能够实现网构软件的自动化特性.

实时嵌入式软件时间抽象状态机的扩展

针对时间抽象状态机(TASM)存在的不足,对TASM进行扩展,增加数组数据类型、while循环处理规则以及"%","&","|","^",">>"和"<<"等运算符,定义扩展后TASM的语法和语义。采用扩展后的TASM为实际的实时嵌入式软件需求建模,通过实验,验证了采用扩展后的TASM为实时嵌入式软件需求建模的有效性。

基于抽象状态机的普适服务组合分析与验证

提出了一个普适环境下服务组合的框架,使用抽象状态机对服务的行为进行不同精化层级的形式化描述,然后利用CoreASM这一模型检测工具对服务组合进行模拟执行验证,从而验证服务组合的正确性.最后给出了一个运用此方法进行服务组合验证的典型应用场景.

基于抽象状态的类的行为规格化方法

为独立方法定义严谨的规格可以保证程序的正确性。但是在面向对象的程序中,方法之间因为共享属性而相互影响,这就需要能够反映方法间影响的规格化方法。研究者们使用抽象变量、状态抽象、堆、查询等多种方法进行了尝试。文中给出一种基于抽象状态的类的行为规格方法,该方法基于抽象状态解决了类方法间的共享依赖和相互影响,同时实现了规格与实现的独立描述与运行时自动化验证。

一种连续U-树抽象状态最佳分裂点选取方法

经典连续U-树算法使用分布检验来确定抽象状态的最佳分裂点,但选取合适的置信阈值非常困难.提出一种基于最优的最佳分裂点选取方法,该方法将抽象状态的最佳分裂点选取问题转化为一个最优问题,从而规避了置信阈值大小难以确定的问题,并从理论上减少了连续U-树算法的时间复杂度.通过消解协商僵局的学习任务实验验证了它的有效性,表明了算法的性能得到增强.

Fortran内存泄漏静态检测方法研究

内存泄漏在没有垃圾回收机制的语言中是常见的问题,虽然Fortran95引入ALLOCATABLE数组解决了部分泄漏问题,但是通过指针申请内存资源仍然会造成泄漏,现有研究对Fortran内存泄漏的检测流程适配度不高且面向Fortran内存状态分析的效率和精确度上仍存在优化空间.针对这一问题,本文提出了一种面向Fortran指针引发的内存泄漏静态检测方法.首先引入指针引用控制流图(PR-CFG,Pointer Reference-Control Flow Graph)来精简程序模型,并符号化程序节点的内存状态信息,依据数据流生成路径敏感的符号化函数摘要作用于过程间分析,最终通过PR-CFG节点上由抽象内存状态计算得到的内存状态集进行故障模式状态机的状态转化来实现内存泄漏的检测.实验表明,本方法提高了Fortran指针引发内存泄漏的检测精度和效率,降低了检测的误报率.

形状分析符号执行引擎中的状态合并

符号执行技术以其良好的精确度控制和代码覆盖率被广泛应用于静态程序分析和高覆盖率测试用例自动生成。符号执行在分析程序时,以模拟真实的程序执行过程的方式分析程序的数据流和控制流信息,并检查程序可能出现的所有状态,得到程序的分析结果。高精确度和高覆盖率要求对程序状态描述具体而完备,这会导致符号执行过程中常见的状态爆炸问题。首先提出在不同的执行路径上对具体内存状态进行合并的算法,然后对内存模型进行适度的抽象,扩大状态合并算法的适用范围,最后讨论状态合并所带来的实际效果,并提出了状态合并的优化解决方案。所提出的算法在符号执行引擎ShapeChecker上实现,并取得了良好的实验结果。

抽象技术及其在蒙特卡洛树搜索中的应用研究综述

抽象技术作为人工智能研究中高效拓展决策的重要组成部分,已广泛应用于大规模的决策问题.蒙特卡洛树搜索虽然在众多决策领域取得了卓越成就,但是在现实决策问题中面临着决策空间巨大和规划周期很长的问题.鉴于此,研究抽象技术及其在蒙特卡洛树搜索中的应用,从状态空间和动作空间两个角度出发分析抽象技术如何提升蒙特卡洛树搜索的决策能力,并对抽象蒙特卡洛树搜索研究中仍需要解决的问题和未来的研究方向作进一步展望.

语义Web服务系统中互操作问题的研究

以往的互操作机制没有确切地规定业务处理任务的行为,既使业务处理难以准确地进行任务指派,又难以满足Web上异构和分布的应用程序间语义互操作的需求。为此,提出了一套有效的互操作机制,该机制用接口技术抽象化地描述与Web服务调用实例相关的服务行为,有效地解决了服务双方的通讯和协作问题;用适当的调解技术解决交互过程中的各类异构问题。为了证实该机制,给出了在线健康咨询系统应用实例,并深入探讨了该系统的工作机理和互操作实现。

基于依赖性分析的对象行为协议逆向恢复

对象行为协议对于理解对象行为语义、对象行为验证、测试以及指导其他开发者正确使用对象所提供的外部行为都有十分重要的意义。然而在很多遗产系统中,对象行为协议常常缺失或随着长期的代码维护而出现不一致。针对这一问题,本文提出了一种静态的对象行为协议逆向恢复方法。该方法首先通过源代码分析获取对象(类)内部各方法之间直接和间接的依赖关系,然后在对象(类)内部依赖关系的基础上构建行为协议状态机。由于对象(类)内部的依赖关系是对象行为约束的主要根源,而静态分析具有全面、准确的优点,因此该方法获得的行为协议具有较好的准确性,而相关的实验结果也很好地验证了这一点。

基于静态代码分析的自动化对象行为协议提取工具

对象行为协议对于理解对象接口、正确实现模块集成以及类代码的复用都有着重要的意义。在前期工作中,提出了一种基于静态源代码分析的对象行为协议自动提取方法。该方法通过源代码分析获取对象(类)内部各接口方法之间直接和间接的依赖关系,然后在对象(类)内部依赖关系的基础上构建接口的状态机图。在此基础上,进一步介绍相应的支持工具,包括主要模块、各部分的主要实现技术等。

服务网格的用户3A使用模式

用户如何方便有效地使用网格是网格界面和使用模式研究的一个关键问题,用户3A使用网格,即Anytime,Any place,and on Any device,体现了用户对网格使用的基本需求.本文给出了用户3A使用模式的形式定义,并利用ASM(Abstract State Machine)对用户和服务网格(USG)进行了形式化建模,最后证明了用户和服务网格系统在满足用户合法性s、ession连通性和服务连续性的情况下,用户可以3A使用服务网格.

基于UML扩展机制的MDA协议建模语言研究

由于UML缺少精确的形式化语义,从标准的UML记法产生一个有效的协议实现是比较困难的。为了满足协议工程的要求,通过UML的Profile扩展机制,提出了一种基于模型驱动构架的协议建模语言——交互抽象状态机描述语言IASMsDL,并说明了如何使用该语言描述通信协议,填补UML这方面的缺陷。

基于平台透明化处理的动态信息提取方法

由于没有具体的运行环境，面向嵌入式软件的逆向解析缺少有效的动态信息提取方法。针对这种情况，基于硬件平台和系统平台的透明化处理，设计了基于QEMU中间代码扩展的插桩，定义了基于中间代码层的多粒度插桩接口及回调函数，实现了平台无关的多粒度抽象状态提取和系统无关的内存数据读取，并通过系统语义自省机制实现了系统语义视图的提取。测试结果表明，基本块级和函数级提取信息的速度比语句级快10～20倍，占用的空间少10—30倍。本方法在时间性能方面与DECAF等类似系统相比具有明显优势，能够有效提高面向嵌入式软件逆向分析工作的效率。

一种网构软件体系结构中的纵横验证机制

如何在开放、动态、复杂的Internet环境下开发网构软件是软件技术领域一个挑战性课题。从网构软件整个生命周期入手,对网构软件的形式化模型,在简单介绍抽象状态机(ASM)的基础理论之后,刻画了网构软件的构件模型,并对构件模型进行了基于ASM的形式化描述,在此基础上,将粗粒度抽象构件的精化问题转换为求解构件组合方案的问题,并在体系结构元层,提出一种双向验证方法对不同抽象程度的组合方案进行横向和纵向的验证,以保证目标系统的正确性和求精过程的正确性。以上形式化建模和双向验证方法尽可能地避免和消除了软件设计早期的错误。通过系统实验验证可以看出,该方法对网构软件的开发具有一定指导意义。

安全攸关软件系统建模与验证专题前言

随着计算机技术应用的日益普及和不断深入，软件系统的规模和复杂性急剧增大，软件在越来越多的系统中成为主要的使能部件．在航空航天、武器装备、医疗设备、交通、核能、金融等安全攸关的应用领域，软件系统失效将导致灾难性的后果，保障软件系统的质量成为迫切的需求和挑战．建模、分析与验证是保障软件系统质量的重要环节和手段．本专题收录的14篇论文反映了近年来我国学者在安全攸关软件系统建模与验证领域的部分研究成果．《基于形式化方法的航空电子系统检测》基于形式化方法研究面向航空电子系统的检测方法，建立了航空电子系统的形式化模型，并在此基础上提出了从静态和动态两方面对航空电子系统进行检测的途径．《基于时间抽象状态机的AADL模型验证》提出了一种基于时间抽象状态机的AADL形式转换语义，并在此基础上给出了一种AADL模型的验证方法．

SDL-2000的形式语义研究

介绍了 SDL - 2 0 0 0形式语义的理论基础抽象状态机 (ASM) ,深入分析了 SDL - 2 0 0 0形式语义 ,其中静态语义使用一阶谓词演算定义 ,动态语义使用多代理的分布式

基于ASM的混合式情境感知共享机制研究

移动的用户能够方便地访问分布在普适计算环境中的传感器,进而获得情境信息,是情境感知系统的核心目标。本文提出了一种融合分布式P2P和Publish/Subscribe模式的混合式情境感知共享机制,基于抽象状态机对该机制的高鲁棒和可扩展的特性进行设计和规约,并采用AsmL测试工具生成有限状态机验证该机制的有效性和合理性,表明该机制可满足动态的分布式情境感知系统要求。