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

精品文档2016全新精品资料全新公文范文全程指导写作独家原创1/18初探一种构件化嵌入式软件设计模型验证工具1引言嵌入式计算系统已经广泛的应用于生活中的各个领域，如交通、能源、医疗、控制、通信、军事等。近年来随着计算机硬件性能的不断提高，嵌入式系统中软件的规模和复杂性不断增加，使软件对整个系统的影响逐渐占据了统治地位。关键系统中的嵌入式软件失效将会导致生命与财产的重大损失。因此，嵌入式软件通常具有极高的功能可靠性、严格的实时性等要求，如何保证系统同时满足给定的功能和非功能需求已成为当前高可信嵌入式计算领域中的研究热点。目前，工业界已有一些比较有效的嵌入式软件测试和调试方法（如在处理器中嵌入ICE功能，调试代理软件，JTAG模拟等）。但从软件工程的角度来看，这些方法都是在系统的开发中后期阶段所使用，而在嵌入式软件设计与分析的前期阶段还缺乏有效的方法和工具对系统设计进行分析与验证。本文基于接口自动机模型对构件化嵌入式软件设计（CBESDCOMPONENTBASEDEMBEDDEDSOFTWAREDESIGNS）的分析与验证方法展开进一步研究，在ECLIPSE开放平台上实现了一个CBESD的模型分析与验证原型工具TCBESD（ATOOLFORCOMPONENT精品文档2016全新精品资料全新公文范文全程指导写作独家原创2/18BASEDEMBEDDEDSOFTWAREDESIGNS）。该工具的目的是应用于构件化嵌入式软件开发的设计建模阶段，对设计者所关心的系统重要功能性质以及与时间相关的实时行为性质进行严格形式化分析和验证，提高系统可靠性的可信度。本文内容安排如下第2节中给出了非实时功能行为验证以及实时功能行为验证的理论基础，包括描述系统动态行为的多种接口自动机模型，基于场景的系统规约描述模型，以及形式化分析与验证的抽象算法等。在第3节中给出了原型工具TCBESD的基本设计思想，非实时功能行为验证模块以及实时功能行为验证模块的设计与实现，包括工具输入输出接口设计、状态空间数据结构设计、基于场景的系统规约模型的输入预处理、具体验证算法的设计与实现等。第4节中给出了应用实例研究；最后是相关工作比较和结束语，对本文中原型工具的特点、意义以及进一步的工作进行简要讨论。2工具的理论基础软件工程中的构件化设计方法学通过复用和组合软件模块来构造系统，从而提高系统开发效率和可靠性。通常，一个复杂的嵌入式系统由多个计算子系统构成，其软件系统也具有较高的构件化特征，因此，构件化的设计已成为解决嵌入式软件设计复杂性问题的一种手段。与此同精品文档2016全新精品资料全新公文范文全程指导写作独家原创3/18时，构件接口之间的交互场景也成为体现系统行为复杂性的一个重要方面。本文中所讨论的原型工具就是使用形式化的接口自动机模型来对系统构件接口动态行为进行设计建模，并使用UML交互概观图模型来描述多种基于场景的构件交互行为规约，然后应用形式化分析算法对设计模型是否满足系统规约进行分析和验证。21建模系统构件以及组合行为接口自动机（INTERFACEAUTOMATA，简称IA）是用来刻画软件构件接口交互行为时序特征的一种形式化语言。它描述了一个构件被使用的时候其对外界环境的输入假设和输出保证，即构件内方法被调用的先后次序以及构件对外环境输出调用信息或结果的次序。输入动作可以用来建模1）构件内可以被调用的方法或过程；2）通信信道的接收端；3）调用外部过程的返回等。输出动作可以用来建模1）对其他构件中的方法或过程的调用；2）通信信道的发送消息端；3）构件中方法或过程的调用结束时的返回；4）构件中方法或过程执行中出现的异常返回，等。内部动作则表达了两个构件在组合过程中的同步交互行为。考虑到嵌入式软件的实时性建模需求，需要对IA进行实时语义的扩展，以增强接口自动机对实时系统的描述精品文档2016全新精品资料全新公文范文全程指导写作独家原创4/18能力。直观上，对接口自动机每一个转换添加时间区间约束，以表示此转换发生的最小、最大时限；扩展后的模型称为实时接口自动机。我们使用接口自动机的组合状态空间来表达多构件系统的组合行为；自动机组合状态空间中每一条可能的状态转换序列用来表达多构件系统的一个组合行为轨迹。基本IA和扩展的RTIA组合状态空间的定义略有不同，以下只给出了RTIA组合空间（实时接口自动机网络）的定义；不带时间语义的基本接口自动机的组合定义参见文献。22基于场景的交互行为规约在基于场景的系统规约中，通常将一个系统相对独立的功能模块建模为一个场景描述。这个场景表达了参与其中的各构件之间如何进行交互。进一步的，在系统设计阶段，还会关心有多个简单场景组合起来的复杂场景需求，即需要考虑多个简单场景之间的逻辑关系。交互概观图（INTERACTIONOVERVIEWDIAGRAMS）是在UML2规范中引入的一种用以描述系统中复杂交互场景的动态行为模型。交互概观图本质上是将活动图模型与顺序图模型结合在一起，图中的每一个节点都可以视为一个用顺序图表达的简单交互场景，然后利用活动图所提供的顺序、迭代、并发、选择等操作将多个不同的顺序图场景联系在一起；这样就可以用来表达语义更为丰富的系统交互行为。精品文档2016全新精品资料全新公文范文全程指导写作独家原创5/18在本文中所关心的以下几种场景组合一致性问题都可以用交互概观图来有效的描述1存在一致性某个特定的场景D是否在系统所有行为中至少出现一次，或者某个指定的场景D是否在系统的所有行为中一定不会出现。2前向强制一致性当某个条件场景D1出现时，则场景D2一定会随之在系统后续行为中发生。3逆向强制一致性当某个条件场景D1出现时，则场景D2一定在D1之前就在系统的行为中发生。4双向强制一致性当两个条件场景D1、D2在系统一个行为中先后出现时，则在这两个场景之间一定有D3发生。23模型分析与验证算法基于以上给出的接口自动机系统组合行为模型以及交互场景系统规约模型，可以对22节中提出的多个基于功能的一致性验证问题进行分析与验证；同时，考虑嵌入式软件设计中的实时需求，以上每个基于功能的一致性验证问题都存在一个相应的带时间约束的版本；即在完成功能性验证的同时，也必须同时满足交互场景中给定的时间约束。在相关研究工作中，对上述几类模型验证问题进行了形式化定义和分析，并分别设计了相应的验证算法。算法的基本思想是对带有不同语义信息的系统组合行为的状精品文档2016全新精品资料全新公文范文全程指导写作独家原创6/18态空间进行搜索，将每一个可能的系统行为与基于场景的交互规约进行比较，来判断设计模型是否满足各种系统规约。例如对于存在一致性验证问题，如果在组合状态空间中顺序图D所描述场景中的消息事件序列至少出现一次，则判定系统行为满足D，其相应的抽象算法框架参见文献中的算法；其中所提到的投影路径是为了处理状态空间中环路的出现导致所检验的系统行为路径可能是无穷长度的问题。对于系统实时行为的验证算法，则需要进一步考虑由于时间的引入所带来的如何将连续时间进行整型化处理，以及带时间约束的投影路径的建立；RTIANETWORK的一致性验证抽象算法框架参见文献。中国代写论文网与您分享论文范文3TCBESD的设计与实现基于以上的理论分析与验证框架，本文设计了一个原型工具TCBESD（ATOOLFORCOMPONENTBASEDEMBEDDEDSOFTWAREDESIGNS）。TCBESD的目的是应用于构件化嵌入式软件开发的设计建模阶段，对设计者所关心的一些系统重要功能性质以及与时间相关的实时行为性质进行严格形式化分析和验证，以提高系统可靠性的可信度。工具的基本设计原则主要包括以下两个方面TCBESD应当具备跨平台运行、易扩展特征即工具精品文档2016全新精品资料全新公文范文全程指导写作独家原创7/18应该可以尽可能在多种不同运行平台上运行，并且考虑到在未来工作中，我们将在目前的工作基础上对接口自动机模型进行资源以及能耗等语义描述方面的进一步扩展；因此，选择了面向对象程序设计语言JAVA作为工具的实现语言。JAVA具有良好的跨平台运行特征以及丰富的类库资源，并可以使用面向对象程序设计思想中的类继承等方法对工具进行方便可靠的扩展。TCBESD应当具备易使用、易维护特征用户可以比较方便的使用工具，或进行调整；因此，选择了工业界广泛使用的开放集成开发环境ECLIPSE作为工具的运行平台，即使用ECLIPSE的插件（PLUGIN）技术来设计和开发TCBESD。用户可以很容易在ECLIPSE环境中通过插件技术来安装、配置和使用工具；同时，在TCBESD的输入输出接口中所使用的XML语言在JAVA和ECLIPSE环境中也是得到完全的支持。主要的逻辑处理框架包括输入输出接口；UML顺序图模型的预处理；自动机组合模型的建立；非实时功能验证算法的实现；实时功能验证算法的实现等。以下分别给出详细说明。31输入输出接口设计TCBESD的输入输出均是以XML文件形式来描述的系统设计模型、系统需求规约以及验证结果信息等。其中，精品文档2016全新精品资料全新公文范文全程指导写作独家原创8/18工具的输入包括描述系统设计的接口自动机模型的XML文件和描述系统规约的消息交互序列的XML文件；输出则包括描述系统组合行为的接口自动机组合模型的XML文件和包含验证结果信息的XML文件。这里，最核心部分是接口自动机模型的XML文件格式的设计。在图3中给出了一个非实时构件基本接口自动机模型的XML文件示例说明；通过XML的树形标签格式，分别定义了自动机名、自动机个数（如果这是一个组合自动机）、状态个数、状态名、后继状态名、转换个数、转换名、转换的出发和到达状态名、动作个数、动作名、动作类型等数据信息，用来完整准确的保存接口自动机模型的语义信息。此外，对于扩展的实时接口自动机模型，其相应的XML文件格式定义中还包含与动作相关联的时间区间约束标记。在上述定义的XML文件基础上，就可以使用JAVA类库中的DOM（文档对象模型）方法很方便的对自动机模型进行解析及生成。例如在TCBESD中设计了PARSEXMLDOCUMENT（）和PARSERTXMLDOCUMENT（）两个类方法来分别对基本接口自动机模型XML文件和实时接口自动机模型XML文件进行解析，并根据AUTOMATA，TRANSITION以及STATE等类定义在内存空间创建相应的自动机对象。32UML顺序图模型的输入预处理精品文档2016全新精品资料全新公文范文全程指导写作独家原创9/18虽然TCBESD的输入输出定义为标准XML文档格式，但在工具中加入了从UML建模环境RATIONALROSE的顺序图模型到TCBESD的XML输入文件（描述消息交互序列集）的自动化转换处理。其原因有二其一，现在工业界已存在较为成熟的图形化建模工具，可以快速方便的绘制UML模型图，可以利用这些工具作为TCBESD的前端，而不用在TCBESD中重新设计复杂的用户接口来支持图形化建模设计。其二，在22节中提到，一个顺序图场景可能会包含多个不同的消息事件序列；显然，如果让系统设计与分析人员从每一个顺序图中手动的生成所有可能的消息事件序列，这并不是件容易的事情。因此，需要提供一种从顺序图模型自动化生成所有可能的消息事件集合的方法。在RATIONALROSE中所生成的顺序图模型文件是MDL格式，需要先转换成XML格式文件，然后进行相应消息序列的抽取。其处理过程如图5中所示，首先通过在RATIONALROSE中加载XMI插件将MDL格式的文件转换为XML格式；然后对XML文件进行解析，建立文档解析树，提取消息事件节点，并根据顺序图中的事件发生先后顺序构造一个相应的有向无环图（在此，定义了顺序图的参加者类（ELEMENTCLASS）、消息类（MESSAGECLASS）以及结点类（NODECLASS）用于图的构造）；最后设计了一个拓扑排序精品文档2016全新精品资料全新公文范文全程指导写作独家原创10/18算法，对该有向图中的消息事件节点进行拓扑排序，从而得到一个顺序图中所有可能的消息事件序列的集合。33自动机组合模型的建立接口自动机的组合过程与一般自动机组合的语义存在不同之处。在两个接口自动机组合的状态空间中，有可能存在两个构件接口之间交互不同步的所谓“非法状态”，在应用验证算法之前必须将这些非法状态找出来并从状态空间中去除掉。文献中给出了一个识别非法状态集合的基于不动点（FIXPOINT）的抽象算法框架，基本思想是先构造出所有可能的组合状态的空间图，然后逆向搜索非法状态集。在TCBESD的实现中我们则采用正向的合法状态集合构造方法，其好处是避免了需要首先生成所有的状态空间。给出了工具中基本自动机模型的组合算法流程图。此外，在实时接口自动机组合的过程中还需要进一步考虑时间约束；如在21节中形式化定义表示一样，所得到的每一个组合状态都会有一个相应的时间标记值。34非实时功能性质验证算法的实现在33节中建立的自动机组合状态空间的基础上，就可以应用文献中的一致性验证算法等对32节中所给出系统需求中的消息交互序列进行分析验证。TCBESD中实现了包括存在一致性、前向一致性、逆向一致性以及双向一致性在内的多种形式的非实时功能行为验证算法。给出了精品文档2016全新精品资料全新公文范文全程指导写作独家原创11/18工具中非实时功能性质验证模块的类图框架。主要包括两大部分一部分是自动机模型核心类，包括AUTOMATACLASS，TRANSITIONCLASS，STATECLASS以及组合模型的COMPOSITIONCLASS；另一部分则是与验证算法相关的类，包括EXISTCONSISTENCYCHECKINGCLASS，ACTIONSTRINGCLASS，ADJACENTMATRIXCLASS和辅助类TRANSITIONNODECLASS。其中，存在一致性验证类（EXISTCONSISTENCYCHECKINGCLASS）作为功能验证算法类的基类，其他形式的一致性验证算法类（如BACKWARDCONSISTENCYCHECKINGCLASS，FORWARDCONSISTENCYCHECKINGCLASS和BICONSISTENCYCHECKINGCLASS等）都依赖存在一致性验证类，调用其方法实现所需的功能。在基类EXISTCONSISTENCYCHECKING的实现过程中，一个关键的问题是当在系统组合状态空间图中搜索与UML顺序图交互序列所对应的投影路径时，有可能出现一个满足条件的投影路径一部分出现在某个环路内部，而另一部分却出现在此环路的外部路径上的情形11,12。如果只是采用经典的深度优先遍历或广度优先遍历方法对组合状态空间图进行搜索判定，将会遗漏掉这种情况。为此，在TCBESD中设计了动作名表（ACTIONSTRINGCLASS）和邻接矩阵（ADJACENTMATRIXCLASS）。其中，动作名表是以接口自精品文档2016全新精品资料全新公文范文全程指导写作独家原创12/18动机的动作名作为表头向量，并以执行该动作名的转换作为表结点的一张哈希表，其定义见图8所示（注未包含类方法说明）。基本思想为对于所给出的一个消息交互序列，先根据消息名从动作名表中依次取出与消息名所对应的表头结点以及表结点，构成一张与消息序列中消息次序对应的消息名表。然后遍历这张消息名表来搜索投影路径，搜索过程中需要根据邻接矩阵来判断两个结点之间是否可达。35实时功能性质验证算法的实现在实时功能性质验证算法的实现中，考虑到实时一致性验证抽象算法框架实际上包含了两次对组合系统状态空间图的搜索过程；也就是说在非实时功能一致性验证中只需找到一条满足条件的投影路径，而在实时功能一致性验证中，是需要先根据消息序列找出所有可能的投影路径，然后进行检验。因此，TCBESD中依据动作名表以及邻接矩阵对图进行穷举搜索，搜索到一条投影路径之后并不立即结束，而是继续找下一条投影路径，找出所有与给定路径相符合的投影路径。在此基础上根据所给出的时间布尔表达式对这些投影路径进行筛选，如果找到符合时间布尔表达的投影路径验证则验证成功，否则，验证失败。4实例应用精品文档2016全新精品资料全新公文范文全程指导写作独家原创13/18目前，TCBESD的设计开发和运行环境是WINDOWSXP操作系统平台，ECLIPSESDK340，JAVASDK16，所引用的MDL文件是由RATIONALROSE2003生成。本节中分别给出TCBESD的非实时功能性质验证和实时功能验证两方面的实例应用说明。在TCBESD中所构造的构件COMMUNICATION和USER的合法组合状态空间（去除了非法状态集）包括6个组合状态（S0|S0），（S1|S1），（S2|S1），（S3|S1），（S4|S1），（S5|S1）。对于存在一致性验证，不妨设顺序图中抽取的一个消息交互序列SENDNACKSENDACK作为验证规约，显然，直观上就能判断COMMUNICATION和USER的组合系统应该是满足这个规约的。运行TCBESD进行验证的结果，显示组合系统确实满足存在一致性，其相应的系统执行路径为S0|S0S1|S1S2|S1S3|S1S4|S1S5|S1。对于前向一致性验证，就本例而言，不妨设D1消息序列为SENDNACK，D2消息序列为SENDACK，然后将其作为工具的系统规约来输入，其验证结果应该仍然是满足。运行TCBESD的验证结果，显示的确存在一条系统执行路径满足前向一致性。事实上，所找到这条路径与存在一致性的路径是相同的。精品文档2016全新精品资料全新公文范文全程指导写作独家原创14/18对于逆向存在一致性，若设D1消息序列是SEND，D2消息序列是ACK，TCBESD给出的结果是不存在这样的一条组合系统路径满足它。这也符合对本例的直观判断，即在接受到ACK之后又执行SEND动作是不合法的，因此这个存在一致性是不满足的。对于双向一致性，若给出的D1消息序列是SEND，D2消息序列是SEND，D3消息序列是NACK，验证的结果是搜索成功，得到的可满足的组合系统执行路径为S0|S0S1|S1S2|S1S3|S1S4|S1。图13所示为TCBESD的非实时功能验证模块插件的界面。界面左边部分为操作区，主要提供组合、查看、工具输入、验证类型等功能选择，界面右边部分为分析与验证过程中工具所反馈的数据信息。5相关研究工作SPIN是一个经典的分布式系统模型检验工具。系统每一个构件的自动机模型使用SPIN中PROMELA语言所构造的进程（PROCESS）来表达，组合系统的状态空间通过计算所有自动机异步积来得到，系统规约使用LTL时序公式描述；系统是否满足规约性质则通过组合系统和时序公式相对应的BUCHI自动机进行同步积，然后检验其结果是否为空。目前SPIN在工业界硬件设计以及通信协议规约的验证领域得到了较广泛的应用，但对同时具有功能和非功能需精品文档2016全新精品资料全新公文范文全程指导写作独家原创15/18求的嵌入式软件验证领域，SPIN并未提供相应的支持。UPPAAL是一个基于时间自动机理论的实时系统仿真和验证工具。其基本思想为将实时系统的行为建模为一个实时自动机网络，并进行了数据类型的扩展，采用时间算子作为系统的规约语言，主要对系统进行安全性和活性等性质的检验。UPPAAL具有良好的图形化编辑和模拟功能。目前，已有一些工具以UPPAAL为核心作进一步扩展，如TIMES是以时间自动机模型验证为基础的一个工具集环境，可以进行建模、可调度分析、系统合成以及特定平台上的代码生成；SAVEIDE则是基于构件模型SAVECCM20所建立的一个支持构件化嵌入式系统开发的工具集，等等。此外，与接口自动机相关的工具包括CHIC是第一个基于接口自动机理论的原型工具。它是作为JBUILDER集成环境下的一个插件模块来设计开发的，其目的只是用于对相关理论工作的一个初步验证，现在已经被另一个工具TICC所替代。TICC的理论基础是接口自动机的一个扩展版本SOCIABLEINTERFACE，其基本思想仍然是检验构件接口组合中是否兼容。PTOLEMYII中也实现了基本接口自动机模型的组合兼容性分析工作，不过PTOLEMYII是一个包含了多种不同工具集的混成系统建模、分析、合成和代码生成的开发环境。此外，以法国INRIA为中心的欧洲多个研究机构精品文档2016全新精品资料全新公文范文全程指导写作独家原创16/18正在构建的OPENEMBEDD是一个以ECLIPSE为开放平台的模型驱动嵌入式系统开发工具集。这是一个庞大的开源工具组合环境，提供嵌入式系统设计（包括软件和硬件）、模拟、验证、合成以及测试等各个阶段的开发支持。与上述相关工具相比，TCBESD的特点在于首先，可以直接使用UML的顺序图模型作为系统规约输入进行验证，而不需要系统设计人员去重新学习时序逻辑语言来构造规约说明；避免了在大多数相关工作中需要在不同的形式模型之间进行复杂转换，通常这些转换是需要相当的空间和时间消耗。其次，相比较上述基于接口自动机模型的研究，本文的工作在接口自动机组合兼容性的基础上对构件式嵌入式软件系统设计模型与场景式规约模型之间的一致性问题给出了一个更为完整的验证框架；可以进一步进行各类一致性问题的分析和验证；第三，通过扩展时间区间所得到的实时接口自动机的描述能力本质上与时间自动机的描述能力是等价的，并且通过在顺序图模型中使用时间不等式约束，使得所定义的实时接口自动机网络与带时间约束的顺序图之间的一致性问题更具有一般性。最后，ECLIPSE开放平台给工具提供了良好的开发、维护和使用环境。6结束语及未来工