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

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

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

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

Chord协议的抽象状态机模型

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

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

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

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

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

运用ASM描述安全协议

介绍了抽象状态机（ASM）,建立了基于这种形式化方法的协议描述于验证的环境,并建立了一般意义上的入侵者模型.作为应用实例,给出了 Helsinki协议的 ASM规约,说明利用这个规约可以直观的演绎 Horng-Hsu攻击.

抽象精化和可满足性结合的EFSM模型测试用例优化生成

基于模型的测试是测试自动化的重要手段,通常采用模型检验技术从系统模型自动生成测试用例集,但生成的测试用例集往往存在冗余,这将影响测试用例执行的性能和成本.该文以扩展有限状态机(Extended Finite Machine,EFSM)为建模工具,根据公式簇建立状态等价关系,构建抽象模型,采用模型检验技术生成抽象反例(测试用例);给出了判定生成的抽象反例是否为伪反例的方法;采用反例引导的方法精化抽象模型,删除伪反例;最后,使用我们之前提出的基于可满足性的测试用例生成方法在抽象模型上生成约简的测试用例集.实验表明:该方法的测试用例数目约简比例最高达76%(警报侦测组件EFSM),总长度约简比例最高达68%(ATM EFSM),同时不会影响测试用例集的迁移覆盖率和查错能力.

Verilog语义的ASM表示方法研究

使用抽象状态机模型(ASM)对Verilog的语义进行研究,给出各类赋值语句和延迟/事件控制结构的形式定义。以此为基础与VHDL进行对比,说明各种赋值语句和延迟/事件控制结构向VHDL的转换方法以及二者在转换前后的差异。

基于ASM描述共享网络的实时任务可执行概率设计

利用抽象状态机(ASM),形式化描述了共享网络中实时任务接纳控制机制,提出了实时任务可执行概率设计过程的ASM模型,利用Spec Explorer给出了分析该模型的方法步骤。该模型不仅有助于验证其设计,还有利于实现实时任务接纳控制机制,并为利用ASM模型方法设计实现其他控制机制提供了范例。

基于ASM模型的协议一致性测试研究

针对协议测试中,状态机描述、测试集成环境和被测实现彼此独立带来的问题,提出了在可视化编程环境下利用抽象状态机模型和桩函数结合实现协议一致性测试方法。在分析抽象状态机测试理论的基础上,给出基于抽象状态机和remoting技术的协议分布式测试模型。以抽象状态机语言描述简单文件传输协议为例,采用分布式测试模型,实现了被测协议的远程一致性测试。

用基本ASM定义SDL动态语义

提出了用基本 ASM(Abstract State Machine)定义 SDL(Specisification and Descripiton Language)动态语义的方法框架。由于 SDL的复杂性 ,重点介绍了用 ASM模拟 SDL状态机交替工作方式 ,创建 agent和procedure实例以及复合状态应用。该方法简化了当前用分布式 ASM定义的

基于ASM的元模型形式化语义的研究

提出一种在模型驱动开发过程中的形式化语义描述方法。该方法利用元建模技术,形式化地描述了元模型及其语义间的映射关系,以提供精确的语义描述,从而为模型驱动开发提供有力的支持。将描述框架用于模型转换规则的定义以及元模型的分析与验证,并以简单Petri网为例,说明该方法可以有效地支持模型转换和代码生成。

一种用基本ASM定义SDL静态语义的方法

提出直接用基本AbstractStateMachine定义SpecificationandDescriptionLanguage静态语义的形式方法,其主要特点是:语法域中的元素统一解释为语法值;转换规则定义为ASM规则;映射规则定义为一系列称为t-函数的映射函数形式.

面向参数化系统验证的自动抽象方法

针对参数化系统验证面临的状态空间爆炸问题,提出自动抽象方法化简参数化系统状态空间.首先进行Y-抽象建立单进程有限状态机模型,然后通过对多个Y-抽象模型的合成运算得到异步合成的参数化系统,最后根据定义的谓词对参数化系统进行X-抽象得到二维抽象模型.运用该方法,对基于Synapse N+1,Illinois,MESI,MOESI,Berkeley,Firefly和Dragon的7个参数化协议和注入错误的MESI协议进行自动化抽象建模,并验证了相关性质,有效地提升了验证参数化系统的能力、缩短了验证时间;应用文中方法验证FT-1000CPU的一致性协议的结果表明,该方法在降低验证复杂度方面具有明显优势.

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

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

语义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这方面的缺陷。

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

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

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

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