其一，现在工业界已存在较为成熟的图形化建模工具，可以快速方便的绘制UML 模型图，可以利用这些工具作为T-CBESD 的前端，而不用在T-CBESD 中重新设计复杂的用户接口来支持图形化建模设计。
其二，在2.2 节中提到，一个顺序图场景可能会包含多个不同的消息事件序列；显然，如果让系统设计与分析人员从每一个顺序图中手动的生成所有可能的消息事件序列，这并不是件容易的事情。因此，需要提供一种从顺序图模型自动化生成所有可能的消息事件集合的方法。
在Rational Rose 中所生成的顺序图模型文件是MDL 格式，需要先转换成XML 格式文件，然后进行相应消息序列的抽取。其处理过程如图5 中所示，首先通过在Rational Rose中加载XMI 插件将MDL 格式的文件转换为XML 格式；然后对XML 文件进行解析，建立文档解析树，提取消息事件节点，并根据顺序图中的事件发生先后顺序构造一个相应的有向无环图（在此，定义了顺序图的参加者类（Element Class）、消息类（Message Class）以及结点类（Node Class）用于图的构造）；最后设计了一个拓扑排序算法，对该有向图中的消息事件节点进行拓扑排序，从而得到一个顺序图中所有可能的消息事件序列的集合。
3.3 自动机组合模型的建立
接口自动机的组合过程与一般自动机组合的语义存在不同之处。在两个接口自动机组合的状态空间中，有可能存在两个构件接口之间交互不同步的所谓“非法状态”，在应用验证算法之前必须将这些非法状态找出来并从状态空间中去除掉。文献中给出了一个识别非法状态集合的基于不动点（Fixpoint）的抽象算法框架，基本思想是先构造出所有可能的组合状态的空间图，然后逆向搜索非法状态集。在T-CBESD 的实现中我们则采用正向的合法状态集合构造方法，其好处是避免了需要首先生成所有的状态空间。给出了工具中基本自动机模型的组合算法流程图。此外，在实时接口自动机组合的过程中还需要进一步考虑时间约束；如在2.1 节中形式化定义表示一样，所得到的每一个组合状态都会有一个相应的时间标记值。
3.4 非实时功能性质验证算法的实现
在3.3 节中建立的自动机组合状态空间的基础上，就可以应用文献中的一致性验证算法等对3.2 节中所给出系统需求中的消息交互序列进行分析验证。T-CBESD 中实现了包括存在一致性、前向一致性、逆向一致性以及双向一致性在内的多种形式的非实时功能行为验证算法。给出了工具中非实时功能性质验证模块的类图框架。主要包括两大部分：一部分是自动机模型核心类，包括Automata Class，Transition Class，State Class 以及组合模型的 Composition Class ； 另一部分则是与验证算法相关的类， 包括：ExistConsistencyChecking Class ， ActionString Class ， AdjacentMatrix Class 和辅助类TransitionNode Class。其中，存在一致性验证类（ExistConsistencyChecking Class）作为功能验证算法类的基类，其他形式的一致性验证算法类（如：BackwardConsistencyCheckingClass，ForwardConsistencyChecking Class 和 BiConsistencyChecking Class 等）都依赖存在一致性验证类，调用其方法实现所需的功能。
在基类ExistConsistencyChecking 的实现过程中，一个关键的问题是：当在系统组合状态空间图中搜索与UML 顺序图交互序列所对应的投影路径时，有可能出现一个满足条件的投影路径一部分出现在某个环路内部，而另一部分却出现在此环路的外部路径上的情形[11,12]。如果只是采用经典的深度优先遍历或广度优先遍历方法对组合状态空间图进行搜索判定，将会遗漏掉这种情况。为此，在T-CBESD 中设计了动作名表（ActionString Class）和邻接矩阵（AdjacentMatrix Class）。其中，动作名表是以接口自动机的动作名作为表头向量，并以执行该动作名的转换作为表结点的一张哈希表，其定义见图8 所示（注：未包含类方法说明）。
基本思想为：对于所给出的一个消息交互序列，先根据消息名从动作名表中依次取出与消息名所对应的表头结点以及表结点，构成一张与消息序列中消息次序对应的消息名表。
然后遍历这张消息名表来搜索投影路径，搜索过程中需要根据邻接矩阵来判断两个结点之间是否可达。
3.5 实时功能性质验证算法的实现
在实时功能性质验证算法的实现中，考虑到实时一致性验证抽象算法框架实际上包含了两次对组合系统状态空间图的搜索过程；也就是说在非实时功能一致性验证中只需找到一条满足条件的投影路径，而在实时功能一致性验证中，是需要先根据消息序列找出所有可能的投影路径，然后进行检验。因此，T-CBESD 中依据动作名表以及邻接矩阵对图进行穷举搜索，搜索到一条投影路径之后并不立即结束，而是继续找下一条投影路径，找出所有与给定路径相符合的投影路径。在此基础上根据所给出的时间布尔表达式对这些投影路径进行筛选，如果找到符合时间布尔表达的投影路径验证则验证成功，否则，验证失败。
4. 实例应用