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

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

基于消息顺序图和Petri网的移动应用监测平台建模分析

随着移动互联网的迅猛发展,移动应用的数量呈现井喷式的爆发,对其性能、故障和短板进行实时、有效的监测与分析是保证系统正常运行的关键。统一建模语言(Unified Modeling Language,UML)作为一种功能较强的面向对象的图形建模工具,可以对移动应用监测平台进行建模分析,但在其过程描述中缺乏严格的语义。Petri网作为一种离散事件动态系统的建模和分析方法,提供了在逻辑时序下研究系统特性和性能的有效手段,并具有图形方法的直观性和逻辑方法的概括性。通过将基于UML消息顺序图和Petri网的建模方法应用到移动应用监测平台的分析过程中,针对用户下发的监测任务构建系统的消息顺序图和Petri网模型,利用消息顺序图对平台各对象之间在时间顺序上的交互关系进行了验证,并利用Petri网化简规则和状态方程对该模型进行了结构上的正确性验证和可达性分析。

CTCS-N等级转换场景形式化建模与验证

新型列车控制系统的车载设备承担更多地面设备的功能,其功能测试主要是以现场测试为主,费时费力,构建满足系统功能与性能需求的模型有助于保证列车在线路上安全、高效地运行,因此针对新型列控系统提出一种基于时间自动机的形式化建模与验证的方法。首先,选取等级转换场景为主要建模场景,提取规范中的功能与性能需求,梳理信息交互图,基于UPPAAL建立车载设备、应答器、临时限速服务器、无线闭塞中心的时间自动机模型;然后,使用模拟器进行模型的仿真,生成对应的消息顺序图;最后,以自动机语言为基础,验证正常模式和故障模式下车载设备转换是否满足要求。验证结果表明:所建立的模型满足等级转换场景的需求,其功能符合对应的技术规范,证明了该形式化建模的可行性,为新型列控系统测试、其他场景或功能的建模与验证提供了参考。

形式化语言MSC消息机制的扩展

为了使消息顺序图(messagesequencecharts,MSC)能更好地满足在通信领域应用的需要,在现有MSC标准的基础上,参考了其他常用的顺序图,并采用面向对象的思想,对MSC的消息机制进行扩展.MSC是用于描述系统间消息传递的一种有效的形式化语言,但现在的MSC存在着数据表达能力不强,消息顺序机制不够灵活等问题.因此,在对消息的扩展中,将消息作为一种对象进行研究,增加了消息本身的信息量.在此基础上对消息的顺序机制进行扩展,通过引入一些新的概念、符号,介绍了如何表达消息之间的相互关系和消息的运算等.扩展后的MSC能更加直观、清楚、完整地描述消息的轨迹和系统的静态与动态特性.

基于角色的工作流研究

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

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

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

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

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

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

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

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

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

动态可配置网络爬虫系统的形式化研究

为了在动态可配置网络爬虫系统开发的初期发现问题,对其进行形式化研究是十分必要的。本文通过SDL对爬虫系统进行形式化建模,并使用仿真的MSC运行结果来对爬虫系统可能出错的情况、可达性以及一致性等性质进行了分析。使用Telelogic TAU的仿真结果表明,自顶而下的形式化研究角度可以保障动态可配置网络爬虫系统的完备性。

LTE系统HARQ机制的研究与设计

长期演进(TD-LTE)系统HARQ过程是移动通信系统中终端(UE)与基站进行数据传输的一个非常重要的过程。针对LTE协议采用HARQ作为其关键技术之一,提出了新数据指示值(NDI)在HARQ技术中的应用方法。着重介绍了不同DCI格式中的NDI分别在上行重传和下行重传中所起到的作用和功能。通过说明和描述语言(SDL)和树表结合表示法(TTCN)协仿真,生成HARQ过程的消息顺序图(MSC),NDI在HARQ技术中的正确性得到验证,在TD-LTE射频一致性测试仪表的开发中,该设计方法得到应用。