可在www.sciencedirect.com在线获取理论计算机科学电子笔记320（2016）21-34www.elsevier.com/locate/entcs基于UML交互场景的Diversity平台的一个说明性用例马蒂尔德·阿尔诺1Boutheina Bannour2 ArnaultLapitre3CEA，LIST，嵌入式系统模型驱动工程实验室，PointCourrier 174，91191Gif-sur-Yvette，法国摘要Diversity是一个基于符号执行的多用途可定制平台。DIVERSITY的设计目的是管理不同语义的多样性，以及基于符号执行的可能分析的多样性。 在本文中，我们展示了如何多样性的输入语言，用于编码UML场景的语义，其中包括用VSL语言（在嵌入式系统MARTE的UML概要文件我们采用象征性的处决在片上系统示例3的实际场景上，以便使用在DIVERSITY中实现的高级探索策略来选择测试行为。关键词：符号执行和工具，建模语言语义，UML基于场景的交互，VSL/MARTE时间约束，测试选择策略和覆盖率。1介绍符号执行最初是为程序定义的[15]。其基本概念在于执行程序，而不是具体的数值，而是符号参数，并在执行的每一步计算这些参数的逻辑约束。符号执行允许计算程序或模型的语义，并以抽象的方式有效地表示它们。基于模型的测试（MBT）是符号执行最流行的应用之一[11，10，14，2]。符号执行已被用于选择模型的符号表示的某些部分，例如，根据某些覆盖目标，由于存在无界循环，这些部分可能是有限的。 然后，使用约束求解技术从这些选定的部分提高效率1电子邮件：mathilde. cea.fr2电子邮件：boutheina. cea.fr3电子邮件：arnault. cea.fr3部分由欧洲项目OpenES支持的工作www.openes-project.orghttp://dx.doi.org/10.1016/j.entcs.2016.01.0031571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。22M. Arnaud等人/理论计算机科学电子笔记320（2016）21近年来[9，8，4]的求解器帮助符号执行更广泛地用于此目的。许多基于符号执行的正式处理工具已经被开发用于不同的用途，例如在下面的调查中引用的（基于模型的）测试中使用的工具。与这些工具相比，DIVERSITY平台的目标是提供一个可扩展的平台，以考虑各种形式分析的可能性。为此，Diversity提供了一个通用的符号执行平台：• 足够通用，以考虑各种模型的语义;• 可扩展以允许定制基本符号处理以实现特定的正式功能（例如，MBT算法、探索策略等）。Diversity正在成为Eclipse开源项目[6]。在本文中，我们简要介绍了多样性，特别是我们提供了一个例子，它的使用。为了说明可扩展性，我们展示了如何适应探索策略Hit-or-Jump [5]，一种旨在实现目标测试覆盖率的启发式方法，可以轻松地集成到可定制的符号执行过程中为了说明Diversity的通用性，我们展示了它如何为UML序列图的语义提供有趣的支持[13]。序列图显示用于描述系统组件交互行为的UML图形语言。首先，我们已经识别了Diversity输入语言的一个子集来编码这种交互语言。事实上，DIVERSITY提供了一种称为xLIA（交互和架构的可执行语言）的枢纽语言，这是一种具有各种原语的通用语言，这些原语允许对经典语义的多样性进行编码特别是，xLIA支持涉及符号数据和通信动作的经典自动机语法。为了MBT的目的，我们在以前的工作中[3]提供了一种形式化的处理UML序列图的语义，它涉及到时间约束，使用值规范语言（VSL，在MARTE [12]的UML概要中标准化）指定，通过将它们转换成一种transition-labeled符号自动机。在本文中，我们扩展了这项工作，显示这些自动机可以实现xLIA在一个有效的方式使用异步通信机制和设施编码MARTE的时间约束。TIOSTS可以很容易地编码为xLIA的一个子集，具有简单的通信机制。在实现[3]中描述的翻译机制时，它似乎不是符号执行在性能方面的有效表示，特别是消息表示导致了不必要的计算。因此，选择一种不同的方式来翻译消息，以体现这种效果是有用的。我们希望特别强调描述翻译机制和使用Diversity进行覆盖分析，以说明该工具的更通用的功能概况. 第二节介绍了xLIA中用于序列图编码的变迁标记自动机及其相关的符号语义。第3节介绍了多样性中的符号执行过程，以及它如何与点击或跳转探索策略相结合。第4节给出了一个使用序列图规范片上系统的定时交互行为的示例M. Arnaud等人/理论计算机科学电子笔记320（2016）2123第5节举例说明了将序列图转换为xLIA，并展示了一些实验结果，这些实验结果是关于使用Hit-or-Jump探索策略的Diversity符号执行的。最后，我们在第6节结束。2xLIA中的转移标记符号自动机DIVERSITY的xLIA语言支持一种符号自动机的形式，它涉及抽象表示系统状态的变量（我们称之为数据变量）和捕获系统执行的时序约束的变量（我们称之为时间变量）。这种自动机通过在充当缓冲器的通道上交换符号项来进行通信，在缓冲器中存储发送的数据以供以后使用。 我们称这些自动机为符号转换系统（Symbolic Transition Systems，简称STS它们由三元组（Q，q0，Tr）定义，其中Q是表示控制点的一组状态，q0是Q的区别控制点称为初始控制点，Tr是一组标记的转换。转换由元组（q，θ，φt，φd，act，ρ，qJ）定义，其中q（分别为qφt是一个关于时间变量的一阶公式，称为time guard，φd是一个关于数据变量的一阶公式，称为data guard，θ是一组时间变量，act是一个通信动作，ρ是代表状态演化的数据变量的赋值。系统和> Sys {channel buffer：fifo *> > c ;statemachine or > A {var time real>t; varinteger x，y，i;...状态q1{transitiontr--> q2 { update（t）;t[i]- t[i-1] 0.3）;guardx y;<通过c输出x+y;{|和|y：= y +1; x：= y; i：= i+1};}...图1. 输出转换的DIVERSITY代码数据传递和更新转换的执行导致动作，该动作可以是发射（相应地，接收）信道c上的值v，经典地表示为c！v（resp. c？是的v），或者一个特定的动作τ，它代表不存在可观察的动作。考虑图1中以Diversity编码给出的转换trtr的作用表示通过通道c对x+y进行求值所产生的值的发射，其中x和y是数据变量，通道c与一个无界的浮点数相关联输入的一个例子是通过c输入x，这意味着通过通道c接收一个值并将其分配给x。注意这个方块|和|{...} 引入对tr的替换进行编码：内部语句是并行计算的4。比如说，4.所有顶层语句都是按顺序计算的，因此转换的不同组件的顺序很重要24M. Arnaud等人/理论计算机科学电子笔记320（2016）21假设在执行TR之前，Y最初被分配了某个值V：如果不使用该块，则这导致将V+1分配给X，然而在感兴趣的语义中，X必须被分配V。在tr的动作是输入的情况下，由输入引起的分配在其他分配之前被考虑。然后，如果在输出动作的情况下，在任何数据变量更新之前满足其数据保护，则触发转换;并且在输入动作的情况下，仅考虑由输入引起的分配。在我们的框架中，系统由一组异步运行的通信STS定义，包括数据传递。实际上，对于给定通道上的值的任何输出（即，写入关联的缓冲器），则该值可以稍后使用由不同的STS使用同一通道上的输入动作（即从相关缓冲器读取）。时代造型符号t对应于一个时间变量，它是一个捕捉tr的连续执行时刻的数组。这些瞬间是在与实数同构的时间尺度中拾取的。 语句update（t）表示将tr最后一次出现的时刻附加到t的特殊操作。在时间变量更新后，将评估时间保护。现在考虑时间保护t [i]-t [i-1] <0。3，它表示tr的两次连续执行之间的延迟低于0。3个时间单位。在第一次执行中，t[i-1]是unfined，时间保护通常被评估为true。 为此，我们定义了时间守卫的弱形式φt表示为WF（φt）φt[x]∈φt（x0≤x > len（t）），其中t[x]∈φt表示在时间保护φt内出现的时刻项，len（t）表示t的长度作为一个时间点数组。事实上，时间保护的弱形式表征了在时间瞬时项中发生的索引超出范围的情况，对应的时间变量。例如，WF（t [i]-t [i-1] <0. 3）的结果是t [i] −t [i− 1] <0。3i 1i> len（t）简化后，这是满足触发过渡的实际保护。符号语义学。我们提供STS的语义使用符号执行技术，计算所有可能的行为的自动机的形式的符号树。我们首先讨论转换的符号执行，如图2中的tr所示。这样的执行总是被描述为到达树中的执行上下文节点，表示为EC，其由以下信息组成：• 控制点，其确定哪些转换可能被执行;• 对表示持续时间的符号的约束，称为路径时间条件PCt;• 用于计算的符号数据上的约束称为路径条件PCd;路径条件完全表征了要满足的约束，以便遵循与EC相关的符号树中的路径M. Arnaud等人/理论计算机科学电子笔记320（2016）2125不D不D• 时间尺度的瞬时元素，由持续时间符号的总和表示，并且表示在先前的转换执行中遇到的最后动作的发生时刻;• 以及通过符号上的项来替换STS变量，表示它们的当前关联值。（δk+1）c！X+YECk−→ECk+1一季度二季度P CkP Ckδ0+. . . +δkσk：t[9]←δ0+. . .+δji<$10，x<$X，y<$Y c<$wP Ck<$δj+1+. . . +δk+<10。3PCkXYδ0+. . . +δk+δk+1σk：t[10]←δ0+. ..+δk+1i<$11 ， x<$Y ，y<$Y+ 1c<$w。（X+Y）图2.图1的转换的符号执行。让我们考虑ECk作为可能的EC，其中tr是到被解雇。从ECk执行tr导致引入新的符号来表示tr的持续时间，其为δk+1，并且构建新的EC，ECk+1，其中两个保护，TR满足。在EC k +1中，当前时刻δ 1+…+δ k+1被附加到时间变量t。P C t得到了一个新的约束δj+1+. . +δk+<10。其中ch表示时间保护t [i]-t [i-1]<0的满足。3：在此过渡中，i=10 ，其中t[9]←δ0+. 。 . +δj和t[10]←δ0+. ..+δk+1。 类似地，将约束startTime （ cmd ） { 优 先 级 （ cmd ， J ） > 优 先 级（cmd，j）}对应于较高优先级命令的预处理时间。的情况在只有两种优先级的情况下，紧急命令的预处理不能被中断。因此，如果cmd具有优先级HP，则finishTime（cmd）=t2[id（cmd）]且startTime（cmd）=t1[id（cmd）]。此外，委员会认为，30M. Arnaud等人/理论计算机科学电子笔记320（2016）21startTime（cmdJ）> startTime（cmd）当且仅当id（cmdJ）> id（cmd）成立，因此序列图中给出了约束的公式。图4：预处理命令图5：调度预处理命令处理预处理阶段的目的是产生信息，以简化命令的处理：命令已被划分为子命令，子命令使用给定数量的待处理信息量构建，并存储在命令队列HPQ或LPQ之一中。子命令按照其优先级以循环方式进行处理。FirmwareTaskB根据HPQ和LPQ进行计算。然后，子命令被发送到硬件进行处理，当计算结束时，硬件发回一个finished（subCmd）消息。单个子命令的处理时间必须受该子命令的权重的限制，如时间约束t2[i]-t1[i] Sys {channel< buffer：fifo< *> >msg1Channel;signal Sig（integeratt1，...）; statemachine或>A {var timereal>t1; varintegerx， y;stateq1 {transition tr1 --> q2 { update（t1）;guard x y;输出Sig（x+y，.）通过msg 1Channel;}...statemachine or > B{ timevarreal>t2; varSigs;var integer i_t2;state q3 {transition tr2 --> q4 { update（t2）;tguard WF（t2[i_t2]- t1[i_t2] 0.1）;通过msg 1Channel输入Sig;i_t2：= i_t2+ 1}...图6.异步信号传递的翻译• 输出动作输出Sig（x+y，.） viamsg1Channel隐式地构建具有属性att1，. 赋值为x+y，此实例(with中填充的属性）在通道msg1Channel中被buffered。• 经由msg1Channel的输入动作input Sig（s）表示从通道msg1Channel接收的信号被存储在目标生命线STSB中的Sig类型的局部变量s上（回想一下，该信号在系统级被全局声明）。这样，信号属性可以被B用于计算。注意，当存在与使用t [i]形式的时间瞬时项的消息的发射或接收相关联的时间保护时，我们使用索引it来捕获执行发生的最后时刻。这是接收消息msg 1的情况：在tr2中，索引i t2指的是t 2中最后定义的位置，并且在用于时间保护t2 [i t2]-t1 [i t2] <0之后相应地递增。1.组合运算符的转换主要包括创建决策和连接状态/转换，然后归纳转换其操作数中定义的行为。我们在图7中说明了alt运算符的翻译。从生命线Ai的局部角度来看，alt操作符在操作数OP1和OP2中的两种情况之间给出了一个非确定性的选择：要么发送消息msg1，要么从关联的通道消费消息msg2例如，在后一种情况下，生命线Aj旨在发送消息msg1，以便两个生命线执行相同的场景（在OP2内）。翻译引入了STS中的决策转换，以反映这些选择。生命线Ai，Aj32M. Arnaud等人/理论计算机科学电子笔记320（2016）21当地当地当地当地中文（简体）trreadSched中文（简体）trseOP1：计数器i？x x== NIL柜台！无《行动纲领》（第1、和3段）trfollowOP1： 计 数 器i ？ xx ==NIL柜台！无）trfollowOP1我trfollowOP2trreadSched：counteri？Xx无当地firstOcc（第一次发生，第二次发生，第二次发生，计划局部发生 ）==OP1 （OP1，j）：schedj！OP1counterj！1popFirstOcc（OP1，OP2，schedi） （OP1，j）：谢德岛？ypush（y，schedi）图7.选择操作符的翻译将通过经由专用调度信道schedi、schedj 发 送 协 调 消 息 来 向 彼 此 通 知 它 们 的 选择。因此，Ai忙于先前的执行，可以在sched i中从A j连续接收OP1、OP2、OP1，通知其遵循它们的嵌套行为以与A j的选择一致（参见转换tr followOP1、tr followOP2）。或者，Ai可以以更快的速率运行并发起选择（参见转换tr_riseOP1、tr_riseOP2）。注意，来自通信通道的读取是通过假设阻断，即，Ai不能测试schedi是否为空。 我们使用一个计数器通道计数器i，它被填充：每次在sched i上写入一个值时，填充1;并且填充一个特定的符号NIL，表示缓冲器的结束。此计数器通道强制Ai读取schedi中的所有值，而NIL未被读取（参见transitionstrreadSched）。从schedi读取的所有操作数名称为存储在本地缓冲器计划中，在被分析以寻找给定的操作数之前。众所周知，在完全的一般性，一些操作数OP OP1，OP2与-覆盖Ai和某个其他生命线Ak，kj的其他组合算子也可以是存储在schedi，我们在Diversity高级例程firstOcc中定义了和本地调度器上的popFirstOcc来访问和分别消费调度器中第一个出现的值（在一组给定值中）。多样性实验我们已经开发了UML2DIVERSITY，这是Papyrus [7]的一个插件，它允许将序列图自动转换为xLIA。该插件根据第4节中给出的序列图生成一个文本文件，描述xLIA中的片上系统规范：它分别包括107和199个STS状态和转换。为了证明使用第二节中描述的HoJ启发式的兴趣，第三，我们定义了两类目标• Obj1（k）：依次覆盖Request（newCmd）k次，然后 enqueue（currentCmd） K时代， 和 完成（cmd）k次• Obj2（k）：覆盖k次序列A我一操作数OP1操作数OP2MSG2refMSG1refaltM. Arnaud等人/理论计算机科学电子笔记320（2016）2133目的成功率最佳执行指标#步骤跳跃次数执行时间EC数量OBJ1（1）百分百222111s 607301OBJ1（2）百分之九十548233s867767OBJ1（4）百分百一千九百零二4012s 5612，663OBJ1（8）百分百四千四百四十三9328s4086，202OBJ1（16）百分之九十九、一百三十三1901分 4秒 3毫秒一万二千七百六十四ObJ2（16）百分百八千八百八十五1811m 2s479ms一万二千四百三十五表1交通事故指标请求（newCmd）. enqueue（currentCmd）.完成（CMD）。我们为10次试验的成功率提供了几个k值。对于成功的试验中最有效的执行，我们还给出了以下指标：计算的执行步骤数，跳转数，执行时间和计算的EC数。我们将符号探索策略参数化如下：子树探索的固定最大深度N为5，在命中事件中要保留的EC数量（在当前子树的探索期间至少覆盖一个感兴趣的转换）为7，在跳转事件中要选择的EC数量（在其构建结束时，子树中没有覆盖感兴趣的转换）为5。我们观察到，该策略有时可能无法覆盖所有期望的过渡。实际上，“打或跳”策略是一种包含随机性的策略，即在每一步结束时保留的分支数量。我们观察到，超时的发生很少，成功的探索是非常快的。特别是，注意，措施不增长指数，这将是情况下，如果我们选择使用一个更经典的探索战略。 为了说明司法部战略的有效性，请注意，一系列转换，如Request（newCmd）。. .enqueue（currentCmd）. 完成（CMD），任何经典的勘探策略都必须达到至少40的深度，这是昂贵的。 作为参考，使用BFS战略为了探索40的深度，我们计算了超过500，000个执行步骤。很明显，这样的计算成本太高，无法产生大量的测试输入，以及为什么在这些情况下需要使用逻辑分析6结论多样性的xLIA输入语言的表达语法，使我们能够编码的UML序列图，其中涉及额外的MARTE时间约束的概念在未来，我们计划支持更大的UML集合，特别是状态机似乎是UML的一个特别有趣的子集，以转换标记的符号自动机的形式反映xLIA规范。在本文中，我们还描述了符号执行实现的多样性，以及它是如何与快速探索策略点击或跳转相结合，由于多样性提供的定34M. Arnaud等人/理论计算机科学电子笔记320（2016）21制设施。性能测试-M. Arnaud等人/理论计算机科学电子笔记320（2016）2135以片上系统为例，我们总结了Hit-or-Jump策略在高并发系统模型上实现覆盖目标的适用性。我们还计划在DIVERSITY中集成更先进的技术，如Partial-Order Reduction[16]，以有效地探索并发模型。引用[1] Anand，S.，E. K. Burke，T. Y. Chen，J. Clark，M. B.科恩，W。Grieskamp，M. Harman，M. J.Harrold 和 P.Mcminn ， 自 动 化 软 件 测 试 用 例 生 成 方 法 的 精 心 策 划 的 调 查 ， J. Syst. Softw 。 86（2013），pp. 1978-2001年。[2] Bannour，B.，J. P. Escobedo，C.加斯顿和P.L. Gall，O-基于定时符号模型的一致性测试的行测试用例生成，在：测试软件和系统-第24届IFIP WG 6.1国际会议，ICTSS 2012，丹麦奥尔堡，2012年11月19日至21日。2012，pp. 119-135.[3] Bannour，B.，C. Gaston和D. Servat，从时间序列图中提取酉约束与符号技术：应用于测试，在：第18届亚太软件工程会议，APSEC 2011，越南胡志明市，2011年日，2011年，pp. 219-226.[4] 巴雷特角 ，C. L. Conway ， M. 德特斯湖Hadarean ， D. 约万诺维 奇，T 。 King 、 A. Reynolds 和C.Tinelli，CVC 4，在：计算机辅助验证-第23届国际会议，CAV 2011，Snowbird，UT，美国，2011年7月14日至20日。2011年，第101页。171-177.[5] C avalli，A. R.，D. 李角，澳-地 Rinderkne cht和F. Zadi，命中或跳跃：一种用于智能网服务应用的embedededd测试算法，见：协议工程和分布式系统的形式化方法，FORTE XII/PSTV XIX分布式系统和通信协议描述技术（FORTE XII）和协议规范、测试和验证（PSTV XIX），1999年10月5-8日，中国北京，1999年， pp. 41比56[6] CEA列表，Diversity，http://projects.eclipse.org/proposals/diversity/.[7] CEA列表，Papyrus，http://www.eclipse.org/papyrus/.[8] 德韦拉湖M.和N. Bjørner，Z3：一个有效的SMT求解器，在：系统构建和分析的工具和算法，第14届国际会议，TACAS 2008，作为欧洲软件理论与实践联合会议的一部分，ETAPS 2008，匈牙利布达佩斯，2008年 3月 29日至4月 6日。2008 年，第100页。337-340[9] Dutertre 湾 和 L. M. de Zona ， A fast linear-arithmetic solver for DPLL （ T ） ， in ： Computer AidedVerification，18th International Conference，CAV 2006，Seattle，WA，USA，August 17-20，2006，Proceedings，2006，pp. 81比94[10] 弗兰岑湖J. Tretmans和T. A. C. Willemse，基于模型的测试的符号框架，在：软件测试和验证的形式化方法，第一次联合国际研讨会，FATES 2006和RV 2006，西雅图，华盛顿州，美国，2006年8月15-16日，修订的选定论文，2006年，第10页。40比54[11] 加 斯 顿 角 ， P. L. Gall ， N. Rapin 和 A. Touil ， Symbolic Execution Techniques for Test PurposeDefinition ， in ： Proc. of Int. Conf. Testing of Software and Communicating Systems （ TestCom ）（2006），pp. 1比18[12] 群 、 O. M. ， MARTE 的 UML 概 要 ： 实 时 嵌 入 式 系 统 的 建 模 和 分 析 ， VSL （ 2009 ） ，http://www.omg.org/spec/MARTE/。[13] 群、O. M.，统一建模语言（UML）（2012），http://www.uml.org/。[14] J'eron，T.， Sym bolicmo del-bas edtestsel e.，Electr. 我是希奥。Comput. Sci. 240（2009），pp. 167-184。[15] King ， J.C. ， A new approach to program testing ， Proceedings of the international conference onReliable software10（1975）. 228-233。[16] Valmari ， A. ， Stubborn sets for reduced
我的内容管理
展开
