技术报告基于MVSAS软件自适应UML建模及其形式化验证方法研究

1、计划类别 项目编号 项目技术报告课题名称 项目主持人 承担单位 题目：基于MV4SAS研究软件自适应UML建模及其形式化验证方法研究基于自适应UMI软件开发效率提升的要求以及自适应软件可靠性的保障要求，此次研究提出了MV4SAS方法，其促进了可视化UML与严格化时间自动机的有机结合，能够实现软件自适应建模与形式化验证，首先在UML扩展机制作用下引入新的构造型、标记值以及约束条件等，在软件自适应建模设施基础上构造相应的软件自适应结构模型与行为模型，并通过转换算法实现软件自适应行为模型向时间自动机网络的转换，构建软件自适应形式化模型，对软件自适应形式化验证的性质进行定义，利用模型检测工具UPPAA

2、L对软件自适应模型的可靠性进行验证，结果显示该方法能够在一定程度上降低软件自适应建模与验证的复杂性，提升建模效率，可靠性高，值得参考借鉴。关键词：MV4SAS；软件自适应；UML建模；形式化验证1 引言（Introduction）随着现代科学技术的不断发展，我国的软件规模复杂程度及用户的需求不断加大，这也在一定程度上对软件运行、维护提出了更大的挑战1，在这样的发展环境下，软件自适应技术应运而生，其能够增强软件的环境适应能力，满足用户多变的需求，在运行过程中根据软件信息对相关参数、结构等进行调整，消除软件运行变化带来的消极影响，确保软件服务能力的提升，因此，对软件自适应UML建模及其形式化验证方

3、法的研究有着重要的实践意义与应用价值。2 预备知识概述（Summary of preliminaryknowledge）2.1 软件自适应概念模型作為软件自适应研究的前提与基础，概念模型受到了国内外学者的广泛关注，国外学者提出的软件自适应概念模型主要包括MAPE-K自治计算模型、监视探测决策行动软件自适应模型等2，3，我国学者针对群体自适应提出了Auxo模型，面向复杂信息系统提出了软件模糊自适应SFSA模型，其适应的领域不同，然而都体现了感知决策执行自适应环的内涵与价值4。在自适应目标驱动下，软件能够根据运行环境及自身状态的变化对行为做出适当的调整，完成自适应环与运行环境、用户等之间的交互。此

4、次研究对原有的MAPE-K模型进行了相应的改进，具体见图1，该自适应软件系统主要包括自适应逻辑单元与应用逻辑单元，自适应逻辑单元中的各个模块共享一个知识库构建，此次研究将以该框架为原型构建软件自适应结构模型。2.2 UML及其扩展机制概述作为一种面向对象的可视化建模语言，统一建模语言（UML）能够提供多种图元，从多个视角与层次对复杂软件的结构、特性进行描述，在各个领域中均有着广泛地应用。UML模型主要包括结构模型与行为模型两种，常见的典型结构视图有构件图、类图等，行为视图有状态图、序列图等5。以类图为例，其是软件结构模型可视化、文档化的重要条件，尽管其在运行过程中包含部分具体化行为元素，然而其

5、主要根据其他视图刻画动态特征。从当前UML的建模设施现状看，其能够满足大多数领域需求，然而对于部分特定领域还缺乏一定的建模能力，必须对其进行适当的扩展，要求在原模型的基础上作出通用的扩展，常见的有增加新属性、添加建模设施、增加语义描述等。2.3 时间自动机理论与形式化验证工具为了有效解决实时系统建模及验证问题，可以对自动机理论作出新的扩展，即时间自动机，其能够通过简单的方法对包含时间因素的系统进行描述，进而为实时系统行为建模及性能分析提供形式化模型。国外学者根据时间自动机理论提出了UPPAAL、SPIN模型检测工具3，4。以UPPAAL模型检测工具为例，其主要采用了整型变量时间自动机网络模拟实

6、时系统及时序逻辑TCTL刻画系统性质，在有限状态搜集验证系统的作用下，判断系统能够达到期望性质6。其性质验证规范语言的语法为。3 基于MV4SAS软件自适应UML建模及其形式化验证方法（Adaptive UML modeling basedon MV4SAS software and its formal verificationmethod）尽管UML建模语言具有可视化特征，便于理解、交流能够达到国际工业标准，然而由于模型检测形式化语义的缺乏，其对软件模型的描述很大程度上是半形式化。基于自动机严格语法、语义的特点，其能够实现软件行为分析、求精与验证，然而，缺乏直观性，为软件开发人员的理解带来

7、了一定的难度。UML与自动机在模型验证及软件建模等方面有着较高的互补性7，因此，可以采用UML可视化建模方法与时间自动机进行形式化建模相结合的方式，通过融合扩展对UML及自动机软件自适应建模进行形式化验证，其具体过程如图2所示。首先，要构建软件自适应可视化模型，在MAPE-K改进模型扩展及UML模型裁剪的基础上，构建自适应类图，对自适应软件的结构特征进行描述，然后经过转换作用，使软件自适应可视化模型转变为形式化模型，并通过定义模型转换算法，实现可视化自适应序列图向形式化时间自动机网络的转换，构建软件自适应形式化模型，最后对上述模型的可靠性进行验证。4 UML扩展的软件自适应建模（UML ext

8、endedsoftware adaptive modeling）4.1 自适应类图类图主要指的是对软件结构的可视化描述，此次研究对UML类图进行了扩展，添加了部分软件自适应建模设施，构建了面向软件的自适应结构模型，该自适应类图模型包含一个四元组ACD：=（CA，RA，AA，SA），其中CA表示的是自适应类有限集合，CA=监视，分析，计划，执行，知识库，用户，环境。RA表示的是自适应关系有限集合，RA表示的是基于UML的关系构造，其能够体现出自适应软件各功能单元之间的连接关系。AA表示的是自适应属性集合，其中部分属性采用标记值的方式附加在CA构造型中，其中A表示的是Class属性Attribut

9、e的集合，Tag表示的是添加标记值的集合，能够应用于刻画显示性功能单元的类型与属性8。约束条件集合则采用SA表示，分别表示时间约束与事件约束，此次研究在描述定义约束条件时采用的是对象约束语言OCL。此次研究要求在MAPE-K环的每个单元都能够上升一阶要素实施描述、刻画，与此同时，受软件自适应环与用户、软件运行环境以及动态交互等过程的影响，可以对用户、环境及软件等进行独立实体描述，另外可以将复合结构的类如CA元素泛化成为具体的类。在扩展UML的作用下，自适应类图能够构建自适应关系，并通过软件对自适应类交互关系进行刻画，其语义描述如表1所示。 4.2 自适应序列图UML序列图主要是对对象之间动态交

10、互关系的描述，其能够对刻画对象消息传递时间顺序，以及系统预期功能等做出准确的反应，然而UML序列图也具有自身的缺陷性，其不能够对单个对象某一时间段内的活跃状态进行反映，加大了形式化验证的难度，此次研究通过横向与纵向两个维度对UML序列图进行扩展，并对软件自适应行为模型做出了定义。自适应序列图为一个五元组，具体表示为，其中软件自适应过程对象有限集合采用OA表示，OA=监视，分析，规划，执行，知识库，用户，环境。对象生命线上状态有限集合采用STA表示，ST*A表示的是除去空事件的所有不重复状态集合，即。MA表示的是有穷消息集合，与此同时自适应序列图还在UML序列图基础上对sim、alt和loop三

11、个片段进行了定义，可以表示为FG=，每一个片段都有片段名与执行条件构成，其中sim表示的是简单片段，执行条件为空，alt则为分支选择片段，其下一状态流向往往由执行条件决定。而loop则为循环片段，当条件为真，那么其包含的对象能够转化成为激活状态。约束有限集合采用SA表示，具体表示为，分别代表的是状态内部与状态之间的约束集合状态。自适应序列图也可以采用二维表表示，用横向表示空间轴，代表参与自适应协作的对象集合；纵向则表示时间轴，代表对象生命线，其能够反映出单个对象对一定时间内的活跃情况。另外，自适应序列图还对组合片段与约束的概念进行了强化，体现了软件自适应实时性的特征。此次研究的自适应序列激昂U

12、ML序列图与状态图进行了无缝衔接，不仅能够对自适应环中的各个软件实体交互关系进行刻画，而且能够对特定周期内单个软件实体的活跃状态进行准确描述，与此同时在形式化定义作用下，其能够实现向时间自动机模型的有效转化，进而为软件自适应形式化验证奠定坚实的基础。4.3 基于UML扩展的软件自适应建模原则此次研究软件自适应建立的本质为自适应环（监视、分析、規划、执行）与不断变化软件的交互，因此必须将参与自适应过程的软件实体及自适应环作为一阶要素给予显示化建模与刻画。其次，要遵循自适应逻辑外置分离原则，一般可采用外置式方式，从目标软件系统中对自适应逻辑进行分离，这能够在一定程度上避免应用逻辑与自适应逻辑之间的

13、交织。除此之外，还必须遵循约束条件规范描述原则，对时间约束与事件约束进行相应的规范，其能够为软件自适应UML模型转换奠定基础。5 软件自适应模型转换与形式化验证（Softwareadaptive model transformation and formalverification）5.1 软件自适应UMI模型向时间自动机模型的转换通常，自适应序列图ASD能够对时间自动机网络，以及生命周期状态变化情况进行映射与刻画；自适应序列图的状态即State则能够有效映射时间自动机位置，每个自动机TA的位置集合均有相应的对象纵轴状态集合表示，且ASD纵轴初始状态一般对应的是时间自动机的初始位置。自适应序列

14、图消息message则被映射成为时间自动机通道，且每个消息都恰好与时间自动机的发送事件、接收事件一一对应。另外时间自动机的约束S与自适应序列图约束SA相对应，状态间约束Sinter及分段约束FG则分别对应时间自动机边E的约束S，时间自动机位置不变式Invariant则对应状态内部约束Sintra。为了确保自动机模型的有效运行，在建模过程中，建模工作人员需要结合实际情况对自动机模型进行优化处理，积极处理应用逻辑参数的动态变化，对时间自动机模型进行进一步完善。5.2 软件自适应形式化验证软件自适应形式化验证主要是对软件可靠性、自身适应能力及影响因素等的检测，主要检测的能力包括系统有无死锁、自适应规

15、则是否正确、自适应相应能力是否满足需求等9。（1）系统是否有死锁。与传统的软件有所不同，自适应软件对系统持续运行能力有着较高的要求，一般需要严密观察自适应软件系统是否进入死锁状态，避免软件运行中进入到错误状态。（2）自适应动作是否有效1。该检测主要针对的是自适应动作的执行情况，一般情况下，建模人员会事先构建自适应动作以便随时应对软件运行中的内部状态、环境及用户需求变化，与此同时还需检查其是否存在重复、冗余等。（3）自适应规则正确性。该检测针对的是系统应对某种特殊变化时的应对情况。（4）自适应快速反应能力。其主要指的是触发自适应行为后，自适应逻辑单元在一定时间内的响应速度与响应能力，其需要确保自

16、适应策略的正确性与有效性。除此之外，还需要对软件自适应行为进行模拟与形式化验证。UPPAAL所提供的simulator模拟器能够对软件自适应交互过程进行模拟，并形成一个完整的运行轨迹，若运行出现错误，系统将会立即做出反馈，便于建模人员及时做出相关调整。在UPPAAL验证器verifier中输入TCTL可靠性规约，系统能够对软件自适应性质进行自动检测，最终得到完善的软件自适应模型。6 结论（Conclusion）传统的UML具备形象、直观等特点，然而缺乏科学的分析与验证机制，其形式化方法定义相对严格，不利于软件工程师理解，基于上述因素，此次研究提出了UML扩展与时间自动机有机融合的自适应建模及形

17、式化验证方法，其不仅降低了设计难度，而且在一定程度上提升了软件建模的可靠性，值得广泛推广、应用。参考文献（References）1 赵晓宇，等.基于HUML的列控系统形式化建模与参数分析方法J.铁道学报，2016，38（11）：80-87.2 Thomas Vogel，Holger Giese.Model-Driven Engineering of Self-Adaptive Software with EUREMAJ.ACM Transactions on Autonomous and Adaptive Systems（TAAS），2014，8（4）：1-33.3 Yang ZQ，et al

18、.A Systematic Literature Review of Requirements Modeling and Analysis for Self-Adaptive Systems.Requirements Engineering：Foundation for Software Quality，2014.4 郭雨婷，潘文林，江涛.基于common logic的UML类图形式化及验证J.云南民族大学学报自然科学版，2015，22（6）：506-509.5 安越，李国宁.基于Timed-UML顺序图的RBC交接形式化建模与分析J.铁道标准设计，2016，60（6）：132-138.6 Ding Z，Zhou Y，Zhou MC.Modeling Self-Adaptive