C-TILCO时态逻辑的组件集成验证

理论计算机科学电子笔记116（2005）241-252www.elsevier.com/locate/entcs使用C-TILCO验证组件集成为例P. Bellini P. Nesi D. Rogai1Dipartimento di Sistemi eInformaticaUniversit`adegliStudidiFirenze Firenze，ItalyVia S. Marta 3，50139 Firenze，Italy，电话：+39-055-4796523，传真：+39-055-4796363摘要时态逻辑通常用于指定和验证属性以及需求，以描述系统并证明这种形式化是否满足预期的行为。本文考虑C-TILCO时态逻辑。C-TILCO是TILCO时态逻辑的扩展，提供了组合和通信原语。TILCO系统规范可以直接用作实现，因为它们可以通过使用TILCO执行器直接实时执行。验证阶段可以应用于单个组件及其集成，以验证整个解决方案。在这篇文章中，一个关于通信系统规范的案例研究，以及从验证阶段获得的一些重要属性证明。关键词：形式规范语言，一阶逻辑，时态区间逻辑，实时系统，时态算子，定理证明器，验证，组件集成，通信系统。1介绍实时系统的具体化意味着采用具体的形式化模型来定义事件和动作之间的时间约束[6]，1这项工作得到了意大利大学和研究部在COFIN 2001项目“Quack：新一代集成嵌入式系统质量平台”框架内的1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.080242P. Bellini等人理论计算机科学电子笔记116（2005）241[1]、[7]。这些形式化方法通常用于描述不变性，事件之间的优先级，周期性，活性和安全条件等属性。为此，使用了几种时态逻辑[1]，或定时状态机，Petri网等。当指定的系统不是平凡的时，其指定需要通过将问题分解为更小的部分或组件来执行，以解决特定的子问题[10]，目的是获得整个系统进行组合。采用组合模型进行系统规范必须得到用于验证组件和组合系统的形式化方法的支持[9]。验证是通过对系统的操作描述使用模型检查方法来执行的，在其他情况下，验证是通过验证形式组合以及组合行为来执行的。本文提出的方法是基于TILCO（时态逻辑与组合运算符）和它的组合版本称为C-TILCO。请注意，TILCO中的C是指构成时态约束的缩写。TILCO为从过去到未来的时间提供了一个统一的模型，以及用于沿时间轴陈述事实和事件的唯一运算符[8]，以及扩展的时间运算符（TILCO-X）[5]和过程通信支持（C-TILCO）[4]。C-TILCO的进程通信允许通过将其分解为多个进程来指定复杂系统，并且允许对它们之间的进程间通信进行建模。TILCO语言可以直接执行，这种可执行性在于使用规范作为实时系统的实现，从而允许（在每个时刻）基于当前输入（包括与通信有关的输入）和内部状态在线在这个意义上，TILCO执行器，在[3]中提出，可以执行TILCO规范的片段。本文介绍了一个案例研究，其中C-TILCO已被用于规范和验证。C-TILCO允许描述（i）架构中涉及的每个过程的内部属性和（ii）适合组件正确交互的外部属性2C-TILCO概述C-TILCO中的系统规范是通信过程组件的层次结构，其规范是用TILCO编写的。TILCO是一种逻辑语言，可以定性或定量地描述时间约束[5]; TILCO公式的含义是针对当前时间给出的。时间是离散和线性的，P. Bellini等人理论计算机科学电子笔记116（2005）241243−是整数的集合。最小时间间隔对应于一个时刻，当前时刻由0表示，正（负）数表示未来（过去）时刻。TILCO中的基本实体是时间间隔，其边界可以分别使用方括号（“["，“]”）或圆括号（“（“，“）”）的常用符号来包括或排除。基本的TILCO时态运算符是：• “• “怎么样？“，在时间间隔上的存在性量化;• “until”,或者，它将为真，直到另一个谓词变为真;• “TILCO已经扩展到提供一些更具表达力的操作符，从而创建TILCO-X语言[5]。动态间隔允许使用取决于TILCO表达式的边界来定义间隔。例如，A@（0， +B]断言A为真，因为下一个时刻到B从现在开始第一次出现的时刻;这样的时刻包含在表达式中。类似地，像B这样的边界指的是B在过去最后一次出现的时间。在C-TILCO中，相同过程组件规范的许多实例可以安排在全局架构中。进程可以有一些参数，每个实例都有自己的不同值。进程之间的通信连接是1：1，每个输出端口最多连接到一个输入端口，反之亦然。C-TILCO过程的外部特征在于：一组外部输入端口，用于从外部获取信息;一组外部输出端口，用于向外部生成信息;一组外部变量，用于提供有关过程状态的一般信息或简化外部行为规范;一组外部参数，用于允许一般过程规范，以便使过程重用更容易，因为不同的过程实例可能具有不同的参数;一组外部TILCO公式，通过交换的消息和外部变量的约束来描述外部过程行为。C-TILCO的内部特征在于：一组C-TILCO子过程;一组内部输入端口，用于从子过程获取信息;一组内部输出端口，用于向子过程发送信息;一组内部变量;一组内部TILCO公式，用于描述过程的内部行为。244P. Bellini等人理论计算机科学电子笔记116（2005）241¬子进程的端口可以直接连接到包含进程的端口（相同类型，输入到输入和输出到输出），或者可以通过通道连接到互补的内部端口（输出到输入和输入到输出）。内部端口的使用允许部分分解的实现，当进程行为仅部分由子进程指定时，因此，与子进程的一些相互作用通过内部指定的TILCO公式来表示。在TILCO公式中，点符号用于访问过程组件。由于系统中可能有许多相同过程的实例，因此它的规范对所有实例都有效。通过将冒号运算符应用于流程组件，可以在规范中轻松区分流程和局部变量由于在TILCO中，时间轴在两个方向上都是无限的，因此没有一个时刻可以被视为执行过程的开始时刻。在系统规范中，当过程开始工作时，自然会考虑参考时刻：在此之前，所有信号都是稳定的。因此，每个进程都引入了一个布尔变量进程启动对于每个进程，此变量仅在一个时刻为真应该注意的是，每个进程都有自己的开始时刻，内部规范的公式用于定义其子进程的开始时刻。通常，当一个进程启动时，它的子进程也会启动。通信原语C-TILCO提供同步端口，这些端口上的基本操作符是：Send（！！）并接收（？？）：！！[];; 通过输出端口发送通过计算表达式获得的值。当通信结束时，TILCO表达式被断言。在等待时，断言时间表达式。？？[];; 等待来自输入端口inPort>的消息（如果尚未到达）<。当消息到达时，TILCO表达式被评估为接收到的值的函数。在等待时，表达式被断言。操作员：outP！在P？已经被引入以指定进程不必在端口上发送消息或者进程不必请求消息。这些条件不能通过使用（inP！！[2019 - 05 - 15][2019 - 05-15][ 2019 - 05 - 05][2019 - 05 - 05][2019 - 05][2019 - 05 - 05][2019 -05][2019 - 05 - 05][2019 - 05][2019 - 05]P. Bellini等人理论计算机科学电子笔记116（2005）241245一一一通信通信通信节点节点节点BBBBBB通信通信通信节点节点节点一一一3使用C-TILCO指定通信协议下面的案例研究展示了C-TILCO如何帮助基于组件的体系结构的形式化验证。所述系统是基于众所周知的协议的通信系统。通信系统由若干节点组成，这些节点以环形结构连接（见图1）。Fig. 1. 通信系统这种通信基本上旨在对单个节点故障具有鲁棒性，并在节点上均匀地分配通信优先级提供了两个同心环：主环，其中信息沿着元件传递;以及备用环，其恢复主环故障连接并允许执行通信直到系统被恢复。主环标有字母A，备用环标有字母B。输入和输出端口。 通信系统节点正确连接的结果。固定的信息（称为令牌）由每个节点接收并转发到相邻节点。如果一个节点需要传输一个数据，它等待令牌，然后它传输数据在保持令牌的同时，发送到相邻的消息，并且当发送的消息返回到发送方时，它释放令牌。一个节点在超时后识别出故障通信，并且它重定向在主环的相反方向上工作的备份环该系统是根据通信节点实现的;在每个节点上，通常连接更高级的通信接口。这些节点仅执行简单的数据通信和协议管理。令牌被认为是布尔型的，并且通过专用通道传输。消息被视为包括源节点ID和目的节点ID的结构化类型。数据通信结构如下：246P. Bellini等人理论计算机科学电子笔记116（2005）241structDATAPACK{int srcID;int dstID;char data[MAX_LENGHT];}3.1系统要求节点主要执行以下操作：• 它等待令牌;• 当接收到令牌时，可以在环上传输数据而不释放令牌，否则必须沿节点链转发令牌• 如果相邻节点不应答，则它必须在反向工作的备份环上重定向相同的信息（令牌或数据）• 当发送的数据从环返回时，节点释放令牌，以便允许另一个节点发送它们自己的数据。• 在备份信道上接收的任何数据都必须在没有任何检查的情况下被重传，如果相邻节点不重放，则仅将其重定向到主环上。3.2通信节点节点必须确保通信，并应特别注意令牌传递。当在节点上观察到错误行为时，必须授予基本令牌传输以保持通信活跃。为此，将节点系统分解为子系统。图2中示出了分解的通信节点，并且其呈现了三个子系统：• 通信管理器：它获取令牌并在主环上执行通信协议;• 令牌转发器：当令牌到达通信节点时，将令牌转发到下一个节点，供备用环使用;• 数据中继器：像令牌中继器一样，它只是处理数据。主要组件是通信管理器，其规格由几个部分组成，以确保更好地理解它们的含义。P. Bellini等人理论计算机科学电子笔记116（2005）241247inData outDatasendDatasendTokenrecDatarecTokenrecTokenBackrecDataBacksendTokenBacksendDataBack图二. 通信节点的分解下面的TILCO-X规范表达了在通信管理器内部传递的基本令牌。：readyF或T oken=dd：recT oken？？[<$：readyF orT oken<$$>：transmantAnything];;（<$：readyF orToken（：dataBufferEmpty（：transmitten oken any. ：transmittData（any））@[0，+：readyF or Token））（：getDataBuf fer（%d）（：transmittData（d）transmittT oken）@[0，+：readyF orToken）当节点进程启动时初始化的“就绪”谓词将系统置于等待接收的状态。当节点等待令牌时，它不能传输任何东西（既不能传输令牌也不能传输数据）。当令牌到来时，有两种不同的选择：重新传输令牌或传输从inData端口缓冲的数据关于数据传输，要求规定新数据从较高层输入端口接收，并将其存储在特定缓冲器中，直到节点抓取令牌。在该方向上的异步通信用于避免环形通信中的任何不必要的延迟时间：以这种方式，直到需要时才抓取令牌，也就是说，当有数据要传输时。使用非空缓冲器和抓取的令牌，可以开始传输，如以下公式中所指定的。 必须考虑一个简单的规则，即每当主环出现故障时，在备用环上提供令牌（或数据）重定向。sendingToken（或send- ingData）断言传输尝试开启（直到节点在成功传输之后从相邻节点接收到ACK信号）。因此，超时条件可以计算为：<$：reset@（−（（：sendingToken：sendingData）@（−10，0]），0）重置：brokenChannel通信管理器发送数据返回发送令牌返回recTokenBackrecDataBack令牌中继器数据中继器248P. Bellini等人理论计算机科学电子笔记116（2005）241在接收到令牌之后发生的令牌的传输由以下公式指定：：transmitten okenmusician. ：transmittData（any）= 0：transmittAnything up（：transmittT oken通道：brokenChannel）=dd<$：readyF或T okenB@[0，+：brokenChannel]：sendT oken！！[sendingToken：readyF or T okenA];;<$：sendingT oken@[0，+（：transmittT oken<$：repeatToken））：readyF or T okenA：transmittAnything up（：transmittT okenA：brokenChannel）=dd：sendT okenBack！！[<$：readyF or T okenB];;：readyF或令牌B 发送任何内容：readyF orT okenA选项：readyF orT okenB选项：readyF orT oken下面的表达式指定transmitData（d）激活后的行为。因此，节点必须将数据d传输到相邻节点（这与先前描述的令牌传输非常相似up（：transmittData（d）：broken Channel）=dd<$：readyF或T okenB@[0，+：brokenChannel]：sendData！！d[sendingDataString：readyF or T okenA]; ;<$：sendingData@[0，+1next. （：transmartData（next）：repeatData（next））：readyF or T okenA：transmantything up（：transmartData（d）：brokenChannel）=dd：sendDataBack！！d[<$：readyF or T okenB];;：readyF或T okenB：transmission任何内容在这些公式中，使用备用环来恢复在中断的信道上的失败的通信尝试;如果两个信道都中断，则节点不能再通信。两个不同的谓词可以在一个可用信道上成功传输后确定就绪状态（readyForT okenA，readyForT okenB必须注意的是，中断的通道将冻结发送状态的端口，永远等待远程同步。传入数据的管理也采用类似的结构。进程初始化将系统的所有接收端口置于等待状态。因此，为了完成指定，引入了指定谓词来断言在激活相应谓词之前不会发送数据或令牌。初始化表达式如下：：process start= 0：readyF或Token：readyF或Data：repeatAnything：readyF or T oken返回：readyF or DataBack返回<$：sendingT oken@（−∞，+（：transmittT oken<$：repeatT oken））<$<$：sendingData@（−∞，+ ∞d. （：transmittData（d）重复数据（d）））P. Bellini等人理论计算机科学电子笔记116（2005）241249DD其他子组件在本文中没有描述;这些部分的规范通常重用来自通信管理器的公式，并且它以不太复杂的行为引入不同的功能以帮助组件重用。4验证规范为了证明单个过程级别和整个系统的属性，可以使用为C-TILCO和TILCO-X定义的推理规则。这里报告的验证只是整个验证的一小部分为了证明单个过程的性质，必须考虑以下两个定理：► tp！！v[Ws]; ;Ps► t直到0PsWs你好吗？[Wr];; Pr► tv. 直到0 Pr（v）Wr这两个定理允许在目标的前提下用弱直到算子代替发送/接收在用来证明连通过程性质的定理中，RWait算子起着重要的作用。它总结了通信状态，说明过去是否收到过消息，但尚未确认。这两个主要定理如下：► tin. R等待我|= out → in我|= out → in► tin？？ [W r];; Pr► t+tsout！！v[Ws]; ;Ps► tin？？@[t s − d，0）ts−d<► tP r（v）► t+dPs► tW s@[t s，d）► tout！！@（t s，d）► t +1 in. R等待► tin？？ [Wr];; Pr► t+tsout！！v[Ws]; ;Ps► tin？？@[t s − d，0）► tout！！@[−d，ts）−d≤ts► t+ts+dPr（v）► t+ts+2dPs► tW r@[0，t s+d）► t+tsWs@[0， 2d）► tin？？@（0，t s + d）► s in！！@（0，2d）► t+ts+d+1in. R等待这意味着在左侧定理的前提下：如果两个端口以延迟d连接，则在时间t断言接收，并且在接收之前的ts时刻断言发送。在左侧的含义中：消息在时间t被接收，Ps在d个时刻之后为真，发送的等待公式从发送时刻到通信时刻的结束为真，并且在t+1处RWait为真，说明没有消息待决。250P. Bellini等人理论计算机科学电子笔记116（2005）241¬∞∧ ∃右边的定理处理相反的情况：当没有待处理的消息时，发送在接收之后或延迟之内完成通信节点的令牌/数据传输的安全性可以证明为单进程级。readyForToken预测不能与令牌/数据的传输尝试（transmittT oken和transmittData）一起断言。这可以表述为：：process start =（：readyF或T oken（<$：transmittT okenany. ：transmittData（any）@[0，+∞）它可以转化为：：process start=进程开始=进程：readyF或进程：transmitAnything：readyFororToken<$：transmitAnything=< $：transmitAnything@[+：readyFororT oken]这可以通过使用规范来证明。此外，从该结果可以导出安全性属性：令牌和数据不能同时传输（B@[0，+））。这可以表述为：：process start=进程开始=进程开始（：transmitten oken进程开始。：transmittData（any））@（0，+∞）为了证明不能满足这样的临界条件，采用了一种类似于初始归纳的策略来分支主要目标：：process start= 0：readyF或T oken：readyF orT oken=（<$BAD）@（0，+：readyF orT oken]其中BAD=：transmittoken any。：transmittData（any）断言坏条件。 第一部分是从规范中琐碎地衍生出来的。第二种方法需要进一步分离动态区间末端的奇异点。这可以写成如下：：readyF orT oken=（<$BAD）@（0，+：readyF orT oken）：readyF orT oken=（<$BAD）@[+：readyF orT oken]第二子目标直接由安全性条件：readyForToken：transmantanything;而第一个子目标可以通过观察系统在等待令牌时和令牌到达后的规范来证明。根据第7页所写的表达式，可以实现以下证明状态► t +1：recT oken？？[<$：readyF orT oken<$$>：transmantAnything]; ;（<$：readyF orT oken（：dataBufferEmpty（：transmittenokenany. ：transmittData（any））@[0，+：readyF orToken））（：getDataBuf fer（%d）► t：readyF或Token（：transmittData（d）发送：transmittToken）@[0，+：readyF orToken）► t（<$BAD）@（0，+：readyF或T oken）规范必须根据组件的集成进行验证。授予令牌传递的属性确保环的每个节点的均衡通信优先级。令牌传递是快速的，并且在端口通信的小延迟的基础上，P. Bellini等人理论计算机科学电子笔记116（2005）241251在一个单一的时间样本。集成属性断言，如果通信信道中断，则令牌沿备份环传递考虑到两个相邻节点（n1，n2），我们假设：n1正在尝试发送令牌（n1.sendingT oken），n2正在等待令牌。n2的等待状态可以表示为：n1.sendT oken！！ @[−n2.readyForT oken，0）此外，必须断言<$n1.brokenChannel<$n 2.brokenChannel;n2. buferEm pty为真，意味着没有消息可以发送。连接的端口n1.sendT oken和n2.recT oken之间的同步激活n2. transmittToken;中断的信道条件使令牌能够在n2.sendT okenBack端口上传输。等待同步的连接端口n1.recTokenBack可以在备份环中传播令牌。5结论和今后的工作验证和确认对于基于组件构建的系统非常重要C-TILCO允许在子组件和原语中指定整个系统，以控制它们之间的通信在对基于组件的体系结构进行适当的形式化之后，可以通过属性证明来执行集成测试这种验证需要专门的工具来轻松地进行大量的证明。为此，在PVS定理证明器中实现TILCO时序逻辑（包括TILCO-X和C-TILCO功能）正在进行中。引用[1] P. 贝利尼河Mattolini和P.Nesi，Temporal logics for real-time system specification，ACMComputing Surveys31（2000）。[2] P. Bellini，M.A. Bruno，P.Nesi，无功系统外部规范的验证，IEEE Trans.《系统人与控制论》，A部分，30-6（2000），pp.692-709[3] P. Bellini，A.李文龙，“时序逻辑规范的实现”，第八届IEEE国际会议论文集。复杂计算机系统工程会议，Greenbelt，（马里兰州，美国）（2002年）。[4] P. Bellini和P. Nesi，Communicating TILCO：a model for real time system specification，in：Proc of the 7th[5] P. Bellini和P. Nesi，TILCO-X：TILCO时序逻辑的扩展，在：第七届IEEE复杂计算机系统工程国际会议论文集[6] G. Bucci ，M.Campanai和P.Nesi，Tools for specifying real-time systems，Journal of Real-Time Systems 8（1995），pp. 117-172[7] A. Coen-Porisini角Ghezzi和R. Kemmerer，Specification of real time systems using ASTRAL，IEEE Trans. on Soft.工程师：23（1997）572-598252P. Bellini等人理论计算机科学电子笔记116（2005）241[8] R.李晓云，一种实时系统的区间逻辑，北京：计算机科学出版社，2001。工程师：2001年3月至4月[9] G. Leavens和M.西塔拉曼基于组件的系统的基础。剑桥大学出版社，2000年。[10] L.陈晓，基于构件的软件，北京大学计算机科学与工程学院学报，2003，（M。Pezze，编），华沙，2003年4月。