评价网 > 科教论文 > 工学毕业论文 > 电子信息工程论文 > 正文

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

2013-07-03 01:06
　　在基于场景的系统规约中，通常将一个系统相对独立的功能模块建模为一个场景描述。这个场景表达了参与其中的各构件之间如何进行交互。进一步的，在系统设计阶段，还会关心有多个简单场景组合起来的复杂场景需求，即需要考虑多个简单场景之间的逻辑关系。
　　交互概观图（Interaction Overview Diagrams）是在UML2 规范中引入的一种用以描述系统中复杂交互场景的动态行为模型。交互概观图本质上是将活动图模型与顺序图模型结合在一起，图中的每一个节点都可以视为一个用顺序图表达的简单交互场景，然后利用活动图所提供的顺序、迭代、并发、选择等操作将多个不同的顺序图场景联系在一起；这样就可以用来表达语义更为丰富的系统交互行为。在本文中所关心的以下几种场景组合一致性问题都可以用交互概观图来有效的描述：
　　1. 存在一致性： 某个特定的场景D 是否在系统所有行为中至少出现一次，或者某个指定的场景D 是否在系统的所有行为中一定不会出现。
　　2. 前向强制一致性：当某个条件场景D1 出现时，则场景D2 一定会随之在系统后续行为中发生。
　　3. 逆向强制一致性： 当某个条件场景D1 出现时，则场景D2 一定在D1 之前就在系统的行为中发生。
　　4. 双向强制一致性： 当两个条件场景D1、D2 在系统一个行为中先后出现时，则在这两个场景之间一定有D3 发生。

　　2.3 模型分析与验证算法
　　基于以上给出的接口自动机系统组合行为模型以及交互场景系统规约模型，可以对2.2节中提出的多个基于功能的一致性验证问题进行分析与验证；同时，考虑嵌入式软件设计中的实时需求，以上每个基于功能的一致性验证问题都存在一个相应的带时间约束的版本；即在完成功能性验证的同时，也必须同时满足交互场景中给定的时间约束。在相关研究工作中，对上述几类模型验证问题进行了形式化定义和分析，并分别设计了相应的验证算法。算法的基本思想是对带有不同语义信息的系统组合行为的状态空间进行搜索，将每一个可能的系统行为与基于场景的交互规约进行比较，来判断设计模型是否满足各种系统规约。例如：对于存在一致性验证问题，如果在组合状态空间中顺序图D 所描述场景中的消息事件序列至少出现一次，则判定系统行为满足D，其相应的抽象算法框架参见文献中的算法；其中所提到的投影路径是为了处理状态空间中环路的出现导致所检验的系统行为路径可能是无穷长度的问题。对于系统实时行为的验证算法，则需要进一步考虑由于时间的引入所带来的如何将连续时间进行整型化处理，以及带时间约束的投影路径的建立；RTIA-Network 的一致性验证抽象算法框架参见文献。中国代写论文网与您分享论文范文

　　3. T-CBESD 的设计与实现

　　基于以上的理论分析与验证框架，本文设计了一个原型工具T-CBESD （a Tool forComponent-Based Embedded Software Designs）。T-CBESD 的目的是应用于构件化嵌入式软件开发的设计建模阶段，对设计者所关心的一些系统重要功能性质以及与时间相关的实时行为性质进行严格形式化分析和验证，以提高系统可靠性的可信度。工具的基本设计原则主要包括以下两个方面：
　　T-CBESD 应当具备跨平台运行、易扩展特征：即工具应该可以尽可能在多种不同运行平台上运行，并且考虑到在未来工作中，我们将在目前的工作基础上对接口自动机模型进行资源以及能耗等语义描述方面的进一步扩展；因此，选择了面向对象程序设计语言Java作为工具的实现语言。Java 具有良好的跨平台运行特征以及丰富的类库资源，并可以使用面向对象程序设计思想中的类继承等方法对工具进行方便可靠的扩展。
　　T-CBESD 应当具备易使用、易维护特征：用户可以比较方便的使用工具，或进行调整；因此，选择了工业界广泛使用的开放集成开发环境Eclipse 作为工具的运行平台，即使用Eclipse 的插件（plug-in）技术来设计和开发T-CBESD。用户可以很容易在Eclipse 环境中通过插件技术来安装、配置和使用工具；同时，在T-CBESD 的输入输出接口中所使用的XML语言在Java 和Eclipse 环境中也是得到完全的支持。
　　主要的逻辑处理框架包括：
　　输入输出接口； UML 顺序图模型的预处理；自动机组合模型的建立；非实时功能验证算法的实现；实时功能验证算法的实现等。以下分别给出详细说明。

　　3.1 输入输出接口设计
　　T-CBESD 的输入输出均是以XML 文件形式来描述的系统设计模型、系统需求规约以及验证结果信息等。其中，工具的输入包括：描述系统设计的接口自动机模型的XML 文件和描述系统规约的消息交互序列的XML 文件；输出则包括：描述系统组合行为的接口自动机组合模型的XML 文件和包含验证结果信息的XML 文件。这里，最核心部分是接口自动机模型的XML 文件格式的设计。在图3 中给出了一个非实时构件基本接口自动机模型的XML 文件示例说明；通过XML 的树形标签格式，分别定义了自动机名、自动机个数（如果这是一个组合自动机）、状态个数、状态名、后继状态名、转换个数、转换名、转换的出发和到达状态名、动作个数、动作名、动作类型等数据信息，用来完整准确的保存接口自动机模型的语义信息。此外，对于扩展的实时接口自动机模型，其相应的XML 文件格式定义中还包含与动作相关联的时间区间约束标记。

（科教作文网http://zw.ΝsΕac.cOM编辑）

　　在上述定义的XML 文件基础上，就可以使用Java 类库中的DOM（文档对象模型）方法很方便的对自动机模型进行解析及生成。例如：在T-CBESD 中设计了parseXmlDocument（）和parseRtXmlDocument（）两个类方法来分别对基本接口自动机模型XML 文件和实时接口自动机模型XML 文件进行解析，并根据Automata，Transition 以及State 等类定义在内存空间创建相应的自动机对象。

　　3.2 UML 顺序图模型的输入预处理
　　虽然 T-CBESD 的输入输出定义为标准XML 文档格式，但在工具中加入了从UML 建模环境Rational Rose 的顺序图模型到T-CBESD 的XML 输入文件（描述消息交互序列集）的自动化转换处理。其原因有二：