分布式嵌入系统中的交互一致性

在安全攸关的控制系统中通信或计算机出错的情况下,所有无错的部件必须保证传送的数据是一致的。为解决这一问题,需要专门的算法。本文介绍了总线通信时的签名消息算法,以分布式冗余刹车控制系统为例,讨论了算法的实现,并讨论了CAN在签名消息算法中应用的可能性。

构件演化的交互行为一致性研究

构件演化前后的交互行为执行序列不一致,会导致系统行为偏离系统的功能目标。针对该问题,基于进程代数描述构件间的交互行为,归纳交互行为一致性的定义,给出交互行为一致性所需满足的约束条件,提出一种保证交互行为一致性的方法。实例分析结果证明了该方法的可行性和正确性。

面向基于场景规约的Web服务消息流分析与验证

采用UML顺序图构成基于场景的规约、WS-BPEL作为Web服务的描述语言,提出了一种面向基于场景规约对Web服务消息流进行分析与验证的方法:首先,对WS-BPEL消息流进行分析并将其自动抽象为基于Petri网的模型;同时,为了缩小状态空间、提高验证效率,在不影响消息交互顺序的前提下,对WS-BPEL源码和基于Petri网的模型分别进行化简,即面向基于场景规约将与验证无关的活动和元素删除;最后,通过遍历基于Petri网的模型以验证WS-BPEL消息流与基于场景的规约之间的一致性(消息交互顺序的存在/强制一致性).文中通过一个贯穿整个分析与验证过程的实例加以说明.该方法已经实现成为一个原型工具.

Timed RAISE方法在列控系统等级转换场景中的应用研究

高速铁路列车运行控制系统是一个复杂的实时性系统,结合其实际特点,将域方法作为系统描述的切入。通过对模型检验和定理证明两种验证方法的分析比较,提出使用基于定理证明的时间化工业软件工程的严格方法Timed RAISE形式化方法对等级转换(CTCS-2级至CTCS-3级)场景进行描述,并对其场景交互一致性和实时性进行验证,结果表明该场景不会出现场景交互一致性错误,也不会违反时间的约束。