嵌入式系统反应式规范设计流程及执行契约的影响

理论计算机科学电子笔记203（2009）121-135www.elsevier.com/locate/entcs嵌入式系统增量原型的可执行契约莱昂内尔·莫雷尔1INSA Lyon，LIESP，Villeurbanne，F-69621路易斯·曼德尔2LRI，Universit'eParis-Sud11，CNRS，OrsayF-91405INRIAFuturs，ProVal，Orsay，F-91893摘要在本文中，我们提倡一个无缝的设计流程，嵌入式反应式程序。我们特别关注假设担保合同（作为非确定性规范的一种形式）的使用，并介绍如何将其用于早期执行反应性规范。 我们说明的方法，从航空电子应用的案例研究，试图显示这种模拟方法的影响在设计上-流程。关键词：反应式系统，假设保证合同，早期执行，嵌入式系统1介绍反应式系统和同步方法如[11]所定义的反应系统，其特征在于与环境的交互是其行为的突出方面。嵌入在飞机、核电站或类似物理环境中的软件就是一个典型的例子。他们与一个非协作的环境互动，这可能会强加自己的节奏：它不会等待，也不会重新发布事件。同步语言[2]对反应式系统的编程做出了重要贡献。 它们都基于同步假设，该假设建立了系统的不同组件之间的通信是瞬时的，更重要的是，组件执行的计算从其这一工作部分是由作者在Verimag，G i`eres，Frannc e进行的。1电子邮件：lionel. insa-lyon.fr2电子邮件：louis. lri.fr1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.03.030122L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121HP环境的观点。在这些语言中，最重要的是ESTEREL[3]，LUSTRE[8]和SIGNAL[15]。它们提供了强大的形式化语义和相关的验证工具，现在通常用于高度关键的工业控制系统的设计原型和仿真一般来说，在软件工程中，对系统日益复杂的一个答案是完整设计流程的定义。这些描述了系统开发中的不同步骤，并将这些步骤中的每一个步骤与一些非正式或正式的方法相关联，以帮助在开发时验证系统。交互式方法包括从早期原型到最终产品的连续路径。 这种设计流程中的每一个新步骤都可以自动化，或者可以在连续的版本之间检查至少某种形式的一致性。这种方法的一个重要验证特征是使用模拟技术，通过该技术，开发人员可以观察系统在其当前开发状态下的可能行为，而无需手头上的完全实现无缝设计流程和增量验证在这项工作中，我们的目标是提出一个正式的无缝设计流程的反应系统。这个想法是能够在开发生命周期内尽快开始验证系统。通过验证，我们的意思是模拟，测试或验证，虽然在这里介绍的工作，我们集中在模拟方面。就仿真或测试而言，我们目前所能做的就是在系统完全实现时（即当它描述完全确定性行为时）测试系统。这种方法是黑盒测试的经典方法.在那里，我们假设测试系统的可执行版本的存在，并对环境进行非确定性描述。我们也可以提供观察者来检查系统是否满足期望的属性，只要环境满足系统这种此外，这是一个整体的方法：我们所要执行的测试是整个程序的可执行版本。当然，也可以在独立的组件上执行一些单元测试，即使整个系统还没有实现。但这只是对系统的部分（甚至非常小）理解。此外，还需要为每个组件指定一个有意义的环境。在早期的工作[19]中，我们提倡使用本地规范（通过假设保证合同）来帮助在开发过程中描述系统。 合同可以用作 渐进式描述方法：程序员可以首先描述系统的全局结构。然后，他可以通过为每个组件编写一个契约来描述通过逐步细化，他可以更精确地描述每个组件L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121123V V VV实施.这些契约还可以通过一些用于将证明目标委托给验证工具的验证规则来帮助对系统的全局理解[18]。早期模拟就模拟而言，在设计方法学中引入契约具有以下含义：1）模块化。一旦程序员提供了一个带有契约的组件，这个契约可以被看作是组件环境的规范，因此可以单独用于测试组件，而不依赖于整个系统的实现。这里，可以使用[22]中提出的标准测试方法，其优点是测试的局部性（整个系统不需要完全实现，以测试其组件之一）; 2）早期模拟未完全实现的系统。由于合同是在开发的早期阶段给出的，因此可以在不等待设计完整实现的情况下模拟系统。在这里，我们的目标是提供一个模拟框架，遵循后一种观点。该方法是基于生成的实际代码的确定性组件和连接到一个约束求解器（如在经典的测试方法中使用），用于模拟假设担保合同。论文内容第2节介绍了LUSTRE语言的一个子集，我们将使用它来描述我们正在运行的示例。第三节介绍了一个系统实例。通过这一点，我们说明了渐进的设计流程，我们前面介绍。从3.1中对应用程序架构的一般描述开始，我们通过给出某些组件的契约和最终确定性实现来逐步细化系统的各个部分（3.2）。第4节介绍了组件的形式化，并描述了我们提出的模拟确定性和非确定性组件网络的方法。第5节描述了这个框架的一个简单实现，它使用了现有的工具，并讨论了提出的实际问题。第6节讨论了相关工作，第7节总结并介绍了未来可能的工作。2迷你光泽我们首先定义一种用于编程反应式系统的语言。它是LUSTRE语言的一个精简版本[8]。程序操纵变量列表。 给定两个这样的列表和J，我们使用J作为和的连接J. 我们会用这个 描述我们的运行示例。程序迷你LUSTRE程序是元组N=（Vi，Vo，Vl，F）：124L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121i1C1o1i3C三O三I4i2C2o2预V VV| |||DVFV V V V VV∈ V≥•Vi、Vo和Vl是输入、输出和局部变量的成对不相交的变量列表。 它们在定义域D中取值;•是从o&l到Exp（i）的全函数&O&1），其中，Exp（ ）是在中的变量上的表达式的集合，由以下语法定义：e：：=c x op（e，.，e）pre（i，x）N（x，...，x）。c表示on上的常数;x表示i或l中变量的名称&&;op表示任何组合运算符;pre（i，x）表示变量x的先前值（其中常数i是执行初始时刻的表达式的值）;N（x，...， x）表示对程序N的调用，其中变量名作为对应于N的输入的有效参数。用于示例的通常的具体语法如图所示1.一、IoFig. 1.LUSTRE的抽象具体语法node.图二、一个数据流网络的例子在本例中，我们还将使用卢斯特雷运营商， 称为迭代器，在[21]中引入的，可以看作是有限的高阶算子。语法映射N，n定义了应用于n的节点N的映射操作。 元素数组。red N，n定义了一个reduction（类似于函数式语言中的fold），它在n个元素的数组上迭代节点。在目前的工作中，我们只使用这些迭代器来使示例的呈现更清晰。踪迹语义在迷你L USTRE程序中，每个变量名v都描述了其类型的值的一个序列，即无限序列v0，v1，.。.给定一个输入序列，即值vn，对于每个vi和每个n 0，我们描述如何计算程序的局部和输出流的序列（或迹）：对于所有时刻，输出或局部变量v的值根据F给出的定义计算：n>0。v∈Vo&Vl. x∈Vi&Vo&Vl.vn= F（v）[xn/x][xn −1/pre（i，x）]和v0= F（v）[x0/x][i/pre（i，x）]。我们取表达式F（v），其中我们将每个变量名x替换为当前值xn，并将pre（i，x）的每次出现替换为前一个值xn−1（除了在执行的初始时刻，我们将其替换为相关的初始化表达式的值i）。 这将产生一个表达式，其中运算符应用于常数。我们得到的用于定义所有时间上的时间流的值的方程组必须是非循环的。节点N（类型>的输入的列表Vi）返回类型>的输出的列表Vo）var类型>let的局部变量的列表Vi- -对于每个x，本地或输出：x =F（x）;电话L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121125××PreviousResChannels3输出值4 相同的物理设备3 x 4连接，每个连接由2根线材（共4 x 3 x 2个输入图三.陀螺系统及其环境。同步合成图四、 一轴结构组件被安排在一个数据流网络中，如图1所示。 二、 组件之间存在两种连接：组合（例如i3和o1之间）依赖关系，通过“线“连接和非组合依赖关系（例如i 4和o 2之间）使用语言中提供的pre运算符显式表示 我们要求同一个组件的输入和输出之间的任何循环依赖都被一个前操作符打破。该约束允许更简单的分析技术（例如，用作SCADE工具中的标准）和LUSTRE节点的单独编译。3例如3.1一般列报在本文的其余部分，我们将使用一个常见的例子来达到我们的目的。该应用程序来自航空电子工业，涉及飞机位置变化的处理。 图3描述了该系统，它的物理环境。该系统连接到四个陀螺仪，每个陀螺仪测量沿三个轴的角度变化，即滚动，俯仰和偏航。 由每个物理设备针对一个轴获得的值沿着两条线vA和vB被传输到计算系统。因此，系统接收4 32个值。 从这24个值中，它计算出三个安全值， 作为飞机位置变化的参考三个轴的行为是相同的。 让我们只集中在一个轴上，比如说滚动。 该系统的内部结构如下（见图2）。4）：它由四个通道组件组成，每个通道组件负责两根导线，vA和vB（表示相同的物理值）来自四个陀螺仪之一。每个通道提供一个由滚动值定义的输出值，辊间距偏航resChannels信道信道通道选民预故障容忍系统4对价值观AxisValue126L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121本地故障状态。表决器根据当前故障条件计算四个信号值（resChannel）中的一个信号值（AxisValue）：该值是未声明自己“故障”的通道传输的值的平均值。 三或者多个信道同时发生故障的概率应该非常低。这是由传统的容错分析，这不是本文的主题该系统处理两种故障：链路故障，这是由于测量设备和计算机之间的物理链路的一些不良行为;和传感器故障，这是由于测量设备（传感器）本身被打破或不正常工作一段时间。每个通道将其在两条线路（vA和vB）上接收的值进行比较，并能够检测局部差异。这种从一个陀螺仪到计算机系统的双重传输值是为了检测链路故障。对于要报告的误差，在超过Δt的时间单位内，两个值必须相差超过Δ此外，为了支持传感器故障，通道相互交谈并交换值，以便每个通道都可以将自己的值与其他三个通道进行比较。 如果其中一个陀螺仪不工作，它提供的值可能会与其他三个设备提供的值不同。 通道还必须交换它们的失败状态，因为每个通道都应该将其值与其他通道的值进行比较，但仅限于那些没有声明自己失败的通道（回想一下，由于它执行的本地比较，通道可能会声明自己失败）。当然，在系统的描述中应考虑故障检测后的恢复。但这不是所提出的工作的主题，我们将不进入这个细节。3.2设计-实践我们提出了一个设计流程，我们大致分解为三个步骤：架构设计，局部规格的描述和组件的实现建筑设计在第一步中，用户定义应用程序的全局架构即组件输入/输出接口及其连接。这正是我们在3.1中所做的。例如，我们将以下LUSTRE接口提供给组件通道：节点通道（previousResChannel：有效的通道104; nbInChannel：int;inChannel：无效的通道104）return（nextResChannel：Valid ReselT）;当地规格第二个设计步骤是通过设计假定担保合同来[19]每一个组成部分。契约是一对（A，G），可用于描述组件的部分行为。A用于编码组件对其环境的假设。G用于编码组件保证的属性L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121127它的行为。 在实践中，假设和保证都可以表示为 [9]观察者的观察。 A涉及组件的输入，并且G涉及该组成部分的输入和输出我们的Channel组件具有由节点assumeChannel和assumeChannel定义的合约（参见图2）。5）。每个通道假设最多有1个其他通道报告本地差异，并且正常工作的通道提供的值与某个理想值相差不远 当置于满足此断言的环境中时，通道保证一些时间属性，其声明：“ 要 么 检 测 到 局 部 差 异 （ 这 意 味 着 它 作为 输 入 接 收 的 两 个 值 在 太 长 的 时 间 段 内 太 不 相 同 ） ， 要 么 没 有 检测 到 局 部 差 异 并 且 当 前 输 出 值 与 它 作 为 输 入 接 收 的 两 个 值 相 距 不远 。”在节目中，Fig。5，此行为由布尔变量normalProp表示。注意，我们还需要一个初始化属性，因为保证依赖于一些在执行的第一时刻不可用的过去值。通道的全局保证是通过在then（initProp，TIME，normalProp）期间调用node来编码的，它声明initProp在第一个TIME时刻保持（TIME是一个常数），然后normalProp在其余的执行中保持。 也可以为选民设计一份合同，但我们不会给在这里，出于明显的空间原因。环境我们还描述了整个应用程序的环境，以便能够进行模拟。最简单的环境env将表决器计算的AxisValue作为输入，并将一些通道输入返回给通道。描述这样的环境是应用程序设计的一个复杂部分，但我们在这里不集中讨论它。我们将假设这样的描述以以下形式给出例如，LUCKY自动机[13]随机选择满足环境所需规格的通道执行最后一步是通过编写确定性地定义其输出的实际LUSTRE组件来完成的（与contracts所暗示的不确定性相反）。投票人（图）5）实际上计算由不声明局部差异的那些通道4仿真方法学我们现在给出一个与语言无关的反应组件的形式定义。首先，我们提出了一个正式的语义组件，包括deterministic组件和假设保证合同。然后，我们给出了我们的模拟方法的总体思路。128L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121VVD∈ V D∈ VVVVnodeassumeChannel（previousResChannel：有效的通道数（4）;nbInChannel：int; inChannel：无效的通道数（4）return（assumeOK：bool）;varunfailedChannels notFarFromIdeal：bool;让assumeOK = NbcodeFailures（previousResChannel，nbInChannel）3和unfailedChannels notFarFromIdeal;unfailedChannels notFarFromIdeal = NotFarFromIdeal（previousResChannel，nbInChannel，ideal，delta to ideal）;电话node_channel_channel（previousResChannel：Valid_valid_valid_channelT;nbInChannel：int; inChannel：Valid_channelT;–nextResChannel：有效的路径104; outChannel：有效的路径104）bool（）;varlastValidChannel：FavoriteProp;initProp，normalProp：bool;让normalProp = outChannel.local failure或（（abs（（lastValidChannel.valuea-outChannel.local value））=delta）和（abs（（lastValidChannel.valueb - outChannel.localvalue））= delta））;initProp= outChannel.local故障或（（abs（（inChannel.valuea-outChannel.local value））=delta）和（abs（（inChannel.valueb - outChannel.local value））=delta））;int findDuplicate（int findDuplicate）;int maximum= maximum（maximum，maximum，maximum）;电话nodeVoter（resChannels：ValidChannels）returns（vote：int）;varsum，nbValid：int;letnbValid=countValidChannels（ resChannels ） ;sum=redaddIfValid;4（0.0，resChannels）;vote=（globalSum/nbValid）;电话图五. 定义通道组件的契约和表决器的实现。 注意delta，ideal和delta to ideal是全局常数。4.1变量、赋值、跟踪、组件我们从一组变量开始，在一个域中取它们的值，旨在表示动力系统的状态。一个反应系统的语义给出的步骤关系。直观地说，阶跃关系涉及的两个估值，旨在表示两个连续时刻的估值。然后我们在阶跃关系之上定义分量变量可以是类型化的。然而，我们忘记了类型化机制，这必然是描述阶跃关系的语言所特有的定义4.1V的赋值σ是从V到D的全函数;让我们用Vals（V，D）表示所有这样的赋值的集合。则V上的阶跃关系涉及赋值，因此它是Vals（V，D）×Vals（V，D）的子集。V上所有阶跃关系的集合是Step-Rels（V，D）=P（Vals（V，D）×Vals（V，D））。定义4.2阶跃关系R第一章（ 、）被称为是确定性的（分别） reactive）反应性：<$σ∈Vals（V，D）. |≤1（分别| ≤ 1 (resp. ≥1）定义4.3Traces（）是变量的所有可能迹的集合。如果t轨L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121129迹（ ），我们将t i记为t的第i个元素，即在执行的第i时刻，根据t.130L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121V V∈ VV DVVV V ∈ VV DV∈ V D VVV∈ V D ∈ V DV↓|||∈V |∀ ∈ V∀若t∈Traces（V）且VJ <$V，则迹TJ∈Traces（VJ）是t在er上J（tJ=tVJ）i f且仅当 t=tJ， XJ，n，tn（x）=tnJ（x）. 此操作可以提升到轨迹集。定义4.4A行为B行为（ ）是一个tuple（ 、l，σ，R），其中是表示行为界面的变量集合。l是局部变量的集合，使得和l是成对不相交的。σVals（l，）是变量的初始值，RStep-Rels（l，）是描述其初始化后的行为的阶跃关系。定义4.5行为B=（，l，σ，R）在V的变量上的迹集方面的语义定义为：T（B）={t∈迹（V&Vl）|t0=σ_n。0< n<|不|<$（t（n −1），tn）∈R} ↓V现在我们可以定义一个组成部分的概念，它将包含假定担保合同。定义4.6分量C是元组（Vi，Vo，Ba，Bg），其中：•i和o是compo的输入和输出的集合（成对不相交）。nent;• Ba行为（i）（分别 Bg行为（i&o））是对断言的描述（分别为保证）的组成部分。定义4.7由其合约描述的组件的语义被给出为迹集T（C），定义为：T（C）={t∈迹（Vi&Vo）|t↓Vi∈T（Ba）<$t∈T（Bg）}一个行为B∈Behaviors（ViVo）D是一个组件C=（Vi，Vo，Ba，Bg）的实现，T（B）T（C）.4.2执行组件前面的语义为我们提供了确定性组件以及假设保证契约的指称特征。从模拟的角度来看，我们需要一种方法来描述满足这些规范的值的轨迹的生成。 实际上，我们需要能够通过一些函数initC（）、computeOutC（）和updateStateC（）来描述组件C，这些函数可用于构建这些跟踪。这些功能的具体实现取决于每个组件的形式。对于确定性组件，它们通过源代码的经典编译获得。然而，从全局的角度来看，我们需要确保单独汇编各组成部分。为此，我们要求，如前所述，源代码中的所有依赖循环都被pre打破。从假定担保合同来看，这种对应关系就不那么微不足道了。computeOutC（）函数的算法如图6所示。该断言可以被视为L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121131VVVV在输入值的每个时刻都应该检查的约束。因此，我们定义了一个布尔函数checkAssert（），它获取组件的输入变量的当前值，并检查这些值是否满足它所表示的约束。这个测试函数可以被编译出来，并在组件被激活时使用。断言的非确定性方面在这里被放在一边，因为它不用于实际生成值。如果违反断言，则应向用户发送警告消息。否则，如果断言被满足，则可以使用保证来生成有效输出。现在合同的担保部分基本上代表了io变量的一组约束条件。实现对应的computOut（）函数意味着提供一个函数choose（），给定i的值，通过求解约束条件i，将为o提供一个值。当然，不可能从每个合约中编译出这个选择函数。相反，它是由一个约束求解器实现的，每当从相应的合同中请求一个步骤时，该约束求解器就被要求求解一个约束。解决这些约束一般是不可判定的。在实践中，选择功能可以委托给测试用例生成工具，该工具能够解决数值变量上混合布尔和线性关系的约束。由于我们要求这种方法是全自动的，它自然需要对要解决的数值约束的性质进行限制。例如，我们在实际实验中使用的Lurette工具（见第2节）。5）要求这些约束是线性的：它使用多面体来解决这些约束。系统环境的描述以非确定性自动机的形式给出，该自动机可由前面提到的测试用例生成工具解释。我们也可以将其表示为提供computeOut（）函数的反应式组件，该函数的实现是对上述函数choose的调用。因此，从模拟的角度来看，环境将被视为另一个组件4.3执行组件网络现在，我们能够将函数computeOutCj（）和函数updateMe emCj（）与每个组件Cj相无论组件是否是确定性的，我们在编写仿真算法时如何考虑它都没有区别如前所述，唯一的区别是实现computeOut的方式我们的目标是能够模拟组件网络，例如 的fig。二、 要解决的问题是确定这样的网络中组件的执行顺序。这是按照[10]中提出的方法完成的。为了便于展示，我们假设该顺序是索引上的自然顺序首先执行C1，然后执行C2，依此类推。然后，相应的简单模拟算法如图所示第七章将这种模拟技术应用于我们的运行示例将产生如下跟踪：132L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121见图6。（A，G）组件的ComputeOut函数。inChannel[1].vA.五点三八五点二五四点七七inChannel[1].vB.五点四七四点五三四点七一.inChannel[4].vA.五点二四五点二八四点九四inChannel[4].vB.四点六五四点八一五点四三resChannel[1].<1，5.41><1，5.20><1，4.73>。. ..[4]vote见图7。仿真算法图8中的一个。图八、陀螺仪应用的可能痕迹5执行为了说明这些命题，我们使用语言REACTIVE ML（RML）[16]和LUCKY[13]实现了第3节的示例。系统的模拟是由于REACTIVE ML编译器和Lurette工具之间存在的连接而执行的[12]。LUCKY语言和Lurette工具LUCKY是一种专用于描述反应式同步程序环境的语言。它被设计成以紧凑的方式表达测试场景的序列。它的主要特点是允许非确定性和概率描述。它是Lurette工具的源语言，该工具执行测试序列的自动生成。它将环境的一个LUCKY描述、要测试的程序的一个可执行版本和一个描述作为输入。要检查的属性的程序。 Lurette处理布尔值，但还有环境描述的数字方面ReactiveMLRML是一种为实现反应式系统而设计的语言。它将Esterel中的同步范例与异步设置中的经典功能（例如动态创建进程）相结合。 它是建立 在OCAML之上，因此受益于其表达能力。 RML的一个扩展最近已经开发出来，其中一个可以描述一个特定的组件在LUCKY的行为。这个扩展最初被设计为允许RML程序描述非确定性环境。所使用的机制如下。 在每一个时间点，执行RML代码。 在执行LUCKY环境时，RML程序调用Lurette工具，以便为环境生成新的输出。环境的非确定性方面的解决完全委托给Lurette。在报纸上，对于j，1..initi（i）;while（true）对于j，1..intfindDuplicate（）;对于j，1..nbComponentsUpdateStateCj（）;如果选中Assert（）choose（）;return（）;...<5.21><5.20><4.98分. . ....5.165.144.95...L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121133保持程序的LUSTRE表示，为了不引入太多的符号，但是从LUSTRE到RML的转换应该是自动的。使用RML和Lucky我们使用LUCKY来描述组件的非确定性行为，而不仅仅是环境。每对（A，G）的LUSTRE节点形成一个合同已被翻译成两个等价的LUCKY程序。 第一个用于检测违反组件断言的输入值。如前所述，第二个用于生成有效输出。然后，RML被用来描述确定性组件（从LUSTRE版本的翻译是手工完成的）和应用程序的全局架构。从这个程序中，RML编译器生成一个可执行文件，基本上实现了fig的整个算法。第七章可执行文件还实现每个确定性组件（每个确定性computeOutCj被编译成实际的可执行代码）。对于每个非确定性组件（由合约描述），此代码包含对Lurette工具的系统调用，实现表单检查、断言和选择的调用。评论整个系统可以用LUSTRE来描述。在这里，我们受益于工具之间现有的联系。将LUSTRE契约转换为LUCKY自动机并不是一个显而易见的过程，这里是以一种特别的方式进行的。应该研究这种翻译的完全自动化。在一般情况下肯定会出现限制6相关工作在实时反应式系统的背景下，围绕仿真进行了大量工作。最重要的可能是Ptolemy[5]中实现的那些，这是一个用于设计异构系统的工具集。 在[6]中特别描述了这种类型的系统的模拟。在[24]中，针对同步无功系统的特定情况提出了一种仿真方法。这种方法的一个重要缺点是，它提出了一种确定性系统的模拟方法，因此不能在开发的早期阶段使用，因为我们建议这样做。 在[20]中，Metzger和Queins提出了一种方法，用于从正在设计的应用程序的非正式需求中生成确定性原型。需求首先被翻译成SDL [1]，非确定性从SDL程序中编译出来（多亏了一组预定义的SDL库）。 正如作者自己所指出的，这种方法的主要困难在于自然语言需求和SDL正式规范之间的语义差距。在这里，我们并不声称要填补这个空白。相反，我们的建议站在一个非常不同的地位，因为我们不编译一个可执行文件从非确定性规范，但我们真正模拟他们。更接近我们的方法，但针对不同类型的应用程序是Co-Java方法[4]。Co-Java是一种扩展134L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121在Java中，系统行为的某些部分可以使用对程序变量的约束来表示。在模拟时，这些约束以类似于LUCKY在我们的情况下所做的方式进行解释。 最后，这项工作可以看作是尝试提出[23]中提出的工作的方法学影响。在那里，作者提出了一个任意同步数据流网络的模拟框架，其中不确定性组件直接用L语言表示。我们的方法仅在所使用的语言方面有所不同（我们使用假设担保合同，这是L的严格子集）。可以使用完全相同的模拟算法（在Lurette中实现的算法）。我们有兴趣在基于合同的设计流程中定义这些模拟技术的特定用途。也许，这项工作的一个有趣的扩展将是允许描述的合同的夫妇的L组件。7结论和展望我们已经提出了一个反应式嵌入式系统的非确定性组件可以与完全实现的一起描述的模拟方法。确定性组件被编译为标准的可执行文件，而非确定性组件由其合约描述，由标准测试工具解释。这种方法的主要优点是它可以在开发的最早阶段使用，这可以节省通常在实现级别上花费在错误检索上的大量工作。程序本身及其所有组件可以根据开发阶段的不同详细程度进行描述在这个例子中没有显示，但是插入额外的输入生成器或观察器是很容易的，这些输入生成器或观察器不是系统本身的直接部分，但可以在其开发中提供显着帮助。这些可以被描述为LUSTRE节点或观察者，然后可以以相同的方式进行模拟。从这个意义上说，这种方法似乎很有希望。整个方法已被应用到本文中所描述的例子与ad-hoc变换技术。它已被完全重写在RML的手和翻译合同到他们的幸运对口也是手工完成。尽管如此，这最终还是很有希望的：我们能够模拟系统的部分定义版本，这使得在设计过程的早期发现了几个功能，这可能会节省以后的开发时间。然而，模拟对这个特定示例的全局验证的影响受到了一定的限制，因为我们之前运行的应用程序版本已经达到了非常稳定的状态。从这个意义上说，将这种方法应用于一个全新的案例研究将非常有益。我们仍然想在几个方面进一步推动它第一个是工具支持。如前所述，从LUSTRE到RML的转换是手动执行的。我们希望自动化翻译或直接在LUSTRE工作。我们更喜欢的一个想法是将LURETTE工具的使用集成到像LUDIC这样的调试器中[17]。更重要的问题涉及L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121135所用语言的表达能力。首先，我们想扩展这种方法来考虑的概率部分的幸运。这是一个在测试中被证明非常有用的特性[23]，我们相信它应该被纳入我们的框架。 这就意味着找到一种表达这些概率行为的好方法， 作为合同。第二是将这种方法从纯同步系统扩展到GALS（全局异步，局部同步）系统。从语言的角度来看，看看我们的契约如何用于指定GALS系统（使用[7]的工作作为基础）是很有趣的。我们将研究我们的模拟方法在这些系统中的应用。引用[1] Specification and Description Language （ SDL ） ， ITU-T Recommendation Z.100 ， InternationalTelecommunications Union（1999）.[2] Benveniste，A.，P. Caspi，S.爱德华兹，N。Halbwachs，P. LeGuernic和R. de Simone，Synchronouslanguages，12 years later，Proceedings of the IEEE（2003）.[3] Berry ， G. 和 G. Gonthier ， TheESTERELsynchronous programming language ： Design ， semantics ，implementation，Science of Computer Programming19（1992），pp.87比152[4] Brodsky ， A. 和 H. Nash ， Cojava ： A unified language for simulation and optimization ， in ：OOPSLA194-195.[5] Brooks，C.，E. A.李，X。Liu，S. Neuendor Schlider，Y. Zhao和H. Zheng，[6] 埃文斯，B.，A. Kamas和E. Lee，使用托勒密（1994）。[7] Halbwachs，N. 和S. Baghdadi，异步系统，见：EMSOFT'02（2002年）的报告。[8] Halbwachs，N.，P. Caspi，P.Raymond和D.Pilaud，同步数据流程序设计语言LUSTRE，Proceedings of the IEEE 79（1991），pp. 1305-1320。[9] Halbwachs，N.，F. Lagnier和P.Raymond，同步观测器和反应系统的验证，M。尼瓦特角Rattray，T. Rus和G. Scolo，编者，第三届国际代数方法论和软件技术会议，AMAST[10] Halbwachs，N.，P. Raymond和C.李文，从数据流程序生成高效代码，第三届国际程序设计语言实现与逻辑程序设计研讨会，北京，1991。[11] Harel，D.和A. Pnueli，“On the Development of Reactive Systems”，Springer-Verlag New York，Inc.，1985年，pp. 四七七四九八[12] Jaime，E.， Thelu rettev2userguide，Technicalreport，Verimag，CentreE′ quation，38610G i`eres（2004）.[13] Jaegal ， E. 和 P.Raymond ， The lucky language reference manual ， Technical report ， Verimag ，CentreE′quation，38610G i`eres（2004）。[14] Jaime，E.，P. Raymond和P. Baufreton，lurette v2的案例研究，见：ISoLa 2004，第一届形式方法的杠杆应用国际研讨会，塞浦路斯帕福斯，2004年。[15] Le Guernic，P.和A.Benveniste，同步语言信号，在：M。R. 巴巴奇，编辑，第二届大颗粒物质主义研讨会论文集（1987），pp。56比57[16] 曼德尔湖和M. Pouzet，ReactiveMl，a reactive extension to ml，in：ACM International conference onPrinciples and Practice of Declarative Programming（PPDP136L. 莫雷尔湖Mandel/Electronic Notes in Theoretical Computer Science 203（2009）121[17] Maraninchi，F.和F. Gaucher，Step-wise + Algorithmic Debugging for Reactive Programs：Ludic，adebugger for lustre，in：AADEBUG[18] Maraninchi ， F. 和 L. Morel ， Arrays and contracts for the specifi