软件体系结构静力分析方法的改进与普通微分方程验证

理论计算机科学电子笔记243（2009）49-67www.elsevier.com/locate/entcs软件体系结构验证方法的改进定左华1号浙江理工大学地址：浙江省杭州市余杭区刘静23华东师范大学上海市可信计算重点实验室，上海，200062摘要静态分析可能导致状态空间爆炸问题。在本文中，我们探讨的微分方程模型，使验证软件体系结构属性的任务更加有效。我们演示了如何使用普通的微分方程来验证架构描述的特定于应用程序的属性，而不会遇到这个问题。一个体系结构行为可以用一组包含一些控制参数的普通微分方程来建模，其中控制参数用来表示确定性/非确定性选择。每个方程都描述了状态的变化。通过检查与控制参数相关联的条件，我们可以检查方程模型是否可行。 在求解一个可行方程模型后，根据解的行为和状态变量的表示，可以分析体系结构的性质。一个WRIGHT架构描述的加油站问题已被用作例子来说明我们的方法。所有的方程都是用Matlab工具计算的。关键词：静力分析;建筑;普通微分方程;赖特。1介绍静态分析是一种在不执行的情况下验证程序行为的方法。该方法是特别有用的，在识别程序设计错误之前，实施。事实证明，在生命周期的早期检测错误可以大大降低修复这些错误的成本一些静态分析技术1电子邮件：zuohuading@hotmail.com2电子邮件地址：jliu@sei.ecnu.edu.cn3 通讯作者1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.07.00550Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）49已提出它们跨越了基于可达性的分析技术、符号模型检查、流方程和数据流分析等方法。这些技术和方法已被用于几种分析工具中，例如INCA [5]中使用的Flow方程，FLAVERS [11]中使用的数据流分析， SPIN [14]中使用的可达性分析，SMV [4]和SMC [21]中使用的符号模型检查在一般情况下，所有现有的方法似乎是非常敏感的使用并发结构和异步进程的数量方面的分析特别是，可达性分析可能会导致状态空间爆炸的问题，因为它必须穷尽探索所有的可达状态空间来检测并发错误。尽管已经提出了许多技术来对抗这种爆炸，如状态空间缩减、组合技术、抽象等，但状态爆炸问题仍然是从研究到实践的主要技术障碍。现有的并发系统被描述为离散事件系统模型，适合于对系统并发进行建模。然而，离散将导致状态爆炸问题，因为模型检查器构建了一个有限的状态转移系统，并在可达状态空间中搜索违反所研究性质的行为[3]。因此，要彻底解决状态爆炸问题，一种方法是将离散事件系统模型连续化为连续系统模型，使系统可用解析表达式描述因此，我们可以分析解析表达式的解，而不是计算状态。Petri网是连接离散事件系统和连续系统的一个很好的候选者。一方面，Petri网作为离散事件系统的建模、分析和综合的工具得到了广泛的应用。Petri网相对于有限自动机具有更大的优势，特别是当模型复杂性和进程并发性问题另一方面，连续系统可以用Petri网来近似[20]，并且Petri网模型被Lunze等人用作连续变量系统的离散事件表示[17 ]第10段。然而，Petri网在进行可达性分析时也会出现状态爆炸问题[18]，即使有一些网约简方法。解决这个问题的一种方法是通过去除完整性约束来使用某种松弛。这种松弛导致了一种连续时间形式主义：David和Alla的连续Petri网（CPN）[6][7]。实际上，连续Petri网是时间（离散）Petri网的近似。连续Petri网的语义由一组普通的微分方程（ODE）定义，其中一个方程描述了给定位置的标记值随时间的连续变化CPN中不同的触发样式会导致CPN的不同语义。在本文中，我们考虑了一个修改的VCPNs，其中瞬时射击速度取决于标记，使得标记是连续的，没有不连续点。基于CPN，并发系统可以由一组包含控制参数的常微分方程组来建模，其中控制参数Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）4951参数用于表示确定性/非确定性选择。每一个方程都描述了状态的变化，这表明当程序在执行时，状态可以达到某种程度。通过检查与控制参数相关联的条件，我们可以检查方程模型是否可行。在求解了一个可行方程模型后，基于解的行为和状态变量的表示，我们可以分析体系结构的属性。所有方程组都将由Matlab求解。我们工作的主要目标是研究我们的技能在验证架构的应用特定属性方面的适用性。我们研究了一个示例架构，一个加油站问题的WRIGHT描述，并说明了可以验证的属性类型和可以在生命周期早期发现的错误类型由于我们的体系结构是用CSP描述的，我们首先将CSP转化为Petri网，然后建立一个离散方程模型，以分析状态空间。本文件的结构如下。第2节具体说明了一个加油站与赖特。第三节根据Wright规范建立Petri网模型。第四部分建立了基于Petri网的离散方程模型。在第5节中，我们展示了如何计算状态测度。第六部分是基于解的性质分析。在第七节中，我们演示了如何使用我们的方法来检查加油站的属性。第八部分是本文的结论和讨论。2赖特加油站的规格根据[1]，建筑规范语言Wright的发展是为了为指定建筑描述的结构和行为提供正式的基础。Wright围绕组件、连接器和配置的基本架构抽象而构建。每个组件由一个组件类型描述定义，该描述由一个接口和一个计算组成。接口还包含多个端口。每个端口代表与组件可能参与的环境的交互，而计算描述组件的内部行为。赖特的连接器定义了组件之间的交互模式。每个连接器都由胶水和一组角色组成。角色表示对将参与交互的组件的约束。Glue实际上是组件中计算的对应物。Wright使用CSP[13]来形式化系统行为。加油站问题的性质分析，特别是死锁分析已经得到了广泛的研究。自动化加油站一般由一组操作员、一组加油泵和一组客户组成。场景如下：顾客不断地到达加油站，要求从随机选择的泵中的一个泵获得一定量的气体。每个顾客必须到一个有空的收银员那里付完油费才能被允许加油。如果所有的收银员都在为顾客服务，需要付款的顾客必须等待下一个有空52Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）49收银员。付完煤气费后，收银员会启动顾客的加油泵。如果所有的泵都在使用中，客户必须等待，直到有一个泵空闲。在我们的研究案例中，我们考虑了一个简单的加油站问题，其中包括两个客户，一个收银员和一个加油泵。Wight规范如下所示。组件收银台端口客户1 =接受？x→客户1端口客户2 =接受？x→客户2端口到泵=激活！x→ToPump计算= customer1.accept？x→T oP ump.激活！x→计算Q Customer2.accept？x→启动水泵！x→计算组分泵端口软管1 =带？x→软管1端口气体1 =泵！x→气体1端口软管2 =取用？x→软管2端口气体2 =泵！x→气体2PortFromCasher=获取订单？x→FromCasher计算=FromCasher.getorder？x→（（Hose1.take？x→气体 1.泵！x→计算）Q（软管2. x→气体 2.泵！x→计算））组件客户港口支付=支付！x→支付港口采取=采取！x→取端口气体=泵！x→气体计算=P ay.pay！x→take.take！x→Gas.pump? x→计算组件客户收银台角色Givemoney =支付！x→GivemoneyRole Getmoney =accept？x→GetmoneyGlue = Givemoney.pay? x→Getmoney.accept！x胶水组分客户泵软管角色GETHES = TAKE！x→GethoseRole Givehose = take？x→GivehoseGlue = Gethothes.take？x→Givehose.take！x胶水组分客户泵气体角色Getgas =泵？x→Getgas角色Givegas =泵！x→Givegas胶水= Givegas.泵？x→Getgas.pump！x胶水组分灌装泵角色讲述=激活！x→告知角色确认=获取订单？x→确认Glue= Tell.激活？x→确认。获取订单！x胶水实例customer1：客户customer2：客户收银台：收银台泵：泵（略）附件（略）我们创建了四个组件实例和七个连接器实例，它们都位于连接器部分之下。收银员模块共有三个通信端口（Customer1、Customer2和ToPump）。两个是输入（客户1和客户2，由CSP“？”操作员），剩下的一个是输出通信（ToPump，由CSP“！”操作员）。 该收银员模块的内部操作被指定为收银员组件的计算，Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）495311011112020122212102组件，它非确定性地（使用CSPQ运算符）选择两个可能的执行路径中的一个：与来自端口Customer1的输入通信会合，然后是到端口ToPump的输出通信（这是” → ！将通信从端口Customer2发送，然后将输出通信发送到端口ToPump（即→：！“分支）。所有其他组件和连接器规格可以类似地解释。与[19]一样，我们将检查架构的两个规范。第一个是关键的比赛，其中一个客户支付天然气，第二个客户然后支付并在第一个客户获得天然气之前使用泵。第二个具体规定是，没有客户收到天然气而不支付。3加油站在本节中，我们将解释如何将系统的Wright规范映射到Petri网模型中。我们需要一些可以在[16]中找到的一般概念。层次结构和模块：基本的Petri网模型不支持层次结构和组合。与大多数ADL规范一样，整个系统通常由组件和连接器组成，这些组件和连接器最适合描述为整个系统的子模块为了支持这一点，我们将模块的概念引入我们可以将每个组件或连接器映射到一个小的Petri网模块（子图）中。有了所有的模块，再加上下面的IO-nets概念，我们就可以对整个系统进行建模。IO网、IO位置和IO转换：IO网的概念来自软件设计中的模块化思想。IO-net是Petri网和接口的组合。接口指定了IO-net（模块）与其环境交互的方式。它可以表示一组异步通信通道。IO网络的接口使用IO位置和相关弧表示，如图1所示。IO转换是那些具有到IO位置的传出弧或来自IO位置的传入弧的转换。IO-Net1IO-Net22111Fig. 1. 以IO Net为例。内部变迁：所有没有到IO位置的传出弧或从IO位置传入弧的Petri网变迁都被定义为内部变迁。映射算法的基本思想是将每个组件实例映射到Petri网模型的子模块，将每个原子连接器实例映射到IO库所。0122112112 0254Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）49这里的原子连接器是指其Glue部分仅包含Role部分中定义的操作的连接器。如果有内部计算步骤，而不是简单地在Role部分之间携带数据，这使得连接器是非原子的，我们可以将这些连接器的计算步骤映射到子模块中，方式与组件相同。CSP行为规范的基本单元是一个事件，它代表Wright中的一个动作。因此，Wright中的每个事件都可以映射到Petri网中的一个变迁。携带数据的动作可以映射到IO转换。输出动作（e！x）包含输出弧到IO位置，而输入动作（e？x）包含来自IO位置的传入弧。不携带数据的操作可以映射到内部转换中。一旦转换被固定，就可以在转换之间添加位置，以根据计算部分中的指定将整个Petri网连接在一起。通常，组件实例的每个Port都可以映射到一个包含至少一个IO转换的转换聚合。在大多数情况下，Port不包含内部转换，因此Port可以映射到IO转换，因为这样的Port通常只包含详细的规则，我们参考[16]。这种映射实际上是CSP操作符到Petri网转换结构的转换。定义了一组转换规则，以覆盖最常见的CSP操作[22]。在这些规则下，体系结构的属性（如死锁）将被保留。这样，我们得到的Petri网，使每个过渡有最多两个输入弧和最多两个输出弧。我们有以下定义。定义3.1一个地点/变迁链是一个网，变迁由一个有一个输出弧而没有输入弧的头地点，一个有一个输入弧而没有输出弧的尾地点，以及有一个输入弧和一个输出弧的地点连接。如果起始位置和结束位置重叠，则该链称为位置/变换循环。定义3.2一个库所/变迁循环称为过程循环，如果循环中的每个变迁是1）一个有一个输入弧和一个输出弧的变迁，这个变迁称为过程的内部变迁，2）一个有一个输入弧和两个输出弧的变迁，这个变迁称为过程的输出变迁，这里一个输出弧用于构造循环，另一个用于循环的输出，3）一个有两个输入弧和一个输出弧的变迁，这个变迁称为过程的输入变迁，这里一个输入弧用于构造循环，另一个用于循环的输入，4）一个有两个输入弧和两个输出弧的变迁，这个变迁称为过程的输入-输出变迁，这里一个输入弧和一个输出弧用于构造循环，另外两个分别用于循环的输入和输出。因此，每个组件包含一个或多个过程循环，这取决于组件是否包含任何或一些选择控件。加油站问题的完整Petri网模型见图2。在构建Petri网时，我们可能会得到一些我们使用Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）4955客户2Customer1支付支付泵采取采取泵c2.acceptc1.accept激活收银员获取订单oil2.pumpoil1.pumphose2.takehose1.take泵图二. 加油站网特殊变量，称为状态变量，用于在每个位置记录它们，使得当系统从一个位置执行到另一个位置时，状态变量在本文中，这些变量是从控制结构中提取的，如if/else，switch等。在加油站的例子中，我们可能有两个变量，1和2，分别代表谁付钱，谁挑水管。因此，每个变量都有域{customer 1 customer2}。我们有以下定义。定义3.3（系统状态）系统状态被定义为一组变量，它们的值已经改变。因此，每个地方都对应一个国家。4用普通微分方程4.1连续Petri网最后一节所得到的Petri网是离散Petri网，其库位上的标记数为整数。如果转换的每个输入位置都标记有标记，则启用转换。启用的转换通过从每个输入位置删除一个标记并向每个输出位置添加一个标记来触发。现在看看下面的例子，看看数据是如何处理的。如图3（a）所示，一个过程循环有几个位置，12并且具有输入位置，i过渡时1 .一、 我们假设那个地方1有一个令牌，这意味着该进程正在访问这个地方，我有3个token，这意味着在buffer中有三个数据。56Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）491（）1我2（）111（）2（）21我1121我1121我112(a)(b)（c）第（1）款图三. 离散Petri网中的标记变化。该过程必须访问位置13次，以移走位置i中的所有3个令牌。换句话说，3× 1的token将从位置1移动，如图3（b）（c）所示。因此，输入位置i中的标记可以被视为影响当令牌从处理位置1移动时， 如果缓冲器中的数据量很大，并且一个程序有很多这样的缓冲器，那么我们将得到大量的可达标记，这可能会限制离散Petri网的使用现在，我们假设标记作为连续的连续流移动，则标记移动速率可以被认为是以下的乘积：1（）×i（），其中1（）和i（）分别是时间1和i这可以想象图四、见图4。 Petri网中的连续Petri网。基于这一思想，我们提出了一种新的连续Petri网模型。在这个模型中，过渡的瞬时触发速度与输入位置的标记的乘积成比例。定义4.1连续Petri网是一个元组=prepost，其中（一）={12n}是一个有限的非空的位置集合，（二）={12m}是一个有限的非空转移集，(iii)pre={→}是连接具有过渡的地点的有向弧的集合post={→}是连接过渡到地点的一组有向弧(iv)： →（0 ∞）是一个映射，用于为每个转换分配一个触发速率。定义4.2设=[0 ∞）为时间间隔，设i：→[0∞）=12是与位置i相关联的映射的集合。 连续Petri网=pre-post的一个标记是一个映射：→ [0 ∞）n（）=（1（）2（）n（））Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）49572.1.3一个有标记的CPN是一个2元组（0）其中-是CPN，-0=（1（0）2（0）n（0））是它的初始标记，其中i（0）取值1或0。保持初始标记1的位置被称为开始位置。一个地方的标记可以用来衡量这个地方被访问的频率。我们有这样的定义：定义4.4（状态测度）给定任意时刻∈[0 ∞），状态在某种程度上可以达到。这个度称为状态测度，记为（）。状态度量取非负实数作为其值。稍后，我们将证明每个过程循环的状态取[0，1]中的值。对于一个状态，如果（）= 1，那么我们说程序完全处于该状态，或者只是在国家。如果（）= 0，那么我们说程序不在状态。以上所述，都 因此，如果新的标记被移到一个地方，我们说状态在增加;如果一些标记被移出一个地方，我们说状态在减少。状态测量的变化率可以计算如下。让1和2是转换的输入位置它们的标记1（）和2（）。 让 与之相关的发射率 ，则从每个位置开始的标记移动速率被定义为乘积1（）2（），其中表示正则乘法。此表达式包含启用信息：如果1和2为零，则发射率为0，这意味着转换未启用。我们的定义放大了状态，这在我们研究状态趋势时很有用。我们的定义是使状态标记不连续，因此状态变化是连续的，没有不连续点Gilbert和Heiner [12]已经成功地使用类似的连续Petri网模型来研究生物化学系统，以探索可能的可观察行为，其中所有原子作用的激发速率是所涉及物质浓度的乘积。这里浓度是连续函数，这是我们的论文中的状态测度函数定义4.5标记CPN的稳态是所有转换都在激发的状态。4.2建立微分方程模型净标记（状态测量）变化取决于程序结构和发射率。基于上一节定义的语义，每个位置的标记可以用一个微分方程表示。我们在这里考虑选择结构。至于其他情况，请参阅[9][8]了解详情。1) 确定性选择如图5所示。让一个地方，可以移动标记2或三是基于一定条件的确定性。我们分配一个变量，称为控制参数，以帮助建立方程。与某种情况有关如果条件为真，则58Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）491112233252334图五.决定性的选择。取值1，否则k为0。假设条件为真，到2，则转换1的输入为，而转换3的输入为（1-）。该网络的方程模型为拉吉1个1−2−（1−）3J=−22J=（1−）−332)不确定性选择如图6所示。设为一个位置，可以将标记非确定性地移动到1或2我们还指定了一个控制参数来帮助建立方程。但这一次没有条件与控制参数取值为0或1。在这幅图中，第一个过程的转换1的输入是1，而第二个过程的转换3的输入是3（1-）。3见图6。 不确定性的选择相应的微分方程为：⎧J⎪1吉吉2J⎪3吉吉4=（）1−11=1个1−2 2=（）2−33（1−）=33（1−）−44这里我们使用（）来表示其他一些状态度量。如果共享涉及两个以上的进程，比如3个进程1、2和3，那么我们将有两个参数：1和二、 让一、3和5是需要资源的输入转换。转换的输入为：（）11，（）2（1 −1）2，和（）3（1−1）分别为<$（1−2）<$。系统中的所有参数形成一个向量，（12n），称为对照1−131132424⎪Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）4959[vector. 通过选择12n，我们可以在系统执行时显示不同的方面。5计算程序状态微分方程模型中含有非线性常微分方程，因此很难给出解的解析表达式。然而，我们可以计算解的趋势并估计解的范围。命题5.1对于任何位置/变迁循环，如果它至多有一个起始位置，则无论如何选择触发率，该循环的状态测度都收敛到[0，1]中的数。特别地，1）如果循环不包含起始位置，则所有状态测量值为0。2）如果循环包含一个起始位置，并且循环的所有输入都具有正的状态度量，则循环的状态度量收敛于（0，1）中的数字我们假设每个进程都有一个起始位置。命题5.2当一个系统达到定态时，无论触发率如何选取，每个过程的测度都趋近于[0，1]中的数。证据因为每个过程都是一个或多个包含起始位置的位置/转换循环。从命题5.1开始，过程的状态测度将接近[0，1]中的数字。注：我们没有计算输入位置和输出位置。它们的状态度量可能超过1，除非它们也处于某个地方/过渡周期。命题5.3给定一个过程循环，如果它没有输入，那么所有的状态测度都收敛到（0，1）中的数。6性能分析我们基于Petri网得到的常方程模型可能是不可行的，即，系统不能采取其状态测量可以在方程模型中求解的某些状态。 换句话说，有些状态在执行时是不能访问的。因此，为了研究程序特性，我们首先需要确定所获得的方程模型是可行的。当一个状态被访问时，一些状态变量的值被改变了，或者状态变量的域被改变了。如果某个状态变量在如果没有状态变量域为空，则方程模型是可行的。基本上，可变域由来自控制参数的条件更新比如让 是一个状态变量，我们也使用Dx来表示. 我们称（Dx）为变量的表示 . 设[ ]为条件，变量，则[ ]DxDx。 我们也定义[]（Dx）=（]Dx）60Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）49[如果x=0，则x=0（Dx）=0。让是一个控制参数。 条件与if = 1相关联，表示为（= 1）。假设1和2是两个参数，使得（1=1）1[]and（2=1）2[]，and1[]2[]=0。Then1[]2[ ]（Dx）=1[]（2[]Dx）=（1[]2[]Dx）= （）=因此，具有1的状态或具有2的状态将不会被访问。方程模型是不可行的。一般来说， 对于该系统， 我们有一个向量 变量表示：（（Dx））。对于这个向量，我们有规则[ ]（（Dx））=（]（Dx））系统的性质将从这个向量中得到暗示。注意，在条件有输入或输出的情况下，我们将使用marco将输入/输出从条件中分离出来。因此，上述定义仍然成立。对于可行方程模型，我们有以下定义：定义6.1（稳定和不稳定系统）对于任何一组控制参数值，如果系统的所有状态都收敛到[0，1]中的数字，无论如何选择点火率，那么系统是稳定的。对于某组控制参数值，如果存在一组点火率使得至少有一个状态测度收敛到大于1的数，则系统是不稳定的。在系统稳定的情况下，我们证明了由一组通过消息传递相互通信的进程组成的并发系统的以下结果[10]。定理6.2如果存在一组控制参数值使得程序的每个状态测度要么收敛于1（包括同等于1）要么收敛于0（包括同等于0），则无论触发率如何选择，程序都有死锁.在系统不稳定的情况下，我们有如下结果。定理6.3给定一个不稳定系统，至少有一个输入/输出位置不属于任何位置/转移环。证据假设系统不稳定。有一种状态，其状态测度大于1。 假设状态为，（）1。 如果每个地方都有循环，那么从命题5.1，我们知道它在[0，1]中。因此，它不在任何周期中。我们说它不在任何过程循环中，因为过程循环中的所有状态度量都在[0，1]中。 所以必须是一个输入/输出的地方。 这就完成了证明。这一结果意味着，与一些控制参数值，必须存在一个位置/转移链，是附加到一个过程循环。因此，我们可以推断Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）49614848>4>3个8>3个>3个12133567248在这种情况下，系统有机会遇到一些同步问题或不确定性行为，如竞争条件。非正式地说，如果某个计算步骤的结果取决于各个执行线程的调度，则例如，在图7中，进程1和2向3发送消息。见图7。 种族的例子。我们假设所有的发射率都等于1。方程模型是8mJ=m2−m1，>1个>mJ=m1−m2，>2个>mJ=m4−m3， mJ=m1−km5m7，>5>mJ=m3−（1−k）m6m7，6>>mJ=m8−km5m7−（1−k）m6m7，7：mJ= km5m7+（1 − k）m6m7− m8。如果= 1，则进程3从1获取消息，如果= 0，则进程3从2获取消息。Let =1“和=“然后是（= 1）和（= 0）<$。无论是例中，三个进程都在运行。但是对于1和2的相同输入，我们可能会得到不同的输出。这将反映在以下方程模型中。如果 = 1，我们得到方程模型8mJ=m2−m1，>1个>mJ=m1−m2，>2个>mJ=m4−m3，mJ=m1−m5m7，>5>mJ=m3，6>>mJ=m8−m5m7，7：mJ= m5m7− m8。通过简单的计算，5将被累加为大于1的数设为状态变量，描述进程3将获得消息的情况。 所以变量表示是（{12}）。此表示将更新为（{12}）=（ {1}）。如果= 0，那么我们得到方程Model8Jm1=m2−m1，>mJ=m1−m2，>2个>mJ=m4−m3，mJ=m1，>5>mJ=m3−m6m7，6>>mJ=m8−m6m7，7：mJ= m6m7− m8。62Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）49客户2Customer171支付支付829泵3采取采取泵10413111−1c2.accept1c1.accept125614激活收银员15获取订单1816oil2.pump17oil1.pumphose2.take 1 −22hose1.take泵19通过计算，6将被累加为大于1的数，并且表示将被更新为（ {12}）=（{2}）。因此，在上述两个模型中，对于来自1和2的相同消息，我们得到两个不同的输出。7用微分方程分析加油站基于图2的网络，我们用状态度量标记每个位置，如图8所示。见图8。 加油站网络与标记和控制参数。一共有19个位置，所以我们有19个方程。在组件Casher中，由于13中的token可以无限期地分配给c1.accept或c2.accept，因此我们需要为这个地方设置一个控制参数，在图中为1如果1= 1，那么收银员首先从顾客1那里得到钱，否则顾客2首先得到钱。同样在组件Pump中，hose1.take和hose2.take都有相同的机会从17，我们需要另一个控制参数2在这里十七岁 如果2= 1，则客户1将首先使用软管，否则客户2将使用软管。不失一般性，我们可以假设这两个客户使用相同的速度来付款，挑选软管和泵气。因此，我们可以假设所有的发射率都等于1。我们可以使用两个状态变量1和2来分别表示收银员从谁那里接受钱和谁挑选水管。他们的领域是：Dx1={客户1客户2}Dx2={客户1客户2}向量（12）将与每个状态相关联。让Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）4963910M：J1[1]=收银员接受顾客1的钱€1[1] =收银员接受顾客的钱2，2[2] =客户1选择软管，€2[2] =客户2选择软管。两个参数1和2与这些条件有关（1= 1）（1[1]）（1= 0）（<$[1]）（2= 1）（一）二、[2]）（2= 0）（[2]）加油站的微分方程模型如下：8 mJ= m m −m>16 3 1> mJ=m1−m2>2个> mJ=m2−m3m6>3> mJ=m1−k1m4m13>4> mJ=m2−k2m5m17>5> mJ=m16−m6m3>6> mJ=m9m12−m7>7> mJ=m7−m8>8>mJ=m8−m9m12J=m7−（1 −k1）m10m13>>MJ=m8−（1 −k2）m11m17>11>MJ=m18−m12m912>>MJ=m14−k1m13m4−（1 −k1）m13m10>13>MJ=k1m13m4+（1−k1）m13m10−m14>14>MJ=m14−m15m19>15>MJ=k2m5m17−m16>16>MJ=m15m19−k2m5m17−（1 −k2）m11m17>17> MJ=（1−k2）m11m17−m18>1819 =m16+m18−m19m15方程模型的初始值为1（0）=7（0）=13（0）=19（0）= 1，2（0）=3（0）=4（0）=5（0）=6（0）=8（0）=9（0）=10（0）=11（0）=12（0）=14（0）=15（0）=16（0）=17（0）=18（0）= 0根据分配给1和2的值，我们总共有4种情况：1) 案例1.（12）=（11）。 模型的解如图9（a）所示。 由于所有的状态测度都在[0，1]中，在这种情况下，系统是稳定的。状态变量域可以计算如下。对于过程Casher，我们有（（1Dx1）（2Dx2））1[1]=（（11[1]Dx1）（2Dx2））=（（1{customer1}）（2Dx2））对于工艺泵，我们有（（1{customer1}）（2Dx2））2[2]=（（1{customer1}）（2 2[2]Dx2））=（（1{customer 1}）（2{customer 1}））因此，对于整个系统，我们有变量表示：M64Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）49（（1{customer 1}）（2{customer 1}））我们可以把这个表达理解为顾客付了钱，就可以得到汽油。从解曲线中，我们还可以发现，7→08→ 012→ 018→ 0Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）4965M10男性11例M9m13m3男性19例M4m15m17MM614MM8米12米 1816米71mM21.21.2110.80.80.60.60.4 0.40.20.200−0.20 2 4 6 8 10 12 14 16 1820不−0.20 2 4 6 8 10 12 14 16 1820不见图9。 （一）. 情形1：（k1，k2）=（1，1）. （b）. 情形2：（k1，k2）=（0，0）.8→0意味着状态8最终没有被访问，换句话说，客户2没有支付这笔钱。 同样地，18→0意味着国家8最终没有被访问，换句话说，客户2没有机会拔出软管，因此得不到气体。2)案例2.（12）=（0 0）.模型的解绘制在图9（b）中。系统稳定。这种情况下的客户2与情况1中的客户1相同。顾客2付了钱，得到了汽油。客户1没有支付这笔钱，也不会得到汽油。因此，从案例1中，我们暗示，如果客户支付，那么他/她将获得天然气;从案例2中，我们暗示，如果客户不支付，那么他/她将不会获得天然气。因此，我们可以得出结论，第二个规范“无游离气体”是满足的。3) 情况3：（12）=（10）。 该模型的解如图10（a）所示.从曲线中，我们发现状态测度10接近于2。 因此，该系统是不稳定的。可变结构域可以如下计算。对于过程Casher，我们有（（1Dx1）（2Dx2））1[1]=（（11[1]Dx1）（2Dx2））=（（1{customer1}）（2Dx2））对于工艺泵，我们有（（1{customer1}）（2Dx2））2[2]=（（1{customer1}）（2<$2[2]Dx2））=（（1{customer 1}）（2{customer 2}））因此，对于整个系统，我们有变量表示：（（1{customer 1}）（2{customer 2}））我们可以把这个表达解释为顾客1付了钱，顾客2得到了汽油。M4MM35男性13例男性19例M10m15m17MM1814Mm m7MM8121m6m162标记标记66Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）49M10mm53M9男性13例男性19例男性11例M 4MM15 M1418米17米12M8M mmm7m26161221.51.5110.5 0.500−0.50 2 4 6 8 10 12 14 16 1820不−0.50 2 4 6 8 10 12 14 16 1820不见图10。（一）.情形1：（k1，k2）=（1，0）.（b）.情形2：（k1，k2）=（0， 1）.4) 情况4：（12）=（0 1）。模型的解绘制在图10（b）中。 系统也不稳定。除了客户1和客户2的位置改变之外，这与情况3）相同。因此，从案例3和案例4中，我们可以得出结论，第一个规范是满意的。8讨论与结论最封闭的工作是由Naumovich等人在[19]中进行的，他们使用了两种并发分析工具INCA和FLAVERS来验证与我们论文中相同的加油站架构规范。在INCA中采用了流动方程技术来检验系统的一致性不等式使用标准的整数线性规划包来解决然而，整数线性规划问题通常是NP难的，所涉及的标准技术是潜在的指数。FLAVERS是基于数据流分析的工具。通过近似程序的执行模型，可以使用多项式算法有效地检查属性然而，这样得到的结论通常要么是完整的，要么是合理的，但不是两者兼而有之。一般来说，现有的静态分析技术即使采用了诸如SPIN等状态约简技术，也不能完全避免碰撞状态爆炸问题。原因是我们必须搜索所有可达到的状态，以确定属性是否可以满足。用我们的方法，我们只需要求解2k个微分方程组，其中为控制参数个数。给定这些s的一组值，我们将得到一个方程组。因此，这些方程组是独立的，可以并行求解。所以复杂性仅由一个方程组决定。通过分析解决方案，我们可以确定架构是否能够满足需求。系统越大，这种方法表达的功能就越强大。这就是为什么我们在进行静态分析时可以避免状态爆炸问题。现有的静态分析工具可以自动检查属性，但是仍然要由系统架构师来制定这些属性。通过我们的方法，它m4m119男性13例M3男性19例M5M10 MM1415M16男性17例m6m2MMmm1m812187标记标记Z. Ding，J.Liu/Electronic Notes in Theoretical Computer Science 243（2009）4967用Matlab编写方程组并进行计算是非常容易如果方程的数量很大，我们确实需要一个工具来分析离散值解，而不仅仅是检查Matlab中的曲线。我们并不声称我们的技术可以取代现有的分析工具。 在现有的工具中，属性都是用时态逻辑来表示的。为了检查感兴趣的属性，我们可以设计一些检查语句并将它们插入到输入语言中。通过这种方式，我们可以立即知道指定的属性是否满足。缺点是这些工具可能不适合大型系统。在我们的例子中，我们可以很容易地找到异常行为，然后基于状态变量表示来分析架构的属性是否满足。缺点是我们需要解释变量表示。 此外，我们还没有证明状态变量表示可以描述的所有属性的架构。通过将我们的技术与现有的技术相结合，我们还可以提高检查速度