时间触发语言模型转换工具Giotto在嵌入式系统验证中的应用

理论计算机科学电子笔记152（2006）175-190www.elsevier.com/locate/entcs案例研究：时间触发语言蒂瓦达尔·塞梅蒂美国田纳西州纳什维尔范德比尔特大学软件集成系统摘要在这项研究中，我们介绍了一个时间触发语言的模型转换工具：Giotto。该工具使用图形来表示源代码（Giotto）和目标（携带调度的代码）的转换，并已实现完全使用图重写技术。输入和输出的元模型是使用标准（UML）技术指定的，转换本身是一个编程的图形重写系统（在GReAT中）。该方法说明了如何使用图变换实现非平凡的模型变换，以及如何将此处获得的结果用于嵌入式系统模型的形式化验证。这里开发的转换形成了将高级、特定领域的模型（使用时间触发语言的概念）转换为分析模型（使用分析语言的概念，例如时间自动机）的第一步。使用诸如图转换之类的形式化方法有助于确保此转换过程的正确性保留字：模型转换，图转换，时间触发，Giotto，GReAT1引言基于模型的开发依赖于模型来描述正在构建的系统的结构或特性，以及从模型合成应用程序的生成器模型帮助设计者理解和描述系统，通过关注不同的方面并抽象掉其他方面。生成器取代（或减少）了手工编码的繁琐和容易出错的任务使用基于模型的1Email：tiv@ i s i s. vander bilt. e度1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.024176T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175这种方法还有一个额外的好处，那就是用数学上精确的形式来描述系统。这使得能够以形式化的方式讨论关键属性，并通过形式化验证来证明设计的正确性。请注意，模型自然地表示为图，因此图论的许多结果可以应用于模型的上下文然而，确保模型的正确性只是第一步：为了保持通过建模建立的属性，生成最终系统的过程也必须没有错误。换句话说，生成器的指定方式也应该是正式的，适合于验证。这个论点强调了模型转换的重要性，如果模型表示为图，则可以通过图转换来实现模型转换是研究界内外都非常感兴趣的一个领域这一点可以从正在进行的...由OMG领导的dardization运动[1]。最终的实际目标是为工程师提供方法和工具，他们将使用它来设计和生产可靠的系统。当然，每一种工程方法都必须在实践中证明自己这个问题对于受理论结果影响的方法论来说下面的论文描述了一个实验，建模和转换的时间触发的嵌入式系统使用基于图形的技术的特定语言具体来说，它为这种语言引入了一个编译器，该编译器使用以图重写操作表示的模型转换。人们相信，这种语言的目标领域（高置信嵌入式系统）是上述形式化方法的主要目标，这些实验将吸取重要的经验教训在实施该项目的过程中，采取了以下步骤(i) （Meta-）使用UML对输入和输出语言进行(ii) 确定编译器要解决的问题(iii) 用公式化的图形变换来解决这个问题2输入和输出语言GME [2]环境用于为源模型和目标模型创建元模型GME是一个元可配置的可视化建模工具包：每个领域特定建模语言（DSML）的元模型（或GME术语中的范式）使用基于UML的MetaGME语言进行指定然后，根据这些元模型的模型可以通过GME用户界面进行操作此外，GME提供了一个API来访问和操作作为对象和链接网络的模型每个模型元素（对象和T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175177链接）具有在元模型中定义的特定的对应类型（类和关联）为GME定义元模型包括以下步骤：(i) 使用MetaGME在UML中定义模型的元素和结构(ii) 通过模型方面定义GME用户界面的可视化规则，并将图形表示（图标）分配给模型元素(iii) 制定OCL约束，在DSML中强制执行格式良好和在下面的章节中，我们将简要介绍本实验中使用的两种语言（Giotto和E-code）的元模型。2.1乔托时间触发语言Giotto [5]是一种用于嵌入式系统编程的时间触发语言Giotto专为周期性和多模态操作系统而设计，例如需要周期性传感器读数、控制律计算和执行器更新的控制应用。乔托系统可能有多种操作模式。在每种模式下，执行系统活动（传感器读取，执行器更新，计算任务）的不同（可能重叠）子集。根据时间触发范式，系统的所有活动必须是严格周期性的，在不同的模式下可能有不同的频率。由于其时间触发的性质，Giotto实现了时间的可预测性，使其适用于安全关键的实时系统。Giotto系统由以下实体组成任务是基本的功能实体。任务的行为是在一些外部代码（用一些过程语言编写）中实现的。任务读取传感器（和其他任务驱动程序在任务端口和物理设备（传感器和执行器）之间复制数据驱动程序满足同步假设：它们在零逻辑时间内执行（即它们可以在环境改变之前执行）。端口是（类型化的）存储器位置，承载系统模式是周期性任务调用和执行器更新的集合，以及它们相关的驱动程序调用。每个周期性活动可能都有一个与其驱动程序相关联的保护条件模式之间的转换通过模式切换驱动器防护的（周期性）评估来启用功能（驱动程序和任务实现）以引用的形式提供178T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175外部代码（例如C或Java）。Giotto程序描述了执行任务的时间约束：任务的定义及其在每种模式下的速率，但没有明确的调度信息。Giotto编译器的任务是找到一个满足上述约束的合适的调度。2.1.1乔托建模我们已经创建了一个可视化的建模语言表示乔托程序。这个范例中的一个模型代表了一个Giotto程序，可以从三个不同的方面来看待：物理（或环境）：包含传感器、执行器和任务输出端口定义及其驱动程序。端口实体（传感器、执行器和任务输出端口）是原子元素，具有名称和类型。驱动程序被表示为模型（即容器实体），它们保存对其输入和输出端口的Tasks：容器对象，保存对它们的输入、输出和私有端口的引用模式：包含对每个周期性活动（传感器读取、执行器更新或任务调用）及其驱动程序的引用。 模式可以包含具有指定的模式切换保护条件和目标模式的模式切换驱动程序调用。Giotto例如，在Giotto中，周期性活动任务调用）频率必须是模式周期的除数(in换句话说，每个完整的调用周期必须落在模式内）。这可以通过以下约束来表达（self.parent（）->oclAsType（Mode）.periodmodself.frequency） = 0将约束表达式附加到GME中的Meta对象Periodic重新解决了自引用。Periodic是Mode的子元素，它们有整数频率和周期的属性。图1显示了来自Giotto分布的hovercraft032.2E码载表码E-code是E-machine的语言[6]，E-machine是一种虚拟机，在软件进程和环境之间进行实时交互。E-machine保证了可预测的时序和行为，并且它可以在实时操作系统上实现为轻量级虚拟机。T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175179(a) Giotto模型(b) 模型中的模式定义Fig. 1. Giotto模型tems（RTOS）。乔托的基本概念和电子机器密切相关，尽管电子机器的范围要广得多，而且不仅限于时间触发系统。E-machine定义了以下实体：任务一段应用程序级代码实现一个计算。它的执行需要非零的实时时间，可以从任务端口获取参数并将结果写入任务端口。任务可以被抢占，但没有内部同步点。司机实际上是一样的乔托司机。在E代码中，它们被指定为两个实体，一个警卫和一个司机。端口是促进任务间和任务-环境通信的存储器位置。E-machine实体与Giotto实体非常相似主要区别在于，E-code程序定义了一系列E-code指令给出的严格任务/驱动程序执行序列，而不是一组时间约束（Giotto中的模式定义）：if指令根据相关保护的求值提供条件分支。驱动程序调用调用指令执行一个驱动程序，E机阻塞直到驱动程序完成。调度任务调度指令将一个任务实例连同其相对截止日期一起移交给OS调度程序执行，并且E机继续执行。E机对调度没有进一步的控制，但它假设任务在最后期限之前完成180T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175图二. E代码元模型future指令标记了一个将来执行的E代码块。跳转分支指令以帮助代码组织（也使编码模式切换更容易）。此指令是可选的。2.2.1电子代码建模E-code的整个元模型非常简单，如图2所示：程序包含端口、功能和指令对象。端口可以是环境、驱动程序和任务端口。功能对象是任务、驱动程序和保护程序。上面列出了五种指令：if、schedule、future、call、jump。schedule是对任务实例的引用类似地，一个调用引用一个驱动程序实例，两个条件指令引用一个Guard（future也是由默认的计时器保护条件的）。顺序由Next（和Then，如果）连接提供为了得到一个更适合于未来形式验证的模型，还应该对功能对象对端口上面的元模型可以简单地扩展到包含端口访问信息-它被省略只是因为本文的不同重点与Giotto元模型类似，OCL约束可用于强制执行格式良好性规则。例如，指令对象最多只能有一个传出Next连接。（要求恰好一个确保周期性，这不是通用E代码的要求T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）1751813将乔托翻译成电子代码传统的Giotto编译器执行3个任务：(i) 验证源文件的格式是否正确（语法检查）(ii) 将功能和端口定义从Giotto映射到E-code(iii) 生成驱动程序调用和任务调用的指令序列，满足Giotto程序在我们的模型转换上下文中，i）不应该在转换级别完成，因为元模型和模型编辑器为其提供了必要的工具（编辑过程受到元模型和OCL约束的约束至于ii），由于Giotto和E-code的功能概念非常密切相关，这项任务很简单。主要问题是执行（三）。在详细介绍解决方案之前，我们简要介绍一下所使用的图形转换工具。3.1使用GReAT转换GME模型GReAT [4]图形重写引擎是GME工具集的一部分它通过匹配源图的部分和创建/删除/修改目标图的部分来操作这种转换的基本单位是规则。规则可以接收和传递对已经匹配的元素（枢轴点或端口）的引用这样，一个复杂的转换可以被分成（顺序）更小的规则。还可以通过使用规则块将规则组织到更高级别的层次结构中。还为分支提供了一个测试/用例构造过程（C++）代码片段也可以包含在规则中，作为属性操作的代码或匹配的保护条件代码通过GME的API访问模型模式元素是对源和目标元模型实体的引用这实现了强类型，GReAT识别并支持元模型中的UML概念，例如继承：例如，派生类型的对象将在指定基本类型的规则中匹配除了导入的元模型中的对象和关联之外，GReAT用户还可以将临时对象和元模型间的关联指定为交叉链接。这些对象和关联仅在执行转换GReAT转换涉及以下步骤：(i) 导入源和目标元模型(ii) 创建包含图形模式的重写规则182T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175图3.第三章。顶级块和第一规则元模型元素(iii) 使用GReAT语言结构定义（隐式和显式）规则排序(iv) 通过指定源文件、目标文件和起始规则来配置转换在下面的部分中，将给出转换的解释，突出显示重要的部分。3.2Giotto→E-code转换图3显示了转换的高级结构和第一条规则在第一个规则（E-CodeProgram）中，匹配GiottoSystem对象（包含在根文件夹中），并创建相应的E-codeProgram容器它包含一个Guard（定时器），它是每个E代码程序的一部分（由未来指令使用）。一个虚拟跳转指令也被创建并指定为最后一条指令创建另一个程序对象Tmp（将用于在转换期间存储临时对象），并使用一个AttributeMapping代码块来设置对象名称。3.2.1映射功能定义接 下 来 （ 如 图 3 （ a ） 所 示 ） ， System 和 Program 对 象 被 传 递 到AddFunctionality规则块。其中的规则将匹配Giotto模型中的所有功能定义（任务，驱动程序和端口），并创建相应的E-code实体。为了帮助进一步处理，还在相应实体之间创建交叉链接。T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175183(a) Block AddFunctionality（b）Block Giotto2ECode图四、离市中心两个街区如图4（a）所示。3.3生成顺序指令接下来，Giotto2Ecode块生成实现Giotto程序的E代码指令序列。这包括以下步骤：(i) 为每个端口（内存位置）调用初始化器驱动程序(ii) 在序列中附加一个跳转(iii) 匹配每种模式，并为其生成指令序列(iv) 设置跳转（从步骤ii开始）图4（b）中示出了该块。第一步很简单：匹配Giotto模型中的端口，找到它们关联的初始化器驱动程序（使用AddFunctionality期间生成的CrossLinks）;生成驱动程序调用并将其附加到指令链。3.3.1编译模式这个规则块是转变的核心。Giotto定时约束以以下方式给出：每个模式都有一个周期，这是一个持续时间（毫秒）。模式中的每个活动都有一个相对于此周期的频率例如，如果P周期M= 600，任务tA的频率为3，任务tB的频率为2，则当系统处于模式M时，tA必须每300毫秒执行一次（以3.33 Hz），任务tB必须以5 Hz运行（每200毫秒）。为了生成合适的进度表，必须计算基本单元大小，即各个活动期间的GCD在上面的例子中，它们是（200， 300）和GCD（200， 300）=100，因此，184T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175图五.示例E代码序列模式为100毫秒。图5中显示了实现该示例的E-Code序列：(i) 评估任务驱动程序(ii) 执行（调用）驱动程序，(iii) 将任务移交给操作系统调度程序在第一个时隙期间，两个任务都被（有条件地）调度，并且在任务运行期间，E-Machine暂停100 ms下一个100ms时隙是空的，并且电子机器等待另一个100ms。在200ms时，需要调度tB，随后在300ms时调度tA。然后，在400ms处，需要再次考虑tB500ms处的时隙为空，并且在此之后周期重新开始。后续的未来指令可以在稍后阶段进行优化。在图中，实线箭头表示指令排序，虚线箭头表示Then分支。将模式编译成E代码指令序列涉及几个额外的步骤（例如，任务调用之间的端口复制驱动程序调用）。用图形模式描述这些步骤是微不足道的，因为每个对象都映射到一个简单的指令序列上，并且它们的顺序（在同一类对象中）是不相关的。主要问题是a）计算单元大小和b）生成所需数量的时隙。一旦为每个活动确定了正确的时间段，就可以很容易地给出模式来为每个活动生成if-call-sched序列。3.3.2计算单位大小这个问题是通过在递归规则块中实现欧几里得著名的GCD算法来解决的T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175185(a)（b）GCD执行见图6。 GCD和GCD块首先，为模式M的所有活动创建活动时段集合（时段M/fi）。 这些被存储在临时程序模型中作为未来指令（使用future的integer属性）。这是在图6（a）所示的规则populateGCDList中完成的。然后，选择两个数字（a，b），计算它们的GCD，并从列表中删除这些数字，并将它们的GCD插入。实现GCD（a，b）的规则块如图6（b）所示。规则块包含对自身的引用（GCD）：这是在GReAT中实现递归的一种方式。 当不能再从容器中选择两个对象时，它终止：只有一个存在，它必须是GCD。3.3.3生成时隙的代码正如我们在图5中看到的，实现Giotto模式需要为周期/单位大小时隙生成代码。在每个时隙内，如果周期i的开始与当前时隙的开始重合，则需要生成用于ti的指令为了实现这一点，我们创建了另一个临时变量（称为Sum，类似地由ProgramTmp中的未来指令表示），在EQUEEMODE的开始（图中的规则MaintainSum6（a））。该变量表示模式的规则块AddUnits的结构如图7（a）所示AddUnits被调用，匹配（Mode，UnitSize，Prog）。AddUnitHeader创建持续时间为U nitSize的未来指令。PeriodicActions规则将匹配模式中周期开始时间与当前时隙相同的活动（以Sum形式维护）。这个匹配是由GReATGuard条件实现的，它是一个关于匹配对象属性的布尔C++函数186T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175/(a)Block AddUnits（b）测试用例NeedMoreUnits见图7。 生成时隙的规则块Guard的伪代码如下：int unitsize，时间轴，period，freq;unitsize= GCD.When（）;时间轴= Sum.When（）;period= Mode.period（）; freq= Periodic.frequency（）;时间轴-= unitsize;/*Sum 总是提前一个单位 */return（（时间轴mod（周期/频率））==0）;GCD、Sum、Mode和Periodic是对规则中模式匹配的模型对象实例的引用。如果所有模式元素都匹配并且Guard的值为true，则规则匹配。然后，子块AddUnitContent为所有匹配的活动生成if-call-sched 序列。这些序列被插入到未来指令之前，标志着时隙的结束。最后，测试用例NeedMoreUnits（如图7（b）所示）将Sum与PeriodM进行 比较。IfSum=PeriodM，（ casenotFinishe d） ， 则 将match-ing（Mode，UnitSize，Prog）三元组传递给对块AddUnits（测试用例的父块 ） 的 引 用 ， 从 而 实 现 递 归 。 如 果 另 一个 测 试 用 例 匹 配 （ Sum=PeriodM），则没有匹配项通过，递归停止。3.4翻译器生成的E-Code程序图8显示了基于Giotto发行版示例的hovercraft03模型的翻译器生成的程序。（图1显示了Giotto模型的部分内容。）由转换映射的功能对象（Guard、Driver、Task）沿顶部分组。T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175187→图8.第八条。Hovercraft03生成的E-Code程序指令序列从第二行开始，为每个端口调用然后，跳转指令指向启动（且仅）模式的开始在第三行，执行端口复制驱动程序调用，实现必要的任务输出任务输入复制，以便以后可以启动任务。这些指令在每个模式开始时运行。模式的单元0显示在第四行。 它有两个ActuatorUpdates（受保护的驱动程序调用）用于leftMotor和rightMotor。 两者的频率都是1。这些被映射到if→call序列。此外，该模式具有频率为1的任务调用（idleTask）这个任务没有驱动程序（因此没有保护），并且映射到单个Sched指令。任务气垫船。错误有输入驱动getPos，其频率为2，因此它在两个时隙中都被调度 它是第二个时隙（第五行）中唯一的活动，因为所有其他活动的频率都是1。结束最后一个时隙的未来指令指向第3行上周期的4更广泛的背景和相关研究这里描述的实验是一个更广泛的研究领域的一部分，旨在使用模型转换将高级，特定领域的语言转换为分析模型分析模型使用来自分析领域的概念，例如时间自动机和混合系统，并且可以通过模型检查进行验证。该方法在最近的一篇论文中得到了证明[7]。将高级模型转换为平台级模型（在这个特定的例子中是指令序列）是这种方法的第一步以一个明确的平台的形式精确描述这个较低的抽象层次188T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175表单模型允许进一步转换为更精确的分析模型。基于平台的设计的概念是相似的，[8]给出了一个很好的平台概念的artic-ulation。在他们的方法中，作者使用相同的建模语言（Metropolis）来描述设计中的所有抽象层。基于平台的设计的目的是在设计空间中找到最适合需求的平台实例。特定实例的属性是众所周知的，因为它是由使用良好的定义的组合规则。在我们的工作中，给出了平台，问题是映射DSML（时间触发Giotto）模型到平台级（同步，顺序 E-Code）的。在这两种方法中，平台是为更高级别层提供的HW/SW服务的集合/抽象。4.1图变换（GT）在基于UML的模型上使用GT生成分析模型是一个越来越受到关注的领域一个特殊的问题是弥合UML符号之间的语义差距（特别是）。关于动态行为）以及形式分析和验证中使用的MetaEnv工具箱[9]说明了一种通过使用HLTPN（高级定时Peti Net）语言为视觉符号分配精确语义来克服此问题的方法。另一个例子是VIATRA框架[10]。VIATRA是特别相关的，因为它旨在通过使用GT生成的分析模型进行验证和确认。在这里，元模型以UML类图的形式给出，动态语义通过由图形模式组成的GT规则来指定作为一个有用的想法，VIATRA重写规则可以包含一个可选的负面应用条件图。这在指定模式的“缺乏”方面非常有帮助，这在GReAT中可能是难以理解的VIATRA建议直接从高级模型为每个分析任务构建单独的转换。在我们的经验中，这会导致人工生成的转换代码中的繁琐重复：通常，所有分析模型都共享由DSML语义和执行平台属性指定的公共结构这个结构应该由一个明确的、平台级的模型来捕获，所有分析特定的转换都可以访问这个模型。关于GT方法的另一个问题是验证GT本身，因为分析的正确性取决于它们。这个问题是审查一般由J。 Küster在[11]中。虽然没有为这个问题提供一个普遍的解决方案，但他的结果为进一步研究提供了良好的第一步T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）1751895结论和进一步研究在解决了前面介绍的问题之后，我们可以得出结论，基于图重写的模型转换是一种可行的方法来生成满足由约束给定的调度问题的显式指令序列与传统的编译器不同，这种方法依赖于输入的格式良好性.正如我们所看到的，这不是一个问题，因为建模语言和模型编辑器能够强制执行格式良好的约束。这仍然突出了模型转换语言中使用的模式匹配方法的一个主要缺点。不匹配给定模式可能有两个原因：(i) 该模型是病态的（例如，缺少强制性实体）(ii) 模型是格式良好的，只是不包含模式要匹配找到原因可能需要使用几个额外的模式来验证格式良好性（即，每个可能的错误消息或丢失实体对应一个模式这些模式基本上重复描述相同的结构5.1进一步研究在当前形式中，翻译不支持Giotto模式切换，即系统模式之间的保护转换在E-Code中实现模式切换需要在源模式和目标模式内对齐时隙 Giotto允许相同的活动存在，即使在不同的模式开关频率，使问题更加困难。另一项任务是在E-1000上对端口访问（驱动程序/任务读写）进行建模。代码级别。这些信息可以从Giotto模型中提取，并有助于获得更精确的低级别系统模型。从长远来看，这些模型可能会被扩展以适应最近的Giotto和E-Code扩展以及当前的研究方向，例如分布式操作和动态链接。6确认NSF ITR关于作者还要感谢加州大学伯克利分校乔托团队成员SlobodanMatic的帮助190T. Szemethy/Electronic Notes in Theoretical Computer Science 152（2006）175引用[1] T. Gardner等“http://www.zurich。 ibm.com/pdf/ebizz/gardner-etal.pdf[2] L'edecziA'.， Ba kayA'. ， 我的 妈 妈 ， Vo ？lg yesiP. ， Nordstrom G. ， 小 J ， 卡尔赛 湾“Composing Domain-Specific Design Environments”，Computer，pp. 44-51，2001年11月。该工具可在www.example.com上获得http://www.isis.vanderbilt.edu/Projects/GME[3] A'。 Ba kay，E. 我是阿里。“http://www.isis。 vanderbilt.edu/Projects/mobies/[4] AgrawalA. Karsai G.， 施F. “G r a p h T r a n s f o r m a t i o n s o n D o m a i n - S p e c i f i cM o d e l s ” T e c h n i c a lr e p o r t ， I S I S - 0 3 - 4 0 3 ， N o v e m b e r ， 2 0 0 3 . 可 在http://www.isis.vanderbilt.edu上在线[5] Thomas A. Henzinger，Benjamin Horowitz，and Christoph M.基尔希Giotto：一种用于嵌入式编程的时间触发语言。在第一届嵌入式软件国际研讨会（EMSOFT）的会议记录中，计算机科学讲义2211，Springer-Verlag，2001年，pp. 166-184。[6] Thomas A. Henzinger和Christoph M.基尔希嵌入式机器：可预测、可移植的实时代码。在ProceedingsoftheInternationalConferenceonProgrammingLanguageDesignandImplementation（PLDI）中，ACM Press，2002年，第100页。第315-326页。[7] T. Szemethy和G.Karsai通用计算机科学杂志，卷。10，第10期，2004年，第1383-1407页[8] Sangiovanni-Vincentelli，A.;马丁，G.”Platform-based design and software design methodologyfor embedded systems”, Design11月6日至号决定2001年第23 - 33[9] 巴雷西湖，Pezz`eM.[10] G Y。 Csert'an，G. 胡塞尔岛 我是杰兹克，Z。 Pap，A. Pataricza和D. 好的 在J. Richardson，W. Emmerich和D. Wile Proc.ASE 2002：第17届IEEE国际会议自动化软件工程，第267-270页，爱丁堡，英国，2002年9月 23-27日[11] J. Küster，