初探一种构件化嵌入式软件设计模型验证工具(5)

T-CBESD 的特点在于：首先，可以直接使用UML 的顺序图模型作为系统规约输入进行验证，而不需要系统设计人员去重新学习时序逻辑语言来构造规约说明；避免了在大多数相关工作中需要在不同的形式模型之间进行复杂转换，通常这些转换是需要相当的空间和时间消耗。其次，相比较上述基于接口自动机模型的研究，本文的工作在接口自动机组合兼容性的基础上对构件式嵌入式软件系统设计模型与场景式规约模型之间的一致性问题给出了一个更为完整的验证框架；可以进一步进行各类一致性问题的分析和验证；第三，通过扩展时间区间所得到的实时接口自动机的描述能力本质上与时间自动机的描述能力是等价的，并且通过在顺序图模型中使用时间不等式约束，使得所定义的实时接口自动机网络与带时间约束的顺序图之间的一致性问题更具有一般性。最后，Eclipse 开放平台给工具提供了良好的开发、维护和使用环境。

　　6. 结束语及未来工作

　　本文在 Eclipse 开放平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计分析与验证的原型工具T-CBESD。该工具的目的是应用于构件化嵌入式软件开发的设计建模阶段，对系统重要功能性质以及与时间相关的实时行为性质进行严格形式化分析和验证，使得设计者可以尽早在系统开发前期发现错误并予以修改，以降低成本并提高系统可靠性的可信度。论文主要内容包括：非实时功能验证以及实时功能验证的理论基础；T-CBESD 的基本设计思想；工具的输入输出接口、状态空间数据结构、验证算法等的设计与实现；以及应用实例分析。
　　进一步的工作包括以下几个方面：
　　扩展工具的输入和输出接口形式。输入方面，目前T-CBESD 中自动机模型的XML 文件是需要用户手动生成，我们希望也可以使用Rational Rose 等图形化建模环境作为前端工具来方便用户进行系统接口自动机模型的设计。但是接口自动机与UML 状态机的语法和语义都存在不同之处，需要重新设计一个中间转换过程来处理。同时，考虑在顺序图形式化定义的基础上进一步对UML 交互概观图进行形式化描述，并将其作为工具的另一种扩展形式的输入模型。输出方面，将设计更为完整的验证结果信息XML 文件格式，并考虑与软件测试技术相结合，利用验证结果给出的系统出错（验证失败）行为轨迹来指导生成相应的测试用例。
　　在工具的核心算法部分，将进一步设计并实现包括资源接口自动机和能耗接口自动机在内的分析与验证算法，以扩展T-CBESD 的功能。同时，考虑到在实时接口自动机组合过程中可能出现的状态空间爆炸问题，将对实时验证算法作进一步改进，设计新的On-the-Fly 验证算法实现，即：在构造一个新状态的时候就对当前路径进行即时验证。
　　应用复杂的多构件系统设计实例，来对工具的性能进行检验和提高。目前所运行的实例相对比较简单，主要目的是为了检查实现算法的正确性，还需要在复杂多构件系统模型情形下对算法性能作进一步检验和改进。现在我们正在对某无人机飞行控制软件系统进行模型分析和抽取工作，准备将其作为T-CBESD 的一个复杂实例验证。
　　进一步完善原型工具的操作界面；目前本文的工作主要关注于基本的输入输出处理和核心算法的设计与实现，还需要考虑工具用户界面接口设计的实用性和有效性。