Signal同步编程语言与Promela异步描述的混合验证方法及其在GALS系统中的应用

理论计算机科学电子笔记146（2006）105-131www.elsevier.com/locate/entcs同步分量F. Doucet，M. 梅纳里尼岛H. Kruger和R. 古普塔1加州大学圣地亚哥分校计算机科学与工程J. - P. Talpin2IRISA/INRIA法国雷恩摘要从Signal同步编程语言中描述的模块开始，我们提出了一种验证GALS系统的方法。 由于GALS系统的异步部分不能在Signal中描述，我们使用Signal中的同步描述和Promela中的异步描述的混合。Promela是SPIN异步模型检查器的输入语言。这使我们能够实现局部同步组件（Signal）的全局异步组合（Promela）。在这里，我们提出了三个关键结果：首先，我们提出了一个翻译从信号模块Promela过程，并证明了他们的等价性。 其次，我们提出了一种技术，抽象的通信总线设计的GALS，松散的时间触发架构（LTTA）总线，一个有限的FIFO通道。这种抽象的好处是提高了使用SPIN进行更大规格的模型检查的可扩展性。第三，我们证明了GALS系统在Promela中的模型的迹等价性，并给出了它的硬件实现，这使得基于Promela模型的GALS系统的验证成为可能。然后，我们使用我们的技术来验证一个中央门锁系统的GALS架构上使用LTTA的汽车关键词：规范，验证，同步语言，模型检查，信号，自旋，GALS。1Email：{fdoucet，mmenar in i，i kr ue ger，r gup ta}@ ucs d. e度2电子邮件：Jean-Pierre. irisa.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.038106F. Doucet等人/理论计算机科学电子笔记146（2006）1051引言设计包含多个内核和多个时钟域的复杂片上系统器件提出了具有挑战性的建模和验证问题。传统上，微芯片是使用同步语言开发的，这有助于降低设计验证任务的复杂性。然而，深亚微米技术的物理特性使得在计算模块之间具有可预测的通信延迟变得非常困难因此，使用这些技术的同步系统的部署很难实现时序收敛。全局异步/局部同步（GALS）架构由于在片上系统设计中使用的许多原因而具有吸引力[7]。它们提供不受通信延迟影响的异步通信然而，由于所使用的组件级验证的多样性，此类系统的建模和验证可能会很困难。在本文中，我们解决了使用Signal同步语言[4]指定的同步知识产权（IP）模块的GALS部署的验证问题同步语言提供了一种将系统指定为转换函数的方法，当进行这些转换时，可以对其施加时间约束 我们使用Spin模型检查器[8]来验证异步环境中的同步模块。 Spin已成功用于验证异步软件系统。我们决定使用Spin而不是其他模型检查器是基于它提供的两个功能：（1）使用偏序约简的异步语义的有效模型检查算法（2）在Spin模型中内联外部C函数调用的能力Spin的异步语义使我们能够有效地建模多个嵌入式同步组件的GALS集成环境我们利用偏序约减来减少GALS模型验证所需的状态空间。此外，为了快速有效地进行验证，我们可以将Signal编译器的输出（一个模拟同步反应的C函数）调用到Promela进程中（Promela是Spin的输入语言本文的贡献是在GALS架构中同步组件集成的验证方法首先，我们提出了一个从Signal模块到Promela过程的转换，并通过证明迹等价来证明我们转换的正确性接下来，我们描述用于GALS架构中的通信的松散时间触发架构（LTTA）总线。我们抽象这个总线的FIFO通道，并使用模型检查，ING证明他们的等价性。抽象增加了我们能够使用Spin验证的GALS架构的大小。使用抽象，我们可以F. Doucet等人/理论计算机科学电子笔记146（2006）105107构建并验证包含同步组件的GALS架构的Promela模型。最后，我们证明了我们的GALS模型在Promela是跟踪等效的硬件实现的GALS系统使用LTTA总线。将Signal用于规范和Spin用于验证的组合使用为GALS架构的验证提供了有效和高效的组合我们的研究结果表明，有一个可能的自动路径，可用于验证同步规范的GALS部署。本文的组织结构如下。在第二节中，我们回顾了相关的工作。在第3节中，我们介绍了计算的同步模型，以及Signal语言及其语义。在第4节中，我们介绍了使用Spin验证同步组件的验证策略。在第5节中，我们展示了验证GALS架构的方法在第6节中，我们给出了一个汽车中央锁系统的例子，并展示了如何使用我们的方法来验证系统的中心属性。我们描述了这个例子的模型检查性能统计。然后，我们讨论未来的工作，并在第7节结束。2相关工作使用IP块设计片上系统的一个核心挑战是通信延迟问题[11]。这一事实使得使用GALS架构之间的纯同步和异步实现吸引人的妥协。随着时间的推移，已经提出了许多不同的架构来将不同的同步组件连接到GALS系统中[12]。Carloni等人[6]提出了一种延迟不敏感的架构，它将通信和计算分离开来。通过特定的协议，各种同步组件在执行任何操作之前等待所有数据出现在它们的输入 在这种架构中，由于物理时钟的时序要求的问题是由称为中继站的逻辑块解决。这些块包含锁存器，锁存器插入在跨越时钟域的长通信线路上。对延迟不敏感的组件称为耐心进程。如果一个进程没有耐心，可以通过使用一个包装器来任意停止它的时钟，直到所有的数据值都出现，并在必要时锁存它们使用这种方法，组件的交互从计算中分离出来，系统可以用一种syn-tax语言来描述。然而，正如[13]中所指出的，Carloni引入的延迟不敏感方法仅限于单个时钟。如果具有不同时钟的多个系统互连，则必须插入一些延迟以减慢较快的系统以满足最慢的子系统。这种解决方案有改进的潜力，因为它降低了所有快速模块的速度。108F. Doucet等人/理论计算机科学电子笔记146（2006）105Ramesh等人[10]提出了一个工具集，用于在片上系统架构的背景下对GALS架构进行建模和验证他们使用交流反应过程（CRP）语言，一种Esterel的方言[5]，并使用Spin验证架构为了利用异步模型检查，他们使用了CRP到Promela的直接转换在这项工作中，我们提出了一种方法，该方法建立在使用信号同步语言[2]进行系统建模的基础上。我们还使用Spin模型检查器，但我们使用总线架构抽象来提高验证的可扩展性我们通过使用论文[6]中提出的包装器和中继站来利用Carloni的工作，以实现硬件实现和Promela模型之间的等效性。3计算的同步模型计算的同步模型实现了同步假设[2][5]，该假设指出系统中的所有组件同步（1）采样输入，（2）点火，（3）写入输出。所有的反应都是瞬时的，当观察系统时，人们看到的输入与输出是同时的。从这个意义上说，同步性假设简化了概念化，因为人们不必考虑所有可能的进程交织，从而潜在地减少了系统状态空间。注意，在同步性假设中，观察者不能观察到输入和输出之间的因果关系在这种范例中可以有效地指定的系统的示例是嵌入式实时应用中使用的数据流控制器Signal [4]是一种实现同步假设的语言。它用于指定信号上的数据流方程，并将这些方程同步合成为反应系统。3.1Tagged模型Signal语义使用了一个标记模型，它等价于跟踪模型，并增加了时间注释。在标记模型中，信号由标记赋值（t，v）的序列表示，其中v是值，t是该值被采样的符号时间。这是一个序列，其中每个事件都标记有记录时间的度量。标签序列t1，...，信号s的n称为它的时钟，用s τ表示。对于信号s，根据时钟sτ对值的流进行采样。例3.1图1描述了三个信号x、 y和z.这两个帧描绘了两个不同的时序域。信号x和y属于相同的时序域：x是y的下采样，其中其事件是F. Doucet等人/理论计算机科学电子笔记146（2006）105109z：•t3···x：·t1y：·t1•t2·····Fig. 1. 多时钟行为示例：方框表示两个不相关的时序域与y上的事件的奇数发生同步，共享那些特定的标签。信号z属于不同的定时域。它的标签不是按照x，e的顺序排列的。G. xτ/≤zτ和zτ/≤xτ也不是y的所有块。x：= y$1初始化 vx：= y默认值zx：=ywhenzy：·t1 ， y1·t2 ， y2·t3 ，y3x：·t1，v·t2，y1·t3，y2y ： ·t2 ， y2·t3 ，y3z：·t1，z1·t3，z3x：·t1，z1·t2，y2·t3，y3y：··t3，y3z：·t1，1 ·t2，0·t3，1x：·t3，y3图二. 单信号方程现在让我们来说明基本信号方程的一个子集的行为。图2描述了在使用Signal编码的规范中常见的语句的行为。第一个是x：= y$1init v，首先定义x到v，然后定义y的前一个值。平等-tionx：= ydefaultz在y存在时用y定义x，否则用z定义。等式x：= y当z为真时，x由y定义。正如我们所看到的，信号时钟的当前值决定3.2过渡系统我们现在使用一个转换系统来定义Signal语言的语义定义1（转移系统）设V是定义域110F. Doucet等人/理论计算机科学电子笔记146（2006）105D. 我们将V 上 的转移系统M定 义 为元组S，T，s0，其中F. Doucet等人/理论计算机科学电子笔记146（2006）105111S：V→D是一组态，T<$S×S是一个跃迁关系，s0是一个初始态。每个状态代表变量的可能估值。 两个状态s∈S和SJ∈S是相同的，如果变量具有相同的精确值s（V）=SJ（V）。定义2（Run）设M是一个迁移系统。我们定义一个过渡系统的运行是一个有限的或无限的状态序列π = s0s1.. .运行是状态序列;跟踪是对变量子集的观察序列。这些变量可以表示输入和输出端口，而内部变量将对观察者隐藏。定义3（语言）设M是一个迁移系统。我们定义M的语言，记为L（M），是M的所有可能游程的集合。3.3信号语义我们现在准备好将Signal语言的语义及其标记模型表示为一个转换系统。Signal过程是一组基本Signal语句的结合，表1列出了它们的解释语义。Signal规格中的每个变量v由转换系统中的两个变量表示：（1）变量v用于保存数据，范围与规格中相同，（2）变量vτ用于时钟，范围在二进制域上，以指示v中存在或不存在值。在一次运行中，我们用vk表示序列中的第k个值，用vτk表示第k个时钟。表1中的报表分为三类。单时钟（多时钟或多时钟方程不要求所有信号都存在;它们的操作取决于当前存在的信号时钟关系建立了信号的时序约束;它们定义了信号的存在和不存在。3.3.1Monopoly操作同步假说假设，对于一个反应，所有的输入和输出都在同一时间出现，反应是瞬间计算的。在Signal中，monochromatic操作实现了同步假设。所有的算术运算都是单行本。陈述XτkParticipateYτkParticipateZτk，Zk：=op（Xk，Yk）表示在循环k处，通过双重蕴涵，如果输入或输出中的一个存在，则它们都存在。这意味着输入和输出信号的时钟需要相同，表示为112F. Doucet等人/理论计算机科学电子笔记146（2006）105表1Signal语言名称语法解释语义学单一业务算术Z：=XopYXτk参与 Yτk参与 Zτk，Zk：= op（ Xk，Yk）Xτ= Yτ= Zτ延迟/寄存器Z：= X$1Xτk参与 Zτk，Zk：= Xk−1Xτ= Zτ多功能手术采样Z：= U，当BBτk<$ Bk <$ Uτk参与者Zτk，Zk：= Uk选择Z：= U默认值V（UτkParticipateZτk，Zk：=Uk）（<$Uτk<$VτkParticipateZτk，Zk：=Vk）同步合成P|Q见第3.3.4小节时钟关系时钟提取Z：= XZk参与者 Xτk时钟相等X = YXτ= Yτ上界钟Z = X + YXτk Yτk ParticipZτk下界钟Z= X* YXτk Yτk参与者 ZτkXτ =Yτ=Zτ。当时钟谓词被满足并且所有输入值都存在且已知时，Zk的计算可以被触发。计算是瞬时的，并且输出值存在于循环k，并且可以用于其他同步反应。延迟操作，也是单稳态，将X的前一个值Xk−1赋给Yk。 同样，时钟是一样的，如果存在输入，则存在输出，但在这种情况下，值为延迟一个采样瞬间。这类似于同步寄存器。3.3.2Polyvinyl操作多边形运算在非同步的信号流上定义关系。时钟存在或不存在可用于在时钟用于描述特定事件的定时从某种意义上说，时钟在保护可能的多晶跃迁。第一种多边形语句是采样操作。当由信号B表示的采样条件既存在又为真时，信号Z对信号U否则，在时刻k的信号Z上，没有值Zk可用，并且其时钟Zτk为假。 当采样条件为假时，我们不关心U的存在或不存在。这又是一个F. Doucet等人/理论计算机科学电子笔记146（2006）105113双重含义因此，如果在指定Zk中的某个地方是必需的，那么输入需要存在，并且采样条件将为真。多边形的第二个操作是选择操作。在时刻k，如果Uk存在，则信号Z被赋予值Uk;否则，如果Uk不存在且Vk存在，则赋予值Vk。注意U的优先级高于V。这种操作被认为是多路复用，因为当两个输入中只有一个存在时，输出可以存在3.3.3时钟关系时钟关系用于通过信号规范定义控制流程。将条件语句（“if-then-else”）编码在接下来的两段中，我们将更详细地解释时钟树的概念以及用于编码条件时钟树表示程序中所有信号的时钟之间的关系每当有时钟出现时，树根就会滴答作响;这是最细粒度的时钟。当沿着树向下走时，每个节点仅针对根刻度的子集存在。树的构建使得规范的控制流程由控制信号的存在或不存在来描述：树中的节点是控制信号。例如，一个“if-then-else”将由两个互补的时钟表示：一个将只在采取“then-condition”的时候出现，另一个将只在采取“else-condition”的时候从根开始，这两个节点位于不同的分支上现在，让我们来描述表1中的信号语句，用于时钟关系。时钟提取语句Z：=X用于指定信号Z描述X的时钟。此语句使设计人员能够显式提取信号X的时钟，以便在条件语句中使用例如，可以在X的存在（Z== 1）或不存在（Z== 0）上附加一些动作。时钟相等的语句X= Y用于指定两个信号的同步约束。这意味着信号X和Y同时存在或不存在。The第一个，Z= X+Y，将信号Z的时钟定义为信号X和Y的时钟的上界。这实际上是两个时钟的并集，导致每当两个输入X或Y中的一个出现时，Z就出现此语句是选择操作的计时行为。第二个陈述Z= X *Y 定义了114F. Doucet等人/理论计算机科学电子笔记146（2006）105信号Z的时钟是X和Y的时钟的下限。这实际上是两个时钟的交点，导致仅当信号X和Y都存在时才存在信号Z此计时行为接近于采样操作的计时行为，不同之处在于采样语句要求第二个输入具有真值。3.3.4同步合成同步合成操作P |Q是一种多时钟操作，因为它可以是多时钟的。在Signal中，每个语句都是一个并发过程，这意味着它是一个小的转换系统.信号规范的行为是一个过渡系统，它是同步合成的。其组成部分的过渡系统为了翻译一个规范，每个语句都被翻译，然后添加到一个连接中，形成整个系统行为。这实际上是所有语句的同步组合。归纳地得到所有Signal语句的同步合成，其结果是Signal规范的转移系统定义4（合成）LetM1=S1，T1，S10，且M2=S2，T2，S20是一组变量V上的可拓变换系统. 我们将其同步分量定义为一个S，T，S0的乘积，其中S =S1×S2，T={（s1，s2）→（sJ，sJ）|<$（s1，sJ）∈T1<$$>（s2，sJ）∈T2}，且s<$=（s1，s2）.1 2 120 0 0在组合系统中，为了具有某些结果行为，P和Q共享的时钟约束和数据值必须一致。这意味着，如果两个转换系统共享变量，组合可以消除许多可能的行为。考虑到时钟是变量，必须考虑组成对时间行为的影响信号的当该关系是函数时，可以计算时钟（例如，从输入信号的状态和值开始）。该计算用于构建控制流程图并生成顺序代码[1]。使用这些时钟关系指定约束。3.4转换系统我们现在考虑将Signal规范转换为跃迁系统。回想一下，Signal程序中的控制流被编码为时钟树。这个时钟树为我们创建的过渡系统的过渡定义了一个“触发时间表”。触发时间表是系统中所有时钟关系的分层组成。每次触发一个同步反应时，时钟树都会被评估，以确定哪些语句必须被触发。F. Doucet等人/理论计算机科学电子笔记146（2006）105115在规范中，每个同步模块都有自己的本地时钟树，其根定义了模块的最一般的触发条件现在，如果我们将一个模块与另一个模块组合在一起，那么第一个模块可能必须保持空闲状态，而第二个模块则会启动。标准的例子是条件语句，它被编码为两个同步“模块”的这些模块中只有一个可以触发为了使同步模块空闲，我们扩展了语义模型，包括口吃的步骤。一个口吃的步骤表示为一个反应，在所有的信号都不存在的情况下，它向观察者呈现自己为了适应这一点，我们需要在转换系统中添加断续转换，将所有时钟变量设置为零定义5（口吃步骤）设M是一个同步跃迁系统，并且M（M）是M中的时钟变量的集合。 我们将口吃状态定义为所有变量都为零的状态。口吃步骤是进入口吃状态的过渡。因此，我们的转换系统将允许断续运行，其中模块可以执行任意数量的断续步骤。定义6（Stuttering Run）设M是一个迁移系统。M的断续运行是允许在两个状态之间采取任意数量的断续步骤的运行。我们定义每个口吃运行π s= s0，s1，，.，S2，. 等价于游程π = s0，s1，s2，. 从πs通过去除所有的断续（stuttering）状态获得。我们现在描述如何将表1中的每个方程转化为跃迁系统。图3显示了每个Signal语句的一个自动机，它描述了操作及其时钟约束。首先考虑算术运算Z：=XopY。相应的自动机有两种状态：一种用于激发反应，另一种反应处于停顿状态状态表1中的等式确保只有当所有时钟都存在时才能进入点火状态，并且只有当所有时钟都不存在时才能进入断续状态这些约束表达了这样的假设，即对于算术运算，对于环境唯一允许的行为是关于信号X、Y和Z的单调行为。在延迟操作的翻译中，自动机还将环境允许的行为限制为单调行为。 对于polymer116F. Doucet等人/理论计算机科学电子笔记146（2006）105操作，自动机也表示对环境行为的定时假设有两种可能的击发状态和一种口吃状态。可以注意到，对于延迟操作，在触发状态内部存在因果关系。在注册X的当前值之前，有必要执行X的最后一个值到输出Z的赋值;否则将丢失要存储的值由于反应是瞬时的，在图中，我们以图形方式将依赖性显示为在点火状态内采取的一组内部步骤采取这些内部步骤不会改变为下一次转换启用的时钟保护算术Z：= X op Y延迟Z：= X$1采样Z：= U，当B选择Z：= U默认值V图三. 将Signal语句转换为transition系统。 自动机转换仅 时钟约束的断言，其描述了正确的单时钟或多时钟行为的环境假设。为了正确，延迟操作需要特定的语句排序。4单个组件的验证策略在本节中，我们将解释如何在异步环境中验证单个同步组件为此，我们使用Spin模型检查器来VτkZτkUτkZ τkZ ：=UK K<$Uτk<$Vτk<$ZτkZk：=VkYτkZτkXτk<$Y τk<$Z τkZ：=op（X，Y）KKKXτk<$Z τkZτkZk：=Xk−1Xk−1：=Xk（Bk）ZτkBτk<$Bk <$Uτk<$ZτkZ ：=UK KF. Doucet等人/理论计算机科学电子笔记146（2006）105117验证组件的正确性我们首先描述Spin;然后概述如何在其环境中集成同步组件。我们讨论了同步组件与异步环境的接口问题，然后讨论了异步环境中的模型是否等效于原始Signal规范的问题。4.1自旋模型Spin模型检查器[8]用于验证分布式软件系统。使用Promela语言描述自旋模型本质上，Spin规范由一组通过通道（或者，作为特殊情况，变量）进行通信的顺序进程组成通道充当有限FIFO缓冲器。进程的主体是一系列受保护的操作。从通道读取/向通道写入、向变量赋值/从变量读取值都是动作的示例守卫是进程状态空间上的谓词，也是同步谓词。当从空通道读取或写入已满通道时，进程可能会阻塞，但共享变量访问不会阻塞进程。Spin编译器将每个进程转换为转换系统，并将每个进程组合到要检查的模型中。未被阻塞的进程可以以任意顺序执行。进程中的每个语句都可以与来自任何其他进程的任何其他语句交错在进程内部，特定的语句序列可以被强制为原子的，这意味着它们不会与其他进程的语句交织为了减少由模型检查器探索的状态空间，自旋操作器执行部分降阶[8]以移除对于观测属性在观测上相同的交织。这意味着，如果异步进程的执行顺序对于某种属性并不重要，则模型检查器将只考虑这些执行中的一个并删除所有其他等价的执行。4.2信号模块到Promela过程在本小节中，我们将描述如何将Signal模块转换为Promela进程。4.2.1同步反应对于Signal模块，Signal编译器将模块的所有Signal语句转换为转换系统，形成它们的同步产物，并生成一个可以模拟同步反应的C函数的C118F. Doucet等人/理论计算机科学电子笔记146（2006）105函数读取输入信号，计算反应并将值写入输出信号，所有这些都符合同步假设，相当于执行Signal模块的同步转换系统的单个步骤如第3节所述，信号模块通常通过关于接口信号时钟的语句来定义关于环境的假设在Signal编译器生成的C函数中，有一些代码用于检查时钟假设是否满足。C函数的返回值是一个布尔值，表示反应是否成功启动4.2.2翻译模板为了验证单个Signal模块，我们将Signal编译器生成的C函数包装在Promela进程中。该进程生成环境信号的值当将C函数集成到Promela进程中时，我们通过触发C函数并检查返回值来知道是否如果不满足时钟约束，它将重置所有信号以引入断续步骤。这样，当在环境信号上生成非法值时，该过程执行断续步骤，并且不会观察到接口信号上的任何变化1：proctype some_signal_module（）{2：loop：3：原子{4：/* 1. 输入生成 */5：/* 2. 反应：调用C代码，如有必要，可引入断续步骤 */6：/* 3. collect output */第七章：8：goto循环;第九章：图四、用于在Spin进程中包装Signal模块的翻译模板图4显示了我们用来在Promela进程中包装编译器生成的C函数的模板。同步信号模型转换为Promelaproctype。第2行的循环与第8行中的goto耦合，用于永远重复同步反应。同步反应在原子块内部仿真（第3 - 7行）。事实上，同步假说要求同时观察输入和输出。投入和产出之间没有因果关系。我们使用原子步骤来重现这种行为。实际上，我们将使用新的Promelcimc构造来观察组件的行为。这是一个布西F. Doucet等人/理论计算机科学电子笔记146（2006）105119自动机同步组成的其余部分的系统;它需要一个transition每次其余的系统需要一个。原子步骤的使用使其内容看起来像单个步骤。因此，never声明不能观察到它内部发生了什么，而只是原子步骤结束时的变量配置图4的第4、5和6行模拟同步反应。第4行生成所有可能的输入值。第5行调用Signal编译器生成的C函数，如果它返回true（意味着时钟条件满足），则将输出信号设置为正确的值;如果它返回false，则所有信号都被重置，以生成一个断续步骤。最后，当某些观察到的属性被违反时，第6行打印信号配置以生成错误跟踪。4.2.3语义我们现在使用一个转换系统来描述Promela流程的语义。Spin将向转换系统添加一些变量，以强制执行Promela转换器的语义。例如，每个proctype都有一个与之关联的进程标识符此外，还将添加一个名为exclusive的全局变量来强制执行原子步骤语义。proctype将Promela过程定义为一个自动化过程M=V，T，s0。在翻译中，显式程序计数器（pc），唯一进程标识符（pid）和名为“exclusive“的全局变量“从图4的第3行开始的原子块被转换为一个转换，其中exclusive被分配给pid。这样，没有其他进程可以与原子部分交织。这用于模拟同步反应是瞬时的。在第4行，输入生成是使用非确定性转换实现的。这样就建立了一个模型的环境，关闭系统进行模型检查。环境模型可以为反应生成任何可能的输入组合。在第5行，通过调用从Signal编译器获得的C函数来调用反应如果函数返回false，我们需要重置输入和输出值以产生一个断续的步骤。这是因为输入生成步骤没有满足同步过程关于环境的假设。如果函数返回true，则意味着反应正确触发。在第6行有一组打印所有信号值的语句。如果有必要，这些用于打印反例他们是120F. Doucet等人/理论计算机科学电子笔记146（2006）105SSSpSpp在验证运行中忽略当离开第7行中的原子部分时，该进程重置独占变量设置为0，允许任何其他进程交错执行。在这个模板中，人们只能在原子截面之后观察反应。这意味着观察者将同时看到输入值和输出值，并且在没有额外信息的情况下将无法推断因果关系如果环境产生有效的输入，那么观察者将同时观察输入和输出该模板可用于对信号模块的LTL属性进行模型检查这是我们在Promela翻译中实现的同步假设4.3描述的等同性在本小节中，我们利用观测等价性证明了Signal模与Promela过程的等价性[9]。我们表明，第一个是迹等价于第二个，因为我们考虑确定性系统，等价性是合成的LTL属性。定义7（迹等价）设M1和M2是具有相同字母表的两个迁移系统. M1和M2是迹等价的，记为M1<$M2，如果它们有相同的语言：L（M1）= L（M2）。在我们的例子中，跟踪等价意味着可以在Promela进程和Signal模块上观察到相同的由于Signal模块的模型包含在Promela进程中并从Promela进程中调用，因此证明是通过构造进行的。我们将Promela过程和Signal过程上的观察者定义为与各自模型同步组成的让我们将V表示为信号处理的接口的输入和输出信号的集合我们将信号观测器定义为一个在V上的转移系统Os，如果它能观测到任何可能的在V上的运行，如果。观测器Os与Signal模块的转换系统同步组成，并在每个同步反应后进行观测，对输入和输出进行采样。我们定义V，如果作为Promela信号模块中对应于Vif的进程这些是Promela过程的可观察输入和输出，对应于信号模块的接口我们在Promela过程上定义一个观测者Op作为一个过渡系统如果它能观察到任何可能超过V的情况。观察者Op是与Promela工艺同步合成，同步反应后观察实际上，观察者无法观察原子部分内部，因为它被表达式：exclusive==0或exclusive==保护着。F. Doucet等人/理论计算机科学电子笔记146（2006）105121SpSpppppSp观察者PID，并且变量我们现在可以陈述下面的定理。定理m4.1对于Signal模及其Promela平移，LetMs= S，Ts，s0ε和Mp=Sp，Tp，sp0 ε分别是一个系统.让O s成为V的观察者，如果在Ms上， Op是 V，如果在Mp上，让L s和Lp分别是他们观察的语言。 则以下成立：Ls= Lp，并且根据定义7，Ms相对于Os和O p <$MP。证明草图：这是一个证明的建设。这两个观察者用相同的字母表观察可观察的事物。事实上，我们可以定义一个双射函数其从Vif中的信号映射到Vif中的值/时钟对。因此我们可以将两个观察者的观察映射到相同的字母表。根据定义，观察者Os可以观察Signal模块的任何合法行为。只有当“proctype”执行到达图4的第8行时，观察者Op才能观察到V中对的配置这是因为“exclusive”变量保护O p的每个步骤，使得当“proctype”在原子块内执行时，保护为假（“exclusive”变量被设置为包含原子指令的“proctype”的进程标识符，并且当块结束时重置为0）在图4的第4行中，如果可以生成。 在执行第5行之后，如果要么是信号模块的有效信号配置或断续步骤。第5行调用Signal编译器生成的C函数。此函数是确定性的，如果提供正确的输入，则返回true并模拟Signal程序的正确反应。如果输入配置不正确（不满足时钟树），则返回false。在后一种情况下，所有信号时钟都被设置为0，从而产生断续阶跃。第6行的执行不会修改Vif。通过构造，第6行只是打印输入和输出变量的当前状态，以提供错误跟踪。(This仅在Spin中重放错误跟踪时发生;在验证运行期间，该行中的所有打印指令根本不执行）。我们证明了观察者Op可以观察到Os观察到的任何词。所有输入都在第4行中生成在行5之后，如果生成的输入信号与时钟树一致，则Vif的配置与Vif相同，并且p s因为第6行没有修改它，所以当Op进位时，这在第8行仍然成立从他的观察。假设在任何时候都可以生成所有可能的正确输入，则s∈ L（Ms）=s∈ L（Mp）。我们现在证明观察者Os观察到Op观察到的所有词：s∈ L（Mp）=s∈ L（Ms）。在第5行之后，我们有相同的配置：如果和V如果或者是Vif的一个结巴的步骤。在第3.4节中，我们扩展了Vp122F. Doucet等人/理论计算机科学电子笔记146（2006）105同步过渡系统，以允许口吃的步骤。在一个断续运行中，我们可以添加或删除无限数量的断续步骤。因此，Op观察到的所有单词都可以被Os观察到。这证明了s∈ L（Mp）参与L（Ms），从而证明了两种语言的等价性现在，给定同步合成，观察者通过构造观察到相同的Signal模块和Promela过程之间的区别是口吃步骤，但是因为口吃步骤不会改变转换系统的语义，所以我们可以说观察到的两种语言是相同的。鉴于这两个模块是迹等价的，在Promela模型上验证的LTL性质适用于信号模型。在Promela中，观察者可以使用never声明来实现。Spin将LTL属性转换为永不声明[8]，它与我们在定理中使用的观察者观察到相同的5GALS体系结构现在，我们将重点从同步模块扩展到它们的异步组合，并将其扩展到全局异步、局部同步（GALS）体系结构。我们将使用异步模型检查来枚举GALS系统中同步块的所有执行交织，以避免意外的错误行为或死锁问题。Spin模型检查器可以找出是否出现这类问题，并可以返回导致错误的执行路径（如果存在）。松散时间触发总线架构（LTTA）的使用是围绕同步计算域实现全局异步通信的一种方式[3]。我们将LTTA总线抽象为大小为1的Promela通道，并通过模型检查证明它们的等价性这种抽象将使我们能够验证更复杂的系统比可能使用LTTA的标准翻译。然后，我们表明，GALS架构模型，我们取代LTTA总线结构与Promela FIFO通道，相当于一个真正的硬件实现。5.1通信信道抽象LTTA的基本结构如图5所示。它由三个设备组成：写入器、总线和读取器，分别用上标（）w、（）b和（）r表示每个设备由其自身的近似周期性时钟激活。在第n个时钟节拍（时间tw（n）），写入器生成F. Doucet等人/理论计算机科学电子笔记146（2006）105123读者作家W值xw（n）和交替的矩阵bw（n），使得：⎧如果n= 0，则w为falseB （n）=bw（n-1）否则这两个值都存储在其输出缓冲器中，由yw表示。在任何时间t，写入器在tr（n）处，读取器将输入缓冲器yb加载到变量x（n）中。和b（n）。然后，以与交替位协议类似的方式，读取器提取x（n）当且仅当b（n）已经改变，意味着值也改变。为了证明协议的正确性，我们需要证明，在对时钟的一些假设下，序列xw和xr必须重合，即，n·xr（n）=xw（n）。xxr=xTWTRyw=（xw，bw）总线维持ybyr=（x，b）tb图五. LTTA的基本结构在[3]中，使用符号模型检查表明，LTTA协议的离散信号模型满足确保时钟一致分布的期望要求。然而，确保实际LTTA协议正确性的假设本质上是定量的（不同时钟的相对周期和时间变化的容限界限）。为了使协议正确，时钟必须是准周期性的（周期可以在某些特定的范围内变化），并且必须在某些特定的范围内相互关联为了允许使用标准的模型检查技术，需要对协议进行两种抽象。第一个是只使用布尔数据类型的总线有效载荷。很明显，这个协议和要验证的属性相对于传输的数据类型X是数据独立的因此，用X类型的有限个实例的有限个集合来验证这个协议是足够的。 这样就可以推导出任何类型X的实例化的协议的正确性。然而，在[3]中，只考虑了X通过布尔类型的实例化。第二个抽象是关于时钟的相对速率。总线必须比写入器快的条件是124F. Doucet等人/理论计算机科学电子笔记146（2006）105事件之间的排序。这是由一个断言抽象的，即在两个总线传输之间不会发生两次写入。同样，两次读取之间不得有两次总线传输这些假设被编码为环境模型中的公平条件，即。e. 读者和作者的时钟一样吗？见图6。 LTTA与大小为1的图6显示了用于验证LTTA总线等效于大小为1的FIFO总线的模型检查设置我们创建了一个读取器和一个写入器进程，并将它们连接到Signal LTTA总线模型的转换写入器进程生成数据值，将它们写入总线和FIFO，读取器进程比较值的正确性。我们在读取器进程中放置了一个断言，即读取的值总是相等的。定理5.1设ML是LTTA总线，MC是容量为1的Promela信道。假设关于用于读取器和写入器进程的时钟速率的约束保持，则M L是等价于M c的迹。验证草图：通过模型检查。LTTA总线作为黑盒被检查，以在读取器和写入器进程可能生成的也就是说，写入器在接口信号上生成每个可能的值，并且我们表明读取的值是相同的。LTTA总线内部握手的时钟假设可以通过FIFO通道的阻塞行为来建模5.2通信抽象和可扩展性优势在本小节中，我们将评论LTTA总线到通道的抽象对验证的可扩展性提供的为了研究这一点，我们创建了三个额外的跟踪等效实验，如图7（a）、（b）和（c）所示，其中我们对总线进行了流水线处理。我们在管道的末端验证系统，以证明它仍然在与FIFO管道的跟踪等价的正确性条件方面表现正确。三个实验的模型检查器的性能数字列于表2中。表中的第一个条目显示了验证单个总线与单个FIFO总线的等效性的结果，RW总线FIFO（大小1）