概率B方法的应用研究：储罐监控中的概率建模与验证

理论计算机科学电子笔记137（2005）183-204www.elsevier.com/locate/entcs储罐监控：pAMN案例研究史蒂夫·施耐德1英国萨里大学计算机系泰山晃澳大利亚新南威尔士大学计算机科学与工程学院Ken Robinson澳大利亚新南威尔士大学计算机科学与工程学院海伦·特雷哈恩英国萨里大学计算机系摘要将概率行为引入B方法是最近的发展。除了允许对概率行为进行建模之外，还可以表达和验证机器状态的期望值之间的关系本文探讨了概率B在一个简单的案例研究中的应用：通过测量进入储罐的液体的流量来跟踪储罐中的液体体积。流量可以随着时间的推移而变化，传感器用于测量流量，具有一定的准确性和可靠性，分别建模为非确定性和概率在规范层面，分析关注概率B机中的期望子句及其与机器操作的一致性在细化层面，概率GSL的细化和等效定律用于确定传感器的特定设计提供所需的可靠性水平。关键词：概率B，精化，形式化方法，概率谓词转换器。1 电子邮件：S. surrey.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.031184S. Schneider等人理论计算机科学电子笔记137（2005）1831介绍B方法[1]提供了一个开发可证明正确系统的框架，基于广义替换语言（GSL）的最弱前提语义，并围绕抽象机的概念构建。最近有人提出将概率行为引入B方法[2]，称为概率B。这种方法建立在以前的工作中，将概率选择引入程序语句，并将最弱前提语义的概念扩展到处理期望[5]。期望值可以被认为是公式或表达式的期望值。因此，程序可以被视为期望转换器而不是谓词转换器，并且它们的语义在程序执行之前的期望方面给出了表达式在程序执行之后的期望。除了允许这种概率行为进入程序之外，prob-probB还引入了对状态方面的期望，以及B机器的现有部分因此，机器状态的几个组成部分的期望值之间的关系可以被表达和形式化地验证。本文探讨了概率B在一个简单的案例研究中的应用：通过测量进入罐中的液体流量来跟踪罐中液体的体积。具有给定可靠性的传感器用于测量流量并向系统提供信息使用概率B描述传感器的行为。我们在我们的模型中明确地包括了水箱，这样我们就可以描述它所包含的液体的实际体积与我们的系统对它的测量之间的除了概率行为外，我们的系统在故障传感器将给出的读数中表现出不确定性行为，并且（在我们考虑的第一种情况之后）在正确工作的传感器将给出的读数中表现出不确定性行为因此，案例研究还探讨了概率和非确定性行为之间的相互作用。案例研究涉及开发过程的两个阶段：规范化和细化。在规格水平上，我们关注的是获得储罐中液体体积的系统值的准确性界限这个分析将涉及概率B机中的期望子句在细化层面，我们关注的是确定特定的传感器组合确实S. Schneider等人理论计算机科学电子笔记137（2005）183185确实提供了所需的可靠性水平。该分析将使用概率GSL的精化和等价定律。2概率导论2.1可能的GSLpGSL是GSL的扩展，包括概率选择语句：prog1p执行这个选择将以概率p执行prog1，并以概率1-p执行prog2。参见[6，3，4]，了解pGSL的完整介绍。为了给pGSL程序一个语义，我们利用期望：状态空间的有界非负实值函数。这些通常表示为状态变量的公式。程序prog的最弱预期望语义将期望exp映射到另一个期望[prog]exp，类似于最弱前提语义。它给出了prog后exp的期望值，即对prog前状态的期望值。图1给出了[6]中的语言及其语义。在本文中，我们将使用一个导算子（也在[1]中给出），从一个非确定性选择的集合S中将某个元素赋给一个变量我们定义x：∈S=^@y. （y∈S=x：=y）因此[x：∈S] exp=（min x|x∈ S。exp）我们还将使用导出算子（也在[3]中给出）来表示选择的最小概率。我们定义p rog1pp rog2=^@q. （p≤q≤1）=prog1qprog2这个程序选择prog1的概率至少为p。算子用于描述具有最小可靠性要求的系统。如果组件需要在至少90%的时间内正确运行，则可以将其描述为正确0。9不正确。例如，这将通过一个至少在95%的时间内正确运行的组件来细化。2.2一些pGSL定律语义支持关于各种运算符的代数定律的集合。[3]的附录A.3给出了一个扩展的定律集。的186S. Schneider等人理论计算机科学电子笔记137（2005）183概率广义替换语言pGSL作用于期望而不是谓词。期望是状态空间的有界非负实值函数，例外的是，当处理奇迹时，它们可以取形式值∞。[x：=E]expexp[E/x][x，y：=E，F]exp exp[E，F/x，y][pre|prog]exppre×[prog]exp，其中re0×∞=b 0prog1[] prog2[prog1]expmin[prog2]exp[pre=nprog]exp1/npren×[prog]exp，其中re∞×0=b∞[skip]exp exp[prog1pprog 2]expp×[prog1]exp+（1−p）×[prog2]exp[@ y。预测值=预测值]经验值（最小值|pred。[prog]exp）所有实验的prog1 ± prog2[prog 1]exp $[prog 2]exp。• exp是一个期望• pre是一个谓词（不是一个期望）• 表示谓词pre转换为期望，这里限制为单位区间：false• ×是乘法。• prog、prog 1、prog 2是概率性的广义替换。• p是程序变量的表达式（可能但不一定是常量），取值为[0， 1]。• x是变量。• y是一个变量或变量的向量。• E是一个表达式。• F是一个表达式，或表达式的向量。• exp 1 $exp 2意味着exp 1处处不大于exp 2。Fig. 1. pGSL-概率通用替换语言[6]本文将使用该附录中的以下定律：定律13：（prog1pprog2）;prog3=（prog1;prog3）p（prog2;prog3）法则24：（prog1pqprog2）=prog1p（prog1qprog2）我们还利用以下定律，我们称之为定律A：prog2±prog1prog1pprog2=prog1pprog2S. Schneider等人理论计算机科学电子笔记137（2005）183187埃克塞特夫体积2.3概率B图二. 水箱系统有两个方面的概率行为引入到B机中提出[2]。首先是允许使用概率GSL构造操作，因此可以在操作中进行概率选择。第二种是在B机中引入期望一个EXPEC-TATION子句通常包含一个expect表达式的集合。这个子句在期望中的作用类似于不变子句关于国家的谓词。相关的证明义务是，来自任何合法状态（即满足不变量的任何状态）的每个操作都不得降低任何期望。每个期望的形式是e$V，这意味着V的期望值总是至少是e的初始值。与每一种预期相关的新的举证义务如下：P1初始化必须建立不变量的下限：e$[Init]VP2每次操作不得降低V的期望值：V$[Op]V在本文中，我们将使用形式V的期望。这是一个0$V的abbre-pixel。注意，这仍然产生了一个非平凡的证明义务P1，即V在初始化时是非负的。3罐我们要模拟的系统是一个装满液体的水箱。液体通过一根管子流入水箱。我们希望跟踪罐中液体的体积。这在图2中示出。该坦克可以模拟使用的机器在图32。这图3和本文其他地方所用的pGSL的asynthetic形式的解释如下：188S. Schneider等人理论计算机科学电子笔记137（2005）183机槽常数最小流量，最大流量属性minflow：REALmaxflow：REAL&最小流量> 0& 最大流量>= minflow可变流量、体积恒定流量：实际&体积：实际初始体积：=0||flow：：[minflow，maxflow]操作tock = flow：：[minflow，maxflow]||体积：=体积+流量结束图三. 储罐系统描述了真实储罐的模型，因此将包含在我们将给出的规范中，以便我们可以将监控系统的状态与储罐的真实状态相关联。在这里，我们假设在一个时间单位内（用tock表示），液体的体积增加的值为tow。最小流的值本身可以是最小流和最大流之间的任何值，并且可以在每个时间步长上改变。l和h之间的实数区间表示为[l， h]。区间[x+l， x+h]缩写为x+[l，h]。4监测系统4.1第一个简单的系统4.1.1质量标准我们希望生产一个软件系统，跟踪在坦克的液体体积到一定程度的准确性。我们需要的系统可以使用图4的概率B机器VolumeTracker1来指定。(The期望值使用了A和B的值，这将在后面给出对于第一个示例，我们采用一种简单的方法，其中单个轮询操作同时更新罐和监控系统状态。在本文的后面，我们将考虑将系统更新与坦克更新分离我们的第一个规范，VolumeTracker1，要求状态更新至少在99%的时间内完全准确。 否则（即高达1%的时间），它在可能的读数范围[min_low， max_low]上可以是完全任意的。参见附录AS. Schneider等人理论计算机科学电子笔记137（2005）183189机器体积跟踪器1包括油箱变量rvolume不变体积：真实& r数量*（最小流量/最大流量）<=体积&体积=r体积*（最大流量/最小流量）期望E1：r体积- A *体积，E2：B * 体积-初始化体积：= 0操作poll= T：tock||V1a：（r体积：= r体积+流量0.99（+）V1b：rvolume：： rvolume+[minflow，maxflow]）端见图4。VolumeTracker1机器系统保持单个状态变量rvolume，其包含系统具有的罐中液体体积的值。因此，我们的规范将关注rvolume和实际volumevolume之间的关系。很自然地，有两个期望值来提供关于在给定rvolume的期望值的特定值的情况下，volume的期望值可以是什么的范围。因为rvolume和volume在每一步都从一个固定的可能值范围中增加了一些值，所以我们认为期望值是rvolume和volume的线性组合。因此，它们的形式如下：E1：rvolume−A×volumeE2：B×体积−r体积它们必须都是非负的，所以我们可以推导出期望值，r体积/B≤体积≤r体积/A因此，给定rvolume的期望值，我们就有了volume的期望值的范围。由A和B给出的所需准确度将自然地作为规范的一部分出现。由于E1和E2都必须大于0，并且在每次出现轮询时都不减，因此我们得到了对A和B的可能性的一些限制。190S. Schneider等人理论计算机科学电子笔记137（2005）183注意，对volume和rvolume之间关系的任何绝对限制都将出现在不变量中。特别地，对于任何给定的rvolume值，体积的下限和上限由以下不等式给出：r体积×（最小流速/最大流速）≤体积≤r体积×（最大流速/最小流速）这将始终为真，因此它包含在不变量中。然而，它没有提供volume和rvolume之间非常紧密的关系。4.1.2推导A和B为了使VolumeTracker1履行其证明义务，我们要求在任何状态下，任何操作轮询调用时，我们可以进行一些计算来推导出A和B实现这一点的条件。我们要求E1$ [poll] E1 和E2$ [poll]E2.因此 ， 我们 要求 ， 对于 任意 的mow 、volume和rvolume，我们必须有（[poll]E 1）-E10和（[poll]E 2）-E2 0。我们从对E1的要求计算对A（[poll] E 1）− E 1=（[T||（V 1 a 0. 99V1b）]E 1）−E1=（[（T ||V 1 a）0. 99度（T ||V 1 b））] E 1）− E 1=（0. 99 × [T||V 1 a] E 1+ 0。01 × [T||V 1 b] E 1）−E 1（0. 99×（r体积+Δw−A（体积+Δw））+0。01×（r体积+最小流速−A（体积+流速）−（rvolume− A. 卷）=0。99×（低-A ×低）+0。01（最小低电压−A×最低电压）=（0. 99− A）×低电压+0。01×最小流量由于这必须在任何地方都是非负的（即对于所有可能的ω w值），我们得到：A≤ 0。99+ 0。01（最小流量/最小流量）对于任何价值的黄金。当最大值为最小值时，该界取其最小值，因此我们得到，A≤ 0。99+ 0。01（最小流量/最大流量）因此，最小最小流量和最大最大流量之间的比值越接近1，A就越接近1，并且对于任何给定的rvolume期望，volume的期望值的上限就越准确。但是，请注意，A始终可以至少为0。99.S. Schneider等人理论计算机科学电子笔记137（2005）183191对于B，我们执行以下计算：（[poll] E 2）− E 2=（[T||（V 1 a 0. 99V1b）]E 2）−E2=（[（T ||V 1 a）0. 99度（T ||V 1 b））] E 2）− E 2=（0. 99 × [T||V 1 a] E 2+ 0。01 × [T||V 1 b] E 2）−E 2（0. 99×（B（体积+Δw）−（r体积+Δw））+0。01×（B（体积+最大流量）−（r体积+最大流量）−（B. volume− rvolume）=0。99×（B. ow −01（B. ow− max=B ×低-0。99× 100 - 0。01×最大流量我们要求对于任意的ω w值，它都是非负的。所以B 0。99 + 0。01（最大低/低），适用于任何低值。表达式的最大值（即B的最大下限）在当λ ow=min λ ow时给出，并且我们获得B0。99 + 0。01（最大流量/最小流量）观察有关[ T]评价的第（*）和（**）行||[1b]对于一个期望。由于V1b在对rvolume的赋值中是不确定的，因此对rvolume必须采取。在E1中，rvolume为正值，因此在计算E1的预期望值时使用rvolume在E2中，rvolume为负，因此在计算E2的预期望值时使用rvolume这意味着，无论后来如何解决不确定性，期望值将至少是计算出的值。期望值应该总是非递减的，所以恶魔非决定论总是考虑增加的最坏情况。4.1.3例如作为一个例子，我们考虑一些具体的数字：如果最小最小值= 100，最大值= 400，那么我们得到A≤ 0。9925和B10。03.因此，我们知道，(100/103）×rvolume≤volume≤rvolume×（400/ 397）这意味着例如，0的情况。97× r体积≤体积≤ 10。03×r体积因此，如果我们要求97%的准确度，这将得到满足。192S. Schneider等人理论计算机科学电子笔记137（2005）183机器传感器1b看到罐操作sf，st<--poll1b =S1bl：sf：=流量||st：= ok>=0.9（+）S1br：sf：：[minflow，maxflow] ||st：=破碎端图五. A传感器机器然而，如果我们的要求是99%的准确度，这将无法满足。说明无法确保0。99×r体积≤体积。 这是因为一个错误的读数，可能发生的概率为0。01可能是错的4倍，导致R体积比体积的实际值大的增加。准确度的高低不仅与正确读数的概率有关，还与错误读数的可能性有关。为了确保99%的准确度，我们要么必须降低最小值和最大值之间的比率（这样坏的读数就不会那么大），要么降低坏读数的概率。请注意，这些改动只与特定机器有关。这台机器给出了确保预期所需的准确读数4.1.4执行我们的第一个VolumeTracker1将使用两个传感器，它们提供流量读数，并提供诊断信息，说明它们是否损坏。我们将首先考虑传感器，这些传感器可能在任何特定读数上失败，而与任何其他读数无关。我们将考虑具有至少90%可靠性的传感器我们需要使用其中的两个传感器，传感器1a和传感器1b，以提供99%的准确度传感器1b如图5所示，传感器1与之完全相似。我们提出了一个实现VolumeTracker1I的VolumeTracker1，它使用两个传感器，以获得更可靠的读数的流量。这在图6中给出，并使用了图7的Context机器。注意，该实现包含自己的变量rvolume。为了避免使用导入的状态使这个例子复杂化，我们放宽了实现机器不能有自己的状态的常规限制。我们需要证明实现中的轮询操作是规范中的轮询操作这可以通过ma-S. Schneider等人理论计算机科学电子笔记137（2005）183193实现VolumeTracker 1I完善VolumeTracker 1IMPORTSTank，Sensor1a，Sensor1b，ContextVariablesrvolume不变量rvolume：实际初始化rvolume：=0操作poll= VARv1，v2，st1，st2，rflow INP1a：v1，st1-- poll1a;P1b：v2，st2--poll1b;F：rflow-- flow（v1，st1，v2，st2）;R：rvolume：= rvolume + rflow;T：托克端端见图6。 VolumeTracker1I的实现机器上下文操作ff-- flow（v1，st1，v2，st2）=PREv1： REALv2： REAL&st1：STATUSst2： STATUS然后F：如果st1 =断开st2 =断开THENff：：[最小流，最大流] ELSIFst1 =断开st2 = ok THENff：= v2ELSIFst1=okst2=brokenTHENff：=v1ELSIFst1=okst2=okTHENff：=（v1+v2）/2端端见图7。 湍流计算使用第2.2节中给出的[3]的定律来计算概率选择。图6的VolumeTracker11中的轮询操作具有特定的形式P1a; P1b;F;R;T，其中变量v1、 v2、st 1、st 2、r_low都是局部的。我们证明了这个操作等价于特定机器VolumeTracker1中给出的轮询，如下所示：P1a;P 1b;F;R;T={展开P1a和P1b}（S 1 al 0. 9S1ar）;194S. Schneider等人理论计算机科学电子笔记137（2005）183（S 1 bl 0. 9S1br）;F;R;T【第十三条】S 1 al;（S 1 bl 0. 9S1br）;F;R;T0的情况。9⊕S 1 ar;（S 1 bl 0. 9S1br）;F;R;T【第十三条】（S 1 al; S 1 bl; F; R; T 0. 9S1al;S 1br;F;R;T）0的情况。9⊕（S 1 ar; S 1 bl; F; R; T 0. 9S1ar;S 1br;F;R;T）={每个分支中的标准程序代数;删除局部变量}（V 1 aT 0. 9V 1 aT）0.9分（V 1 a）0分。9V1bT）={左参数p的同数}V1 a a a T 0. 9分（V 1 a）0分。9V1bT）【第二十四条】（V 1 a aaT 0. 99V1bT）={定律A，因为V1b±V 1a}（V 1 a aa T 0. 99V1bT）因此，我们得到了机器VolumeTracker1中给出的操作轮询。这表明VolumeTracker11确实提供了VolumeTracker1的实现。4.1.5总结第一个例子说明了几点：• 机器期望表达式的期望值在每次操作发生时都应该是非减的。• 然而，机器期望表达式的实际值可以在某些操作调用中减少（假设其期望值不减少）。• 期望值可以用来表达状态变量的期望值之间的关系，在我们的例子中，根据rvolume的期望值提供了volume的期望值的范围。这是作为机器一致性的一部分进行检查的• 罐值体积的近似rvolume的准确性不仅取决于不正确读数的概率，而且取决于最小流量和最大流量之间的比率，因为这会影响rvolume的最大可能误差。• 概率运算可以使用概率运算的组合来实现。S. Schneider等人理论计算机科学电子笔记137（2005）183195机器体积跟踪器2包括油箱常量低错误，高误差PROPERTIESlowerror：REALlowerror<= 0&higherror：REALhigherror>=0变量rvolume不变量rvolume：实际期望E1：rvolume-A* volume，E2：B * 体积-初始化体积：= 0操作poll=T：tock|| V2a：rvolume：：rvolume+流量+[低误差，高误差] 0.99（+）V2b：rvolume：：rvolume+[minflow+lowerror，maxflow+higherror]端见图8。 第二监测系统bilistic组件（传感器）以我们期望的方式。这样的实现只需要根据操作的机器描述进行检查以进行细化机器一致性检查确保机器操作提供了预期的总体要求。4.2引入误差容限4.2.1质量标准在前面的例子中，正确的读数是完全准确的。 我们现在允许在读数上有一定的误差。具体来说，误差可以是[lowerror， higherror]范围内的任何值。通常情况下，完全没有错误的可能性应该在这个范围内，所以lowerror将是负数，higherror将是正数。修改后的机器如图8所示。适当A和B的计算遵循与第4.1.2节中所示相同的模式。现在必须考虑两个不确定性的来源：V2a中传感器的读数（当E1为低时，它可能是最悲观的）和V2b中的任意读数（当E1为高时，它可能是最悲观的）。这种考虑的组合（召回率低误差是负的，所以A≤1）意味着A被以下两个值所限制1+（低误差/最小误差）196S. Schneider等人理论计算机科学电子笔记137（2005）183和0的情况。99 +（低误差/最大低误差）+ 0。01（最小流量/最大流量）例如，如果min_low = 100，max_low = 400，lowerror = − 10，那么第一个值较低，我们得到A = 0。9. 另一方面，如果lowerror=-0。1，则第二个值较低，我们得到A = 0。9915.在第一种情况下，在任何读数中的可能误差都是最小误差的10%，因此最坏的情况发生在最小误差为最小误差时，最小误差+最小误差相加torvolume：结果rvolume可能会有10%的输出。 另一方面，在一项研究中，在第二种情况下，在所述数据流中的误差可以至多为0。1%，因此V2b（1%的时间）可能引入的误差占主导地位，最坏情况发生在当最大值为最大值时，rvolume仅增加lowerror+最小值时。对期望E2的类似考虑得出，B得到的值是以下两个值中的最大值，第一个值是当E2=max E2时的值，第二个值是当E2=min E2时的值。1+（高误差/最大低误差）和0的情况。99 +（高误差/最低误差）+ 0。01（最大流量/最小流量）在这种情况下，第二个值将始终较高，因此将为B提供适当的值，因为max = low/ min = low1，而higherror/ min = low higherror/ max = low。这告诉我们，最坏的情况总是发生在最小最低的最低，以及最大最低+高错误的错误读数。就确保E2不下降而言，这比最大最小最小最大最小4.2.2实施：传感器该误差可能已包含在质量标准中，因为传感器引入了一些误差。我们可以将这些错误包含在传感器描述中，从而生成新版本的传感器描述。例如，在传感器2b中，我们将误差范围设为[le2b， he 2b]。所得传感器如图9所示。实现VolumeTracker2I将与VolumeTracker1I相同，除了它现在导入传感器2a（具有误差范围[le2a， he 2a]）和传感器2b，而不是原始传感器。在附录B的图B.1中给出，以供参考。S. Schneider等人理论计算机科学电子笔记137（2005）183197机器传感器2bSEES罐常量le2b，he2b属性le2b：REALle2b<= 0&he2b：REALre2b >= 0操作sf，st<--poll2b =S2bl：sf：：flow+[le2b，he2b] ||st：= ok>=0.9（+）S2br：sf：：[minflow+le2b，maxflow+he2b] ||st：=破碎端见图9。机器传感器2b注意，在这种情况下，两个正常工作的传感器的读数可能不在这种情况下，上下文机器指定应该取两个读数的平均值。机器VolumeTracker2I提供了一个poll的实现，假设以下情况成立：[le2a， he 2a]删除[lowerror， higherror]和[le2b， he 2b]删除[lowerror，higherror]。换句话说，误差范围为每个传感器都在体积跟踪器2中给出的用于整体组合的那些传感器内。这方面的证明见附录B。4.2.3总结第二个例子说明了几点：• 我们可以指定流量读数的误差范围。• 这样的范围对操作的期望值有影响：状态更新中的不确定性意味着rvolume和volume之间的关系将变弱。• 可以保证的volume和rvolume之间的特定关系取决于读数的误差范围以及max_flow与min_flow的比值。在某些情况下，每一种都占主导地位。• 流量读数可由误差在规定范围内的传感器实现。4.3删除传感器诊断我们现在考虑传感器不提供显式状态信息的情况在这种情况下，识别错误读数的唯一方法是198S. Schneider等人理论计算机科学电子笔记137（2005）183机器传感器3cSEES罐常量le3c，he3c属性le3c：REALle3c<= 0&he3c：REALre3c>=0操作sc--poll3c =sc：： flow+[le3c，he3c]>=0.9（+）sc：：[minflow+le3c，maxflow+he3c]端见图10。无诊断功能与其他阅读比较。在这个例子中，我们将从传感器到规格：我们将推导出传感器组合提供的规格。4.3.1实施：传感器图10中给出了一个没有关于其状态的诊断信息的传感器。它只提供一个流的读数，没有任何关于其状态的信息为了容忍一个错误的读数，我们需要三个传感器：传感器3a，传感器3b和传感器3c。通过取三个读数的中间值，我们得到了一个准确的读数，只要其中不超过一个出错。这表明图11中给出的实现。我们仍然假设任何单个传感器的读数具有90%的可靠性。4.3.2质量标准事实上，这里的体积跟踪器3I是图12中给出的体积跟踪器3的改进，前提是所有传感器误差都在体积跟踪器3中给出的误差范围内，例如：[le3，he 3][lowerror， higherror].对于VolumeTracker3，对E1的方差进行标准计算，我们发现，我们可以获得的A的最佳（最高）值（使期望值E1得以保留）是以下最小值：1+（低误差/最小误差）和0的情况。972 + 0。028（最小低/最大低）+低错误/最大低S. Schneider等人理论计算机科学电子笔记137（2005）183199实现VolumeTrackerI3完善VolumeTracker3进口罐、传感器3、传感器3b、传感器3c变量rvolume不变量rvolume：实际初始化rvolume：=0操作轮询= VARv1、v2、v3在端v1--poll3a;v2-- poll3b;v3--poll3c;rflow：= median（v1，v2，v3）; rvolume：= rvolume +rflow; tock端见图11。 VolumeTrackerI3的实现机器体积跟踪器3包括油箱PROPERTIESlowerror： REALlowerror = 0&higherror：REALhigherror>=0变量rvolume不变量rvolume：实际期望E1：rvolume-A *volume，E2：B * 体积-初始化体积：= 0操作投票=Tock|| S3a：rvolume：=rvolume+flow+[lowerror，higherror] 0.972（+）S3b：rvolume：：rvolume+[minflow+lowerror，maxflow+higherror]端见图12。第三监控系统规范类似地，我们可以获得的B的最佳（最低）值是1+（higherror/max_low）的最大值200S. Schneider等人理论计算机科学电子笔记137（2005）183和0的情况。972+ 0。028（最大流量/最小流量）+（高误差/最小流量）其中第二个将始终是最大值，因为max = min。这种情况类似于第4.2.2节中考虑的前一个例子，但现在错误读数的概率为0。028不是0 01.因此，对rvolume和volume之间关系的预期相对较弱，因为最大流量和最小流量之间的比率具有更大的权重。例如，考虑下面的情况：max_low = 400，min_low = 100，higherror= 1，lowerror = − 1。由于期望值E1=rvolume−A×volume不能减少，无论Wavelow的值是多少，我们都要考虑两个极端• 如果rvolume=min_low，则volume增加min_low，rvolume可以增加的最小值是min_low+lowerror。因此，在这种情况下，我们得到A = 0的可能值。99.• 如果最小流量=最大流量，则音量增加最大流量，如果至少有两个传感器出错（发生概率为0），则rvolume可以增加的最小值为最小流量+最小误差。028），否则max_low+lowerror。因此，最悲观的期望给出了A = 0的可能值。9765. 在这里，max_low和min_low之间的比率比min_low和lowerror之间的比率对rvolume可以下降的量的贡献更大，我们得到的值为0。9765为A。我们还要求期望E2 =体积−B×r体积不能减小。这里我们关注的是体积可以超过rvolume的比例，最坏的情况总是发生在当最小体积=最小体积时。在在这种情况下，读数最坏可能是max_low + higherror（概率为0）。028），否则为min_low+higherror。这产生了至少为10个。085如果E2的期望值不降低。 这是一个误差幅度为8. 百分之五4.3.3总结此版本的罐监控系统考虑了不提供其状态反馈的传感器版本因此，传感器我们考虑了一种使用三个传感器的实现方式，如果最多一个发生故障，则可以获得准确的读数。我们发现，如果每个传感器至少有90%的可靠性，那么组合至少有97.2%的可靠性。S. Schneider等人理论计算机科学电子笔记137（2005）183201提供准确的读数。这使我们能够构建由实现保证的规范。这又使得能够建立volume和rvolume5讨论本文中的案例研究展示了如何应用概率B来指定和细化一个自然包含概率和非确定性行为的系统，并强调了在此过程中可能出现的一些问题。我们考虑了一系列的情况。在第一种情况下，我们考虑了传感器读数完全准确或完全任意的简单情况，传感器指示它们是否正确工作。这使得能够给出系统的值rvolume的准确性的值从本质上讲，准确性是通过允许非确定性的最坏情况来计算的，这与语言语义中反映的非确定性的恶魔方法一致。我们得到了预期的结果，即最大和最小带宽之间的比值越大，我们可以预期的值就越不准确。在第二种情况下，即使传感器正常工作，我们也允许读取值存在一定的误差范围这种额外的不确定性也进入了计算，以确定rvolume的准确度水平，我们再次看到，对于流量读数和可能的流量，可能性范围越宽，系统记录液体体积的准确度水平就越低在第三种情况下，传感器不再提供它们是否给出正确读数的直接指示，因此有必要使用三个传感器并比较读数以推断哪些值最有可能是正确的。在这个例子中，我们从实现到规范，首先获得传感器组合提供的可靠性，然后计算系统可以提供的准确性水平所有这三种情况都是使用一台只有单一操作的机器建模的，该机器同步了真实坦克的更新和监控系统的更新。虽然案例研究是一个简单的系统，本文只探讨了一些有趣的行为，可能会出现在这样的系统，和许多其他的场景仍然准备探索。例如，我们可能希望对传感器进行建模，这些传感器一旦发生故障，202S. Schneider等人理论计算机科学电子笔记137（2005）183休息这样的建模很可能需要一些辅助变量来跟踪传感器再次正确工作之前所剩的时间，而在概率B中对这样的系统进行建模的最佳方法还远不清楚。确认我们非常感谢Neil Evans、Carroll Morgan和Annabelle McIver对这项工作的评论和讨论。这项研究是在Ken Robinson和Thai Son Hoang于2003年7月访问伦敦大学皇家霍洛威学院期间发起的引用[1] J-R 阿布里尔B书：将程序转化为意义。剑桥大学出版社，1996年。[2] T.S. Hoang，Z. Jin，K. Robinson，A. McIver ，和C. Morgan.概率机器的概率不变量。ZB2003：第三届B和Z用户国际会议，LNCS第2651届会议。Springer，2003年。[3] A. McIver和C. Morgan. 概率系统的抽象、精化与证明Springer，2004.[4] A.麦基弗角摩根和T. S.黄可能终止于B。ZB2003：第三届B和Z用户国际会议，LNCS第2651届会议。Springer，2003年。[5] C. 摩 根 A.McIver 和 K. 赛 德 尔 可 能 是 同 品 种 变 压 器 。 ACM Transactions on ProgrammingLanguages and Systems，18（3）：325[6] C. Morgan. 广义替代语言扩展到概率程序。在B’98: the 2nd International B ConferenceSpringer，1998年。[7] S.施耐德B方法：介绍。帕尔格雷夫，2001年。A机器可读pGSL该表给出了本文中AMN描述中使用的pGSL中语句的格式。关于机器可读AMN的更全面的说明，请参见[1，7]。