使用GATeL1处理状态机规范

理论计算机科学电子笔记264（2010）3-17www.elsevier.com/locate/entcs使用GATeL1处理状态机规范本杰明·布兰克a Christophe Junkea 布鲁诺·马雷aPascale Le Gallb Olivier AndrieucaCEA，LIST-软件可靠性实验室（LSL）电子邮件：cea.frbMASLaboratorypascale. ecp.frcEsterel Technologiesolivier. esterel-technologies.com摘要GATeL为Lustre/Scade程序提供了一个测试环境。它的主要组成部分是一个解析过程的基础上CLP解释其输入语言。本文提出了一种两层扩展的GATeL，以考虑到状态机的描述。此扩展依赖于将这些构造编译为多时钟表达式。 我们的第一个贡献是定义了显式约束，以管理GATeL中的时钟类型层次结构。第二个是定义反映由Scade编译模式构建的状态机属性的约束。保留字：反应式系统，状态机，测试生成，约束逻辑程序设计1引言GATeL [3，16]属于基于CLP的测试生成工具家族[2，5，11，13，19，21]。它允许为使用Lustre [7]及其工业实现Scade开发的程序生成复杂的测试序列。这种自动生成工具在应用于这些程序的认证过程（DO-178 B，IEC-61508）中具有很大的意义，并且是对现有模型检查技术的补充[4，18，20]。该语言的最新版本Scade 6 [12]体现了IC程序的一个众所周知的特性：它们分解为不同的模式。使用状态机在高级别上表示模式[15]。目前，GATeL只能通过系统布尔编码来管理这样的状态机描述[1]。由于编码隐藏了转换关系，这种方法效率不1这项工作得到了项目ANR-07-TANG-019和IRSN核安全局的支持。1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.12.0114B. Blanc等理论计算机科学电子笔记264（2010）3然而，出于代码生成的目的，Scade这个编译过程提供了一个结构，以确定状态和自动机的转移关系的时钟时钟的流水。由于它接近GATeL的输入语言，我们因此决定处理这个中间语言及其多时钟运算符。对付这些新营办商的其中一个方法，是把现有的单时钟营办商合并，以界定中电的解释。但是这种模拟也丢失了由强时钟类型提供的信息，因此不能被GATeL有效地处理。我们的主张是，利用GATeL中的时钟类型和运算符，可以解决现实的状态机规范，其中包括SCADE 6模型，但也可以从其他框图模型（例如，[6]第六章：中国的改革开放本文的贡献是双重的：首先，它描述了这些新的多时钟运算符的GA- TeL的扩展，然后它提出了一些改进的编译过程的基础上，以细化状态机的约束。我们首先在第2节介绍Lustre语言及其相关的时钟概念。然后给出了状态机和时钟程序之间的翻译过程的一瞥第3节介绍了GATeL中使用的基本机制，然后介绍了用于时钟扩展的主要更新。下一步是在第4节中定义特定的状态机演绎规则。最后，在第5节中，基于简化的巡航控制模型的案例研究证明了我们的建议与前两个解决方案相比的效率。2Lustre的状态机扩展光泽作用于流动。Lustre属于用于描述关键反应系统的同步数据流语言家族基本的结构单元称为节点，允许声明输入和输出的类型（int、real、bool或用户定义枚举类型），并为每个输出给出一个根据其定义方程计算的值反应回路的每次迭代包括读取传感器值作为输入，然后计算输出。因此，任何Lustre表达式都表示无限数据流：常数3对应于数据流（3，3，3...）， 将表达式A + B转换为多项式（A0 + B0，A1 + B1，. ）.由于Lustre遵循同步假设，因此在循环的每个时刻，所有的同步流都具有相同的长度。大多数情况下，Lustre用于对闭环程序进行建模：输出是执行器命令，这些命令将与下一个传感器值相关联。然后，有必要参考过去的值，以模拟复杂的行为。同步假设允许唯一地引用一个流的过去值：pre（X）=（nil，X0，X1，. ）.为了防止unfined nil值，这个运算符必须被初始化1保护：A->B =（A0，B1，B2，. ）.布尔值（and，≤，.）和算术（+，-，.）运算符也可用于定义输出表达式。B. Blanc等理论计算机科学电子笔记264（2010）35H不F不F不F不一a0级的1一个2一个3一个4一个5一个6Bb0的B1B2B3B4B5B6a when（ h，t）a0级一个2一个4一个6pre（ a when（ h，t）无a0级一个2一个4pre（ a） when（ h，t）无的1一个3一个5merge（ h; a when（ h，t）; bwhen（ h，f））a0级B1一个2B3一个4B5一个6Fig. 1. 时钟控制的数据流的执行跟踪。流动可以被计时。Lustre内核的另一个基本概念是它能够设计时钟额定的计算。时钟允许以一种安全的方式放松同步假设：时钟可以有不同的长度，但这种去同步化只会以有限的方式发生，由专门的操作员精确描述表1示出了计时执行。可以使用when运算符对一个数据流进行采样：Xwhen（Y，v）。当Y计算结果为v，则该表达式的计算结果为X;否则它没有值。重点-扩展了标准算子的明智应用，使得它仅适用于相同速率的卷积。时钟演算然后定义如下[10]，以便为每个表达式分配时钟类型。因此，表达式由电抗回路的连续迭代表示的逻辑时间定义了基准时钟。所有其他时钟类型都是通过采样运算符从该基准时钟导出的。采样时钟Y只允许使用布尔或枚举标识符，v是属于其数据类型的值。最后，在互补时钟（即，依赖于同一标识符但覆盖其数据类型的所有可能值）可以使用合并运算符进行重组。 还请注意，两个pre表达式：第一个仅当h取值时才计算pret，而第二个在每个周期评估pre，然后在H是T。用时钟设计控制。数据流语言的一个主要缺点是它们在定义控制结构方面提供的帮助很差。然而，大多数反应式系统需要控制结构和数据流的混合（例如，定义每个运行模式的输出的不同方程）。我们考虑自动机结构的SCADE 6版本，基于数据流的保守时钟扩展[8]，确保了两个主要的设计规则：在每个周期，只有一个活动状态和一个触发转换。一个重要的特征是状态机可以是分层的：状态体本身可以被定义为状态机。让我们考虑图2中的状态机，它用相应的表达式EA，EB，EC定义了一些输出。粗体边缘对应于强转换，即可以根据当前输入和所有先前值的条件触发的那些转换。虚线边缘对应于可以触发的弱转换，假设在当前周期内没有触发强转换，根据任何输入和输出的修订后的汇编程序首先界定了6B. Blanc等理论计算机科学电子笔记264（2010）3o=EAo=EBo=ECSel一BCA法案BB一BNxtBC一Bout EB EB EA EB图二. 状态机表示状态的枚举类型（每个状态一个枚举器）。基于这种类型的三个循环被创建以执行状态机的动态语义：在每个循环中，Sel标识可以触发强转换的状态，Act标识评估状态体并可能触发弱转换的状态，Nxt定义下一个选定的状态。在没有任何强转换的状态机中，我们因此得到Act=Sel;并且如果没有弱转换发生，则Act=Nxt。这三个流程是从状态机的结构中自动定义的。Sel= A-> pre（Nxt）;Act= merge（Sel;Bwhen（Sel，A）;Bwhen（Sel，B）;Awhen（Sel，C））;Nxt = merge（Act;A when（Act，A）;（if Sel=A thenB else C）when（Act，B）;C when（Act，C））;out = merge（Act;EA when（Act，A）;EB when（Act，B）;EC when（Act，C））;Sel被定义为第一个周期的初始状态（此处为A），否则为Nxt的先前值。Act由Sel上的merge定义，并涵盖了每个状态可能的强转换。Nxt由Act上的合并定义，并考虑在同一周期中没有强转换时的弱转换（这里仅在状态B然后，状态机的输出通过Act上的合并来定义，将所有定义表达式收集到一个表达式中。由于每个表达式都有不同的时钟，类型，时钟演算确保在一个周期内最多计算一个表达式。假设在我们的例子中所有的转换都是无条件的，那么就得到了上表的执行。3GATeL的多时钟扩展GATeL [3，16]是一种基于专用解析程序的测试工具。这个过程依赖于通过约束编程的光泽运营商的解释。管理时钟扩展的第一种可能的方法是通过单时钟前、后和后的组合来模拟when、merge、pre和->你好 例如，Xwhen（Id，v）可以模拟为如果Id=v则Xelse（def ault->preX），当其时钟从未出现时返回def ault值，并保持自其时钟上次出现以来的先前值。这个模拟在时钟的每个瞬间都精确地匹配原始表达式（同上，第五节）。然而，正如第5节所示，CLP对该模拟的解释不如直接解释这些算子有效B. Blanc等理论计算机科学电子笔记264（2010）37内部表示给定一个Lustre模型和一个可达性目标，GATeL会自动生成一个导致此目标的输入序列可达性目标被描述为布尔Lustre表达式。这个目标是使用一个专用的指令，指出达到，这可能会被添加到一个节点的身体。从一个测试描述收集模型与一个识别的根节点，和一个到达，能力目标，GATeL首先将这些元素编译成一个静态逻辑程序P=（Vars，E，R）。Vars是与给定目标相关的一组Lustre标识符，E（Id）是对应于输出或局部标识符Id∈Vars的定义方程的项，R是表示可达性目标的布尔项。 这些术语自然地建立在抽象语法之上，该抽象语法表示所有Lustre操作符和日志变量，而不是Lustre标识符。每个逻辑变量在以下域中解释，根据其相关的Lustre类型：boolin [f，t] finitedomain，int在标准的区间整数运算中。实数或双精度在其对应的有限域中，枚举类型是一种浮点区间算术或实区间算术时钟层次GATeL的多时钟扩展包括使用时钟类型的显式概念。变量中的每个Lustre标识符Id和可达性目标R具有遵循[10]的类型系统模型的闭合类型计算文件，注意到（Lustre标识符Id：cl）。时钟类型cl是基础时钟基础（表示程序的最快时钟流速率）或Lustre时钟流标识符Id（时钟类型的载波时钟流），其属于一个枚举类型，伴随着它的真值v（它所依赖的枚举数cl：：= base|（Id，v）由于时钟类型的载波频率可以定义为wrt。另一种时钟类型，这定义了一个表示时钟类型的偏序的时钟层次结构这层次H由GATeL合成并添加到逻辑程序P。 H的根是基本时钟类型。 给定表达式X和标识符Id的时钟类型cl，当（Id，v）时，X将（Id，v）设置为cl的子时钟。 该层次结构配备了两个导航功能，为每个时钟类型cl提供其唯一的祖先cl+和其子时钟cl-的集合。 对于时钟类型cl，cl.id表示其载波流标识符，cl.v表示其真值。 按照约定，base.id等于base。v.解决引擎这个程序P由GATeL的主要组件使用：它的解析引擎。这个引擎的目标是生成一个矩阵M，其行是来自变量的标识符，列是循环。对于每个已知循环C，M（Id，C）存储与Id相关联的逻辑变量，Id的域根据其类型被初始化。解析引擎根据需要创建新的循环，从而相应地扩展M作为标准CLP算法[14]，解析引擎在确定性和非确定性之间交替8B. Blanc等理论计算机科学电子笔记264（2010）3和非确定性阶段，前者由一组基于Lustre操作符定义的过滤规则管理（见第3节）。这些演绎规则涉及两个循环概念。第一个代表方程成立的当前周期C第二个是代表已知最高周期的向量CM（cl）在H中的每个时钟类型cl。周期编号在基准时钟上编制索引编号逻辑变量的第二向量存储每个最高已知周期的状态SM（cl）。一个状态变量有域[init，non init]。这两个向量对于解释->运算符很有用。滤波规则按照通常的逻辑符号Γ Δ表示。 Δ是方程的一组力偶（Eq，C），等式和循环数C; Γ包含矩阵M、两个向量CM和SM，连同由剩余三元组（Eqi，Ci，Vi）组成的S，由于信息不充分，其对（Eqi，Ci由变量Vi执行。这些三元组对应于仍待解决的约束。解析算法首先用空矩阵M和残差存储S初始化环境;基时钟的最高已知周期CM被设置为零，其状态SM是可变的。然后，它从启动的第一个确定性阶段开始其中（1）目标的时钟类型被设置为真，因为当目标被实现时测试序列结束，因此其时钟必须存在，并且其中（2）可达性目标被设置为真。这两个方程的当前周期是零，它代表序列的最后一个循环和矩阵M的第一列。循环从最后一个循环到初始循环向后编号。 确定性阶段继续进行，直到在滤波规则 请注意，当检测到不满意时，这种过滤可能会失败。然后，与标准CLP算法一样，在剩余约束中出现的变量中选择一个变量，以及其允许域中的值。过滤规则一直适用，直到达到另一个固定点。过滤规则中的任何失败都会通过回溯取消先前做出的选择。为了得到一个终止算法，序列长度的全局边界（标记为MaxC）和数值域的全局边界由用户定位当算法停止时，解（M的每个赋值都失败），这只意味着没有解在用户范围内。过滤规则过滤规则实现了Lustre操作符的操作语义根据选择策略应用规则，该选择策略从当前集合Δ中选择一对（Eq，C），然后根据Eq的右成员的首算子选择规则。当没有规则可以应用于所选方程时，将应用通用存储规则：►HEq：cl V<$FreeV ars（Eq）<$SM（cl）Γ<$（Eq，C，V）<$Δr（Eq，C）Δ店将约束（Eq，C，V）添加到Γ中的残差存储S，等待在定义为自由变量的子集的变量V的集合上发生域缩减。B. Blanc等理论计算机科学电子笔记264（2010）39等式中的变量和等式的时钟类型cl的状态。这种减少导致在Δ中引入力偶（Eq，C）。我们在续集中只介绍了时钟层次结构管理中涉及的规则。那些关于算术和布尔运算符的操作由通用CLP库（COLIBRI）管理，其他测试工具也使用[2，21]。变量规则VAR-I关注输入变量，而VAR-OL关注输出和局部变量。一个。►HId：clΓJ{（cl.id=cl.v，C）}Δr（var（Id）=R，C）ΔVAR−I►HId：clΓJ <${（cl.id=cl.v，C），（E（Id）=R，C）}<$ΔVAR−OLr（var（Id）=R，C）Δ其中rJ是r，M（Id，C）与R统一，并且时钟层次可能更新：如果（Id，R）表示H中的时钟类型，并且其最高已知周期CM（Id，R）低于C，则C成为新的最高已知周期。 以前的状态是实例化为非初始化，以便通知可以使用此信息进行的剩余约束。 然后创建新的变量以表示新的状态SM（Id，R）。由于在周期C处需要Id的值，因此其时钟类型必然存在于相同周期处。相应的方程加到Δ上。最后在规则VAR-OL，E（Id）是标识符Id的定义方程。 全球更新参数CM然后可以导致根据以下属性的级联更新：提案3.1(i) <$cl∈HCM（cl）≤CM（cl+）.(ii) <$cl∈ H，SM（cl+）=init<$（CM（cl） C<$M（Id，j）= v） r<$（X = R，CJ）<$Δ r <$（preX = R，C）<$Δ前c当只考虑基准时钟（规则PRE-B）时，增量为1，因为基准时钟代表最快的时钟速率。当参数X基于时钟类型（Id，v）时，前一个周期对应于最小周期CJ，其中，低识别器Id取真值v，并且在C之前从未未知。在这两种情况下，程序的正确初始化[9]确保了C+ 1（分别为 CJ）低于其相应时钟类型的最高已知周期当没有这种循环可以在非基本情况下找到，可以考虑两种子情况以便手术顺利进行规则PRE-N1规定，如果载波时钟流Id直到基本时钟类型的最高已知周期才在其域中包含v，则需要新的周期。 然后，在环境ΓJ中递归地调用过滤，其中CM（base）递增1，并获得新鲜状态被关联，旧的SM（base）被设置为非初始化，以便通知剩余约束。递归调用旨在处理由B. Blanc等理论计算机科学电子笔记264（2010）311在基础时钟上创建新周期用户绑定MaxC确保了此规则的有限数量的应用程序。►HX：（Id，v）i ∈ [C.. C M（base）] v/∈dom（M（Id，i））Γ J<$（preX =R，C）<$ΔΓ（preX=R，C）<$ΔPRE-N1►HX：（Id，v） CJ= min（j |j> C <$v ∈ dom（M（Id，j）Γ<${（var（Id）= RJ，CJ），（preX = R，C）}<$ΔΓ（preX=R，C）<$ΔPRE-N2规则PRE-N2调用具有新变量RJ的载波流集合的滤波过程。该等式应在大于当前周期C的最小周期Cj处成立，其中Id的域包含v。这旨在获得更多信息，以便知道周期CJ是否确实是时钟类型（Id，v）的前一周期规则INIT-T规定，如果当前周期是时钟类型cl中已知的最高周期，并且其状态为init，则滤波过程应用于其第一个参数。规则INIT-F是互补的：当当前周期小于CM（cl）时，这意味着C是非初始的。因此，过滤程序适用于第二个参数。►HX：cl SM（cl）=init CM（cl）=Cr（X=R，C）<$Δr（X->Y=R，C）<$ Δ初始化-T►HX：cl CM（cl）> Cr（Y=R，C）<$Δr（X->Y=R，C）<$ Δ初始化-F规则INIT-NB允许为基础时钟创建一个新的周期：如果第一个参数的域与周期CM的结果的域不兼容，则状态必然是非初始化。更新T以递增CM（基础）并创建新状态。这里使用序列长度的用户界限MaxC来限制此规则的应用。►HX：baseCM（base）=Cdom（X）C+1≤MaxCΓj（Y=R，C）<$ΔΓ（X->Y=R，C）ΔINIT-NB考虑到非基本情况，状态在ΓJ中被实例化为非初始化，但是最高已知周期在这里不能递增实际上，由于前一个周期取决于载波时钟的实例化，因此仅执行此更新。变量的规则。存在性前提要求X的时钟类型存在这样的前一个重要周期。这可以由一个专门的12B. Blanc等理论计算机科学电子笔记264（2010）3此处未显示约束►HX：（Id，v）CM（Id，v）= Cdom（X）CJ> C M（Id，v）s.t. M（Id，CJ）=v ΓJ< $（Y=R，C）<$ΔΓ（X->Y=R，C）Δ初始化-NC最后，规则INIT-I对应于对称情况，其中第二个参数的域与结果的域不兼容►HX：（Id，v）CM（Id，v）= Cdom（Y）Γ（X->Y=R，C）ΔINIT-I其中对应的时钟状态被实例化为在rJ中初始化。这对H中周围时钟类型及其载波时钟流的状态有许多影响。命题3.2设cl =（Id，v）为X的时钟类型。假设S M（cl）=init以下事实成立：(i) M（Id，CM（cl））(ii) <$clJ∈H，（cl.id=clJ.id<$CM（cl）=CM（clJ））<$SM（clJ）=noninit(iii) S M（cl+）= initi∈ [C M（cl）+ 1.. C M（cl+）]，（M（cl+.id，i）= cl+.vcl.v/∈dom（M（Id，i））(iv) <$clJ=（IdJ，vJ）∈cl−，M（IdJ，CM（cl））=vJ<$SM（clJ）<$init第一个属性在H和M之间建立了直接联系：当时钟状态是初始的，则其对应的载波载波必须被实例化为其真值。第二个声明，所有基于相同标识符但具有不同真值的时钟类型应在当前最高已知周期cl处实例化为non init（当它们的状态尚未在较低周期处设置为init时）。注意，对于这些时钟，还应确保规则INIT-NC的存在性假设。第三属性声明，如果祖先时钟类型cl+已经被设置为init，则对于从CM（cl）到CM（cl+）的每个周期，载波时钟流Id不应包含其真值v。请注意，这也应该由一个专门的约束。最后一个属性指出，对于cl-中的所有子时钟，如果已将循环数实例化为其真值，则应将其相应的状态设置为init，因为在这种情况下，已知的最高循环数必然相等。对于命题1，这些属性由这里没有开发的专用约束处理。例3.3再次考虑第2节中的微型状态机示例，输出输出的公式如下：EA = 0 EC = 0EB =（0 when（Act，B））-> pre（out when（Act，B））+ （1当（Act，B））B. Blanc等理论计算机科学电子笔记264（2010）313计算出的out值为：0，1，0，2，3.. . 方程EB中的采样是由Scade 6编译过程引入的，而用户只需键入状态Bout = 0 -> pre out + 1。假设可达性目标是：reachout=3，可以很容易地猜测至少需要五个周期，这可以通过以下推导得到证实。X：{v1. v k}是X的定义域的符号，我们采用约定“ 规 则 名 称 （ Δ 中 的 选 定 方程 ） " 。MER-I（out0：{3}=merge（Act;EA;EB;EC），0）在周期0引入可达性目标。 时钟标识符Act被添加到Δ以获取其域。VAR-OL（Act0=var（Act），0）引入循环0时的Act方程，其中新鲜变量为Act 0。MER-I（动作0=合并（选择;B;B;A），0）此外，时钟标识符（此处为Sel）也被添加到Δ。VAR-OL（选择0=var（选择），0）介绍周期0时Sel的定义方程。店（Sel0：{A，B，C}=A->pre（Nxt），0，SM（base））没有规则可以应用于这个等式。MER-R（Act0：{A，B}=merge然后，Act的定义项被减少，将C从其域中移除，因为它的任何分支都无法到达。STORE（Act0：{A，B}=mergeMER-R（out0：{3}=merge类似地，out的定义项被简化为一个分支，因为其他分支（EA= 0，E C= 0）与结果3不相容。MER-S（3= 0when（Act，B）-> pre（outwhen（Act，B））+ 1when（Act，B）， 0）然后用结果3探索合并的剩余分支。初始化-NC（3 =pre（outwhen（Act，B））+ 1，0）结果与最初的情况不一致。 时钟状态SM（Act，B）被设置为非初始化，并且其C M还没有增加。存在假设和命题1允许我们将C M（基）设 为1. 然后探索正确的成员。PRE-N2（2=pre（outwhen（Act，B））， 0）对于时钟类型（Act，B），找不到过去的周期。然后，Act的定义在周期1传播，这是Act未知的最小周期。滤波过程的固定点在这里没有完全描述，因为它在Act、Sel、Nxt和时间规则的方程的传播之间进一步交替，直到它推导出基础时钟上存在五个先前的周期4编译状态机上一节中定义的约束捕获了状态机构造的整个语义，如第2节的Scade 6编译过程所定义的。然而，为了优化分辨率算法，可以在两个级别添加一些特定的规则：时钟层次和滤波规则。时钟层次和状态机当应用于状态机转换时，时钟层次用于表示状态机的层次结构。每个状态与两种时钟类型相关联，其载波流是选择状态（Sel）和激活状态（Aid）。14B. Blanc等理论计算机科学电子笔记264（2010）3状态（Act），真值就是这个状态。重要的一点是，对于给定的状态机，所有这些时钟都出现在时钟层次结构的同一级别此外，时钟层次结构包含与嵌套状态机一样多的级别命题1和命题2中陈述的性质因此在推导过程中被广泛使用我们建议加强这些命题，以使过渡函数和时钟层次之间的直接联系。给定一个状态机（I，S，T），其中I是初始周期，S是状态集，T是定义允许从一个状态到另一个状态的转换的转换函数，下面的属性声明初始状态I的最高已知周期和状态与其祖先时钟的周期和状态相同。命题4.1给定一个选定的状态标识符Sel，设cl I=（Sel，v I）是对应于状态机初始状态的时钟类型，cl+H中的祖先时钟。 以下成立：（C M（cl I），SM（cl I））=（C M（cl+），S M（cl+））。在前面的例子中，这个命题可以用来在应用规则INIT-NC时递增时钟类型（Sel，A）的CM。时钟类型的CM之间的偏序关系可以扩展，当一个时钟类型的反域T-1态v是单态vJ：令{vJ}=T−1（v）;则CM（Sel，vJ）≥CM（Sel，v）。状态机约束第3节的规则没有考虑在编译过程中创建的三个变量（Sel、Act、Nxt这些关系主要来自两个主要的设计规则：一个单一的活动状态和每个周期一个单一的转换。 例如，如果下一个状态变量被实例化为给定的状态v和同一周期的活动状态是不同的状态vJ，则选定的状态在该周期必须等于vJ，允许在M.实际上，所选择的状态不能被设置为不同的状态vJJ，因为在vJJ和vJ之间已经触发了转换，从而违反了第二个主要规则。因此，我们建议在系统中添加一个专用约束，称为sm将这三个变量与给定的周期联系起来。此约束由VAR规则管理：每当基于活动或所选状态为时钟类型创建新周期C时，都会启动此约束在这些规则中，XC是M（X，C）的捷径。dom（N xtC）dom（ActC）=SelCActC sm（NxtC，SelC，ActC）dom（ActC）dom（SelC）=ActCNxtC sm（NxtC，SelC，ActC）dom（ActC）：=dom（ActC）（dom（N xtC）dom（SelC））sm（NxtC，SelC，ActC）B. Blanc等理论计算机科学电子笔记264（2010）315国对关闭STDBY残疾F不FEn.中断F不不Reg.对不FFStdByFF不从到条件Dis.En.En.Dis.对关闭Reg.Int.Int.Reg.制动恢复制动对StdByStdBy对Accel速度限制€（加速器速度限制）图三. Cruise示例的状态、输出和转换。5为例我们的案例研究是基于同一状态机的三个实现之间的比较。第一个，称为Cruise I，实现了这个例子的非层次版本，只有布尔和单时钟时态运算符，遵循之前的Scade 5编译过程。第三个是Cruise III，它使用Scade 6工具来描述状态机，以及第2节中的预编译过程。第二个，Cruise II，是一个代码代码重写第三个，通过使用模拟来替换多时钟运算符，单时钟的。所有这些版本在考虑其输出时具有等效行为呈现案例研究是巡航速度控制器的分层版本，它取决于五个布尔输入：制动（踩下制动器），加速（踩下加速器），恢复（从中断恢复），速度限制（速度太慢或太快时为真），开和O（启动/停止请求）。我们的模型由三个嵌套的状态机组成，每个状态机有两种状态：控制器可以是禁用或启用;启用时，第二个自动机可能处于中断或调节状态;第三个自动机定义了两种计算模式，即处于调节状态时，打开或待机。在每个周期，根据其活动状态，控制器计算三个布尔输出：ON，OFF和STDBY，如图所示。3 .第三章。在分层表示之后，Cruise II和Cruise III版本在每个周期有四种可能的状态。这导致对于MaxC个循环，至少4个MaxC个可能序列的搜索空间。另一方面，Cruise I版本在每个周期有六个可能的状态，在至少6个MaxC可能的序列中搜索。覆盖目标。我们建议在我们的设置中通过可达性目标来编码经典的[17]覆盖标准：（1）覆盖所有状态，（2）覆盖所有转换对，以及（3）覆盖模型的所有布尔输出，即获得其中ON、OFF和STDBY至少一次被设置为真的序列。图4显示了每个实现为给定目标生成测试序列所需的平均时间（超过100次执行），MaxC设置为4。Cruise III实现使用了本文中描述的所有功能，显然是最有效的16B. Blanc等理论计算机科学电子笔记264（2010）3见图4。覆盖分辨率时间（ms）的比较。图五. 最大C值增加时的反驳时间（ms）比较。产出覆盖范围跃迁对覆盖Cruise I Cruise IICruiseIII23456789 10 11 12 1314 1516 17安全目标。第二类目标是达到一个不安全的状态，由不可能的输出组合定义。由于在这种情况下没有解决方案，因此不会生成序列。序列长度的界限MaxC逐渐增加，以说明每个实现的行为。图5显示了Cruise I版本的不良行为，这当然最好由适当的SMT来处理解算器 相反，Cruise III版本的响应时间几乎立即且随最大C线性变化。在这两者之间，Cruise II版本的响应时间随最大C成二次方变化。Cruise II和Cruise III版本之间的主要区别来自于过滤规则和解析算法。这种时钟类型提供的指导方针通过丢弃不适当的时钟类型的状态和转换来显著地修剪搜索空间。6结论我们在本文中提出了一个CLP解释的多时钟内核的最新版本的SCADE 6语言。这种解释使用时钟层次结构作为一个全局结构来执行强大的演绎。案例研究表明，一个简单的编码的多时钟操作符的语义不提供这样的演绎能力。此外，如第4节所示，这种解释可以通过Scade 6编译过程确保的特定属性来改进。这里介绍的GATeL的扩展目前正在SIESTA项目的背景下进行更 GATeL的先前单时钟版本提供了基本机制来帮助定义使用定义的测试选择标准[3]。必须扩展这些机制以管理多时钟上下文。此外，来自状态机的数据流解释的见解可用于简化基于状态机的标准的定义。进一步的工作涉及到另一种转换的处理，即那些在进入状态时重置状态行为的转换。如[8]所述，重置条件可以 异步触发，因此需要对同步设置进行全面修改CruiseICruise IICruiseIII020040080010001200 14006000100002000030000400005000060000B. Blanc等理论计算机科学电子笔记264（2010）317引用[1] 定义并将Simulink/State流的“安全”子集转换[2] Bardin，S.和P. Herrmann，Structural Testing of Executables，in：ICST，2008，pp. 22-31.[3] 布兰克湾 和B. Marre，GATeL中光泽描述的测试选择策略，ENTCS111（2005年），第页。93-111[4] Bouali，A.和B. Dion，基于模型的开发的形式验证，载于：汽车工程师协会，400 Commonwealth Dr，Warrendale，PA，15096，USA，2005年。[5] Bouquet ， F. ， B. Legeard 和 F.Peureux ， CLPS-B ： A constraint solver to animate a Bspecification，STTT6（2004），pp. 143-157[6] Caspi，P.，A. Curic，A.迈尼昂角Sofronis，S.李文，“基于Simulink的分布式嵌入式系统设计与实现”，清华大学出版社，2003年。[7] Caspi，P.，D. Pilaud，N. Halbwachs和J. Plaice，Lustre：一种用于同步系统编程的声明式语言，POPL，1987，pp. 178比188[8] ColaPillacco，J. -L. 、B. 帕甘和M。 Pouzet，AConservativeExten sionofSynchronousData-taowithState Machines，in：EMSOFT，2005，pp. 173-182.[9] C olaPillacco，J. -L. 和M. Pouzet，TypebasedInitializationAnalysisofaSynchron ousD atatatowLanguage，STTT 6（2004），pp. 245-255[10] Colaco，J.L. 和M.Pouzet，Clocks as First Class Abstract Types，in：EMSOFT，2003，pp.134-155。[11]Collavizza，H.，M. Rueher and P. van Hentenryck，CPBPV：A Constraint-Programming Frameworkfor Bounded Program Verification，CP，2008，pp. 327-341[12] Dormoy，F. X.， SCADE 6：基于模型的安全关键软件开发，在：ERTS，2008年。[13] Gotlieb，A.，B. Botella和M.鲁赫，使用约束求解技术的自动测试数据生成，在：ISSTA，1998年，pp. 53比62[14] Ja Padar，J.和J。-L. Lassez，约束逻辑编程，在：POPL，1987，pp.111-119[15] Maraninchi，F. 和Y。R′emond，Mode-automata：Aboutmodesandstatesforreatives sstems，in：职工持股计划，1998年。[16] 马雷湾和A. Arnould，Test Sequences Generation from Lustre Descriptions：GATeL，in：ASE，2000，pp. 229-239[17]O Besutt，J.，S. Liu，中国粘蝇A. Abdurazik和P. Ammann，从基于状态的规范生成测试数据，JSTVR13（2003），pp. 25比53[18] 佩斯，G.， N. Halbwachs和P. Raymond，符号抽象模型中的反例生成-检查，国际期刊软件工具技术转让（STTT）5（2