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

　　目前，T-CBESD 的设计开发和运行环境是：Windows XP 操作系统平台，Eclipse SDK3.4.0，Java SDK 1.6，所引用的MDL 文件是由Rational Rose 2003 生成。本节中分别给出T-CBESD 的非实时功能性质验证和实时功能验证两方面的实例应用说明。
　　在T-CBESD 中所构造的构件Communication 和User 的合法组合状态空间（去除了非法状态集）包括6 个组合状态：（s0|s0），（s1|s1），（s2|s1），（s3|s1），（s4|s1），（s5|s1）。对于存在一致性验证，不妨设顺序图中抽取的一个消息交互序列send*nack*send*ack 作为验证规约，显然，直观上就能判断Communication 和User 的组合系统应该是满足这个规约的。
　　运行T-CBESD 进行验证的结果，显示组合系统确实满足存在一致性，其相应的系统执行路径为：s0|s0??s1|s1??s2|s1??s3|s1??s4|s1??s5|s1。对于前向一致性验证，就本例而言，不妨设D1 消息序列为send*nack，D2 消息序列为send*ack，然后将其作为工具的系统规约来输入，其验证结果应该仍然是满足。运行T-CBESD 的验证结果，显示的确存在一条系统执行路径满足前向一致性。事实上，所找到这条路径与存在一致性的路径是相同的。
　　对于逆向存在一致性，若设D1 消息序列是send，D2 消息序列是ack，T-CBESD 给出的结果是不存在这样的一条组合系统路径满足它。这也符合对本例的直观判断，即在接受到ack之后又执行send 动作是不合法的，因此这个存在一致性是不满足的。对于双向一致性，若给出的D1 消息序列是send，D2 消息序列是send，D3 消息序列是nack，验证的结果是搜索成功，得到的可满足的组合系统执行路径为：s0|s0??s1|s1??s2|s1??s3|s1??s4|s1。图13 所示为T-CBESD 的非实时功能验证模块插件的界面。界面左边部分为操作区，主要提供组合、查看、工具输入、验证类型等功能选择，界面右边部分为分析与验证过程中工具所反馈的数据信息。

（转载自中国科教评价网http://www.nseac.com）
　　5. 相关研究工作

　　SPIN是一个经典的分布式系统模型检验工具。系统每一个构件的自动机模型使用SPIN 中Promela 语言所构造的进程（Process）来表达，组合系统的状态空间通过计算所有自动机异步积来得到，系统规约使用LTL 时序公式描述；系统是否满足规约性质则通过组合系统和时序公式相对应的Buchi 自动机进行同步积，然后检验其结果是否为空。目前SPIN在工业界硬件设计以及通信协议规约的验证领域得到了较广泛的应用，但对同时具有功能和非功能需求的嵌入式软件验证领域，SPIN 并未提供相应的支持。UPPAAL是一个基于时间自动机理论的实时系统仿真和验证工具。其基本思想为将实时系统的行为建模为一个实时自动机网络，并进行了数据类型的扩展，采用时间μ-算子作为系统的规约语言，主要对系统进行安全性和活性等性质的检验。UPPAAL 具有良好的图形化编辑和模拟功能。
　　目前，已有一些工具以UPPAAL 为核心作进一步扩展，如：TIMES是以时间自动机模型验证为基础的一个工具集环境，可以进行建模、可调度分析、系统合成以及特定平台上的代码生成；Save-IDE则是基于构件模型SaveCCM[20]所建立的一个支持构件化嵌入式系统开发的工具集，等等。此外，与接口自动机相关的工具包括：Chic是第一个基于接口自动机理论的原型工具。它是作为Jbuilder 集成环境下的一个插件模块来设计开发的，其目的只是用于对相关理论工作的一个初步验证，现在已经被另一个工具Ticc所替代。
　　Ticc 的理论基础是接口自动机的一个扩展版本：Sociable Interface，其基本思想仍然是检验构件接口组合中是否兼容。Ptolemy II中也实现了基本接口自动机模型的组合兼容性分析工作，不过Ptolemy II 是一个包含了多种不同工具集的混成系统建模、分析、合成和代码生成的开发环境。此外，以法国INRIA 为中心的欧洲多个研究机构正在构建的OpenEmbeDD是一个以Eclipse 为开放平台的模型驱动嵌入式系统开发工具集。这是一个庞大的开源工具组合环境，提供嵌入式系统设计（包括软件和硬件）、模拟、验证、合成以及测试等各个阶段的开发支持。