基于SPIN的HMSC模型自动检验方法

自动检测与验证HMSC(high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义,为此提出一种为HMSC模型进行自动检验的方法,并将其实现。利用转换规则为HMSC模型生成Promela检测语言,借助SPIN工具对需求进行验证。该方法不仅支持模型检测,同时通过对系统行为的动态模拟可以实现需求的合理性分析。从Promela实现到SPIN验证整个过程实现自动化操作。在该方法的基础上实现一个文本需求自动建模及检测分析的工具,通过一个实例展示其自动建模检测分析的效果,表明了其有效性和实用性。

基于MSC测试目的的协议互操作性测试生成

提出了一种基于MSC(消息序列图)测试目的的互操作性测试生成方法.采用通信多端口有限状态机作为被测系统的描述模型,MSC作为互操作性测试目的的描述模型,使用全局状态跟踪和逆向查找等技术从系统规范中生成包含该测试目的的测试序列.该方法由于只需遍历系统的部分状态空间,因此在一定程度上减少了发生状态爆炸问题的可能.在移动IPv6协议系统中的应用表明,该方法具备一定的可行性.

基于MSC的网络游戏软件测试方法研究

针对网络游戏软件测试方法研究方面的不足,结合基于模型测试方法和TTCN测试技术,对网络游戏软件可玩性的测试方法进行研究。采用MSC图作为网络游戏玩法建模工具,建立玩法测试模型;用TTCN-3核心语言对玩法测试模型加以实现;结合一个具体的网络游戏软件测试案例,给出上述测试方法和技术的解释。从理论角度验证了基于模型测试方法在网络游戏软件测试上的可行性;从技术角度表明了TTCN对网络游戏软件测试的有效性。

MSC时间表示方法与UML序列图结合建模

介绍了系统建模中的时间相关概念,以及MSC和UML序列图对时间相关概念的表示.将MSC对时间强大的表示能力和准确的表达方法应用于UML序列图,对时间进行建模,提高了UML序列图的时间建模能力,进一步满足了实际系统,尤其是实时系统建模的要求.

场景驱动的构件行为抽取

如果构件含有冗余的功能,特别是含有用户不想要的功能,则无法被用户正确使用.因此,如何从构件中提取场景规约中所描述的用户想要的行为便是一个亟待解决的问题.给出了解决该问题的一种方法.该方法通过为构件构造一个环境,即极大包含环境,使得场景规约中所描述的所有行为可以从构件中抽取出来,并保留到该构件与其极大包含环境的组合中.同时,构件中的其他行为,即不在场景规约中的行为,被尽可能地舍弃.用接口自动机为构件的行为建模,并将用消息序列图描述的场景规约抽象为一组活动序列.构件的组合描述为接口自动机的乘积.给出了基于场景进行构件行为抽取的相关算法,并用一个实例对文中所述方法进行了说明.

基于角色的工作流研究

工作流管理系统是集成企业的信息、参与者和资源,实现过程自动化的CSCW系统。面对变化的经营环境,企业的业务过程呈现动态、不确定的特点。工作流管理系统能否有效处理这种动态性直接影响了其应用效果。传统工作流的定义以活动为组成要素,不易表达参与者的交互和动态行为。本文讨论了基于角色的动态工作流,给出了一种消息顺序图和ECA规则的复合表示方法。

一种新的Petri网模型建立方法

提出了一种通过消息序列表MSC来对现实系统进行Petri网建模的简便有效的方法。即利用了MSC简单、直观的优点,又能够充分利用Petri网相关的分析和仿真的理论与工具。给出了具体的由MSC到Petri网的转换算法。依照转换算法可将复杂系统的MSC模型转换为Petri网模型。经过对具体模型实例的分析可以得出,由这种方法得到的Petri网是安全可行的。

CTCS-3级列控系统临时限速服务器建模与形式化验证

临时限速服务器是CTCS-3级列控系统的重要组成部分,其系统安全性直接影响到高速铁路的运营安全。在TSRS系统研发过程中需对系统进行仿真建模和验证,发现系统设计错误,以保证系统的安全性。分析CTCS-3级列控系统临时限速服务器的组成结构,提取系统功能和性能规范约束,利用消息顺序图对TSRS与外部系统之间的信息交互行为建模,并将系统MSC模型转化为UPPAAL中的时间自动机仿真模型,对系统的功能和性能要求进行形式化验证。验证结果确认了系统的安全性和受限活性,为进一步完善TSRS设计和系统开发提供参考。

联邦接口规范测试方法研究

高层体系结构(HLA: High Level Architecture)可以支持各种类型仿真之间的互操作,同时便于建模与仿真部件的可重用。开发HLA应用必须根据联邦开发与执行过程模型进行,其中联邦测试是FEDEP模型的重要组成部分,主要包括三级测试,即:一致性测试,集成测试,联邦测试。一致性测试主要包括接口规范测试,OMT测试,RTI测试等内容,本文对联邦接口规范测试的方法进行了研究,根据接口规范的测试标准,制定了测试顺序,给出了联邦接口规范的测试顺序模型,使接口规范测试更加系统、清晰。

LTE终端小区选择方案设计及实现

从LTE终端小区选择的高层协议入手,从适合小区和可接受小区驻留条件出发,分析了小区选择正常过程,并对条件不满足的后续小区选择深入研究,设计了解决方案,给出了相应的设计流程,并利用SDL(规范说明与描述语言)和TTCN(树表结合表示法)协议仿真,产生MSC(消息顺序图)。仿真结果表明,该方案有效地完成了协议所要求的小区选择功能。

基于消息顺序图和Petri网的供应链工作流模型设计

根据跨组织工作流的设计思想,在对供应链业务流程进行分析的基础上,提出了一个基于消息顺序图和Petri网的供应链工作流模型设计方案,从而在供应链中建立一个既保证成员的充分合作又使其发挥自主性、集成的业务流程体系,达到提高整个供应链竞争力的目的。最后,以一个实例对该模型进行了分析论证。

分层有色Petri网在物流配送系统仿真建模中的应用

研究了如何使用分层有色Petri网在减少模型复杂性的基础上来建立物流配送模型,并使用Colored Petri Net工具中的monitor机制,对关键库所中托肯的变化情况以及关键变迁的发生次数得到Simulation Performance Report和Message Sequence Chart来对模型进行全方位的定量定性分析,准确模拟了实际系统完成物流配送的整个过程,仿真过程表明该系统具有良好的适应性.在确保物流配送流程合理性的同时,也为物流仿真软件体系结构的模块化及层次化设计建立了良好的基础.

基于场景规约的系统行为建模

提出一种基于场景规约的系统行为建模方法。采用消息序列图描述场景,把场景规约中构件实例之间消息传递的事件序列作为一种显式的场景提取物并给出语义表示,通过场景正样本构造前缀树接受器。此前缀树接受器是一个能接受正样本的最大确定有限自动机,通过合并状态得到商自动机,给出一个状态合并算法。该算法支持交互式增量的场景产生。

面向对象的机电系统结构及行为建模

针对原理设计阶段机电一体化系统的逻辑结构模型、逻辑/物理行为模型和原理方案表达,提出了基于参考模型的机电一体化系统初步逻辑结构,以及基于统一建模语言(UML)类图的详细逻辑结构(即原理方案表达);提出了基于消息序列图(MSC)的交互行为建模及基于规范和描述语言(SDL)的逻辑/物理行为建模方法,从而基于人类认知客观世界的思维方式提出了面向对象的机电系统设计和分析的新视角。基于此对CD播放机工作系统中关键组件的原理方案解进行了表达,研究结果显示了面向对象系统建模方法的有效性。

基于时间自动机的C3+ATO系统场景建模与验证

C3+ATO系统目前在我国处于试验发展阶段且具有自动化等级高、安全标准高等特点。为验证具体场景下高速铁路C3+ATO系统功能是否符合对应技术规范,提出一种基于时间自动机的形式化建模与验证方法。选取车站自动发车场景作为建模对象,提取C3+ATO系统规范中的功能需求,建立场景的时间自动机模型,生成对应流程的消息顺序图并对系统功能属性进行验证,在C3+ATO列控仿真平台仿真验证。仿真验证结果证明:模型满足C3 (10)ATO系统的安全功能属性和受限活性需求,为后续系统设计开发、实际应用及相关规范完善提供理论参考。

基于CPN的求解关键路径的新方法

在证明转换规则正确性的基础上,首先利用转换规则对AOE网进行转换,然后从两个方面对转换后的CPN(Colored Petri Nets)模型不合理的地方进行合理性的修改.再利用编写的函数求出从源点到汇点的所有的可达路径,在获得所有可达路径的同时也获取了所有可达路径所花费的时间,那么时间最大的就是关键路径.该方法不仅简便直观,而且能够在保证正确性合理性的前提下提高执行效率,减小时间复杂度.

虚拟制造企业的Petri网建模／仿真

为降低Petri网建模难度并增强模型的可读性,提出一种通过消息序列表(Message Sequence Chart,MSC)模型对虚拟制造(Virtual Manufacturing,VM)企业的生产经营过程进行Petri网建模的新方法．建立冲突消解机制,给出从MSC模型到Petri网模型的转换算法,在不改变Petri模型活性、安全性和有界性等特性的基础上对其进一步优化,并对Petri网模型进行分析与评估．

基于消息序列图的协议交互过程构建方法

为了有效掌握协议的交互行为,提出一种基于消息序列图的协议交互过程自动构建方法。首先,根据协议交互过程的特点,定义依赖关系图来表示消息序列中事件的偏序关系,将网络流转换为依赖关系图;然后,使用基本消息序列描述协议的交互行为片段,通过定义事件最大后缀来挖掘基本消息序列;最后,搜索出最大依赖关系图并将其连接合并,构建出消息序列图。实验结果表明,该方法具有较高的准确性,构建出的消息序列图可以直观地表示协议的交互过程。

消息序列图模式抽取与组合

在抽象原子模式的基础上,提出了一种基于图连通性判定的模式抽取方法,并给出了其正确性证明。接着,详尽分析和给出了模式组合定理的一个构造性证明以及模式组合前后的消息序列图的行为等价性证明。基于该模式抽取与组合方法,可以在更高层面重新组合模式。通过实验验证了该方法的有效性。