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

《初探一种构件化嵌入式软件设计模型验证工具》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、初探一种构件化嵌入式软件设计模型验证工具　　1.引言　　嵌入式计算系统已经广泛的应用于生活中的各个领域，如：交通、能源、医疗、控制、通信、军事等。近年来随着计算机硬件性能的不断提高，嵌入式系统中软件的规模和复杂性不断增加，使软件对整个系统的影响逐渐占据了统治地位。关键系统中的嵌入式软件失效将会导致生命与财产的重大损失。因此，嵌入式软件通常具有极高的功能可靠性、严格的实时性等要求，如何保证系统同时满足给定的功能和非功能需求已成为当前高可信嵌入式计算领域中的研究热点。目前，工业界已有一些比较有效的嵌入式软件测试和调试方法（如：在处理器中嵌入ICE功能，调试代理软件，JTAG模拟等）。

2、但从软件工程的角度来看，这些方法都是在系统的开发中后期阶段所使用，而在嵌入式软件设计与分析的前期阶段还缺乏有效的方法和工具对系统设计进行分析与验证。　　本文基于接口自动机模型对构件化嵌入式软件设计（CBESD:ponent-BasedEmbeddedSoftbeddedSoftata，简称IA）是用来刻画软件构件接口交互行为时序特征的一种形式化语言。它描述了一个构件被使用的时候其对外界环境的输入假设和输出保证，即构件内方法被调用的先后次序以及构件对外环境输出调用信息或结果的次序。　　输入动作可以用来建模：1）构件内可以被调用的方法或过程；2）通信信道的接收端；3）调用外部过程的返

3、回等。输出动作可以用来建模：1）对其他构件中的方法或过程的调用；2）通信信道的发送消息端；3）构件中方法或过程的调用结束时的返回；4）构件中方法或过程执行中出现的异常返回，等。内部动作则表达了两个构件在组合过程中的同步交互行为。　　考虑到嵌入式软件的实时性建模需求，需要对IA进行实时语义的扩展，以增强接口自动机对实时系统的描述能力。直观上，对接口自动机每一个转换添加时间区间约束，以表示此转换发生的最小、最大时限；扩展后的模型称为实时接口自动机。（转载自.ＮＳＥＡＣ.中国评价网）　　我们使用接口自动机的组合状态空间来表达多构件系统的组合行为；自动机组合状态空间中每一条可能的状态转换

4、序列用来表达多构件系统的一个组合行为轨迹。基本IA和扩展的RTIA组合状态空间的定义略有不同，以下只给出了RTIA组合空间（实时接口自动机网络）的定义；不带时间语义的基本接口自动机的组合定义参见文献。　　2.2基于场景的交互行为规约　　在基于场景的系统规约中，通常将一个系统相对独立的功能模块建模为一个场景描述。这个场景表达了参与其中的各构件之间如何进行交互。进一步的，在系统设计阶段，还会关心有多个简单场景组合起来的复杂场景需求，即需要考虑多个简单场景之间的逻辑关系。　　交互概观图（InteractionOvervies）是在UML2规范中引入的一种用以描述系统中复杂交互场景的动态

5、行为模型。交互概观图本质上是将活动图模型与顺序图模型结合在一起，图中的每一个节点都可以视为一个用顺序图表达的简单交互场景，然后利用活动图所提供的顺序、迭代、并发、选择等操作将多个不同的顺序图场景联系在一起；这样就可以用来表达语义更为丰富的系统交互行为。在本文中所关心的以下几种场景组合一致性问题都可以用交互概观图来有效的描述：　　1.存在一致性：某个特定的场景D是否在系统所有行为中至少出现一次，或者某个指定的场景D是否在系统的所有行为中一定不会出现。　　2.前向强制一致性：当某个条件场景D1出现时，则场景D2一定会随之在系统后续行为中发生。　　3.逆向强制一致性：当某个条件场景D1

6、出现时，则场景D2一定在D1之前就在系统的行为中发生。　　4.双向强制一致性：当两个条件场景D1、D2在系统一个行为中先后出现时，则在这两个场景之间一定有D3发生。　　2.3模型分析与验证算法　　基于以上给出的接口自动机系统组合行为模型以及交互场景系统规约模型，可以对2.2节中提出的多个基于功能的一致性验证问题进行分析与验证；同时，考虑嵌入式软件设计中的实时需求，以上每个基于功能的一致性验证问题都存在一个相应的带时间约束的版本；即在完成功能性验证的同时，也必须同时满足交互场景中给定的时间约束。在相关研究工作中，对上述几类模型验证问题进行了形式化定义和分析，并分别设计了相应的验证算

7、法。算法的基本思想是对带有不同语义信息的系统组合行为的状态空间进行搜索，将每一个可能的系统行为与基于场景的交互规约进行比较，来判断设计模型是否满足各种系统规约。例如：对于存在一致性验证问题，如果在组合状态空间中顺序图D所描述场景中的消息事件序列至少出现一次，则判定系统行为满足D，其相应的抽象算法框架参见文献中的算法；其中所提到的投影路径是为了处理状态空间中环路的出现导致所检验的系统行为路径可能是无穷长度的问题。对于系统实时行为的验证算法，则需要进一步考虑由于时间的引入所带来的如何