安全电子投票模型的随机模拟技术

理论计算机科学电子笔记151（2006）5-25www.elsevier.com/locate/entcs随机模拟方法在安全电子投票模型杰里米·T 布拉德利1英国伦敦帝国理工学院计算机系Stephen T. 吉尔摩2苏格兰爱丁堡大学计算机科学基础实验室摘要我们展示了一种新的模拟技术，分析大型随机过程代数模型，将其应用到一个安全的电子投票系统的例子。通过用连续等价物近似PEPA模型的离散状态空间，我们可以从化学和生物建模中借鉴速率方程模拟技术，以避免直接枚举所涉及的巨大状态空间。我们使用随机模拟技术，以提供轨迹的过程中的值的时间序列，代表在一个特定的状态下的组件的数量。使用这种技术，我们可以得到模拟结果的模型超过10000个国家在短短几秒钟内。保留字：随机过程代数，PEPA，价值过程时间序列，安全电子投票1介绍投票是民主进程的基础。所有的投票系统都是不可靠的，但电子投票系统的问题比任何一个狂热者所能预料的都要严重。这些措施包括在选举日投票过程中返回错误的计票结果，将选民和选票数据库暴露在互联网上[1]。这些错误和一系列其他错误的净效应是破坏选民对电子投票系统的信心[2]。当计算机系统中的错误变得太成问题而不能忽视时，计算机科学中的经典解决方案是通过对系统进行建模来解决问题，1电子邮件地址：jb@doc.ic.ac.uk2 电子邮件地址：stg@inf.ed.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.03.0096J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）良好的形式化描述语言和推理这些模型。这赋予了抽象和清晰的好处，并将话语建立在坚实的基础上。这种澄清是通过集中在用于实现安全投票过程的协议来诸如定理证明[3]、模型检验[4]和静态分析[5]等方法在[3，4，5]中考虑的应用涉及安全协议的定性评估，而在定量方面则保持沉默在电子投票领域，这是一个明显的遗漏：选举必须及时进行。在[6]之后，我们考虑了安全电子投票协议的定量分析。在[6]中，我们使用HillstonPEPA是一个著名的马尔可夫随机过程代数。不熟悉PEPA的读者可以参考附录A中的介绍[7]和语言的正式定义。PEPA语言中模型的含义由交错（小步）结构化操作语义定义。任何进程代数模型的交错语义解释都容易导致一个潜在的致命问题：状态空间爆炸。状态空间的大小作为一个整体是由该模型中的顺序组件的局部状态空间大小的产品的大小的限制。甚至如果可以找到状态空间的紧凑表示（例如，聚集表示[8]或MTBBD编码[9]），则随机过程代数模型通常还需要存储模型状态空间上的概率分布。这个向量的紧凑表示通常不能找到，即使可以找到状态空间。如[6]所述，安全电子投票模型的底层CTMC的数值解不能针对现实规模的选民群体进行。因此，为了在这个问题上取得进展，模型评价中最重要的问题正在扩大，我们尝试了一种不同的方法：随机模拟。在计算系统生物学[10，11]和随机过程代数领域中开发的随机模拟方法，如Priami据我们所知，目前的工作是第一篇论文应用随机模拟方法在计算系统生物学的随机过程代数性能模型的计算应用。这不是一个完全简单的域的变化，我们必须实现自定义速率函数来模拟计算系统的行为，这些系统具有与生物系统不同的相互作用特性J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）72相关工作已经存在许多PEPA语言的模拟器[14，15，16，17]，因此在本节中，我们将我们的新随机模拟器实现与其他实现进行比较。第一个为PEPA语言实现的模拟器是Clark这是一个建立在SimJava上的原型离散事件模拟器[18]，它直接解释PEPA模型。它被用于研究原始的PEPA模型和实验性的基于时钟的PEPA语义，该语义使用一般分布代替指数[19]。PEPAroni模拟器记录了模拟生成的模型状态，以及这些状态出现的频率，以供以后的模型分析使用，并允许将模拟器的结果与马尔可夫链的数值解进行比较（如果该解可用）。Stathopoulos [15] 扩 展 了 PEPAroni 模 拟 器 ， 并 将 其 纳 入 PEPA 模 拟 器 中 。PEPAroni模拟器被证明是研究一般分布的一个非常有用的工具，但当应用于纯马尔可夫PEPA模型时，用户体验很差。模拟器会运行很长时间，但仍然不能生成模型的所有状态，即使是非常小的模型（少于100个状态）。求解马尔可夫链总是比模拟快，即使计算瞬态解而不是稳态概率分布。Clark为PEPA实现了另一个模拟器，包括他的PEPA模型editorin to heMo？biusmulti-paradigmulti-forrmalismodellingplat f orm。M？obius模拟器使用的评估方法比SimJava在PEPAroni下使用的方法具有更高的效率，但在模拟开始之前，它仍然解释模型，而不使用模型聚合。Powell [17]采用了另一种实现方法，他通过将模型编译成Java应用程序来模拟PEPA模型，并执行它以收集模型中每个活动的使用统计数据。没有表示完整的状态空间，这有利于模型的可扩展性。然而，这具有随之而来的缺点，即所获得的性能结果不能直接与通过数值解获得的结果相比较，如果可以这样做的话。相反，导出的结果需要从数值解计算，以便与模拟结果进行比较，从而验证模拟器。这种实现策略具有其他缺点，因为限制因素可以是在下面的Java虚拟机上可以支持的同时执行线程的数量在计算生物学中，一种用于价值过程分析的替代方法是将模型表示为一系列耦合的常微分方程（ODE）的数值积分这种常微分方程的使用在生物建模中被称为在这里出现的关于反应动力学的一些相同问题也出现在ODE设置中，如[20]中所讨论的8J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）defdefdefdef3随机模拟随机过程代数是组合建模形式主义，因此似乎最适合尝试利用对聚合的接受性，这是由组合性决定的。随机模拟方法被开发用于分析涉及大量物种的具有复杂反应动力学的化学反应。没有试图在分子水平上追踪个体：相反，浓度是通过连续变量近似的。这提供了对模拟的当前状态的紧凑描述，作为测量每个物种的数量的实值变量的向量。当模拟化学反应时，常用的反应动力学是质量作用，其中化合物反应的反应速率与所涉及的物质的量的乘积成比例。PEPA中没有使用质量作用动力学，它定义了表观速率的概念，以保持相互作用组分具有不能超过的有限容量的在PEPA实现（如PEPA算法[21]和Imperial PEPA算法（ipc）[22]）使用近似值来降低表观速率评估成本的情况下，实现者有责任了解近似值的影响[23]。出于这个原因，当应用随机模拟方法的PEPA模型，我们计算的同步活动的速率的方式尊重PEPA语义的表观速率和有界容量。这取决于对总汇率3的函数表达式的使用，如下节所述这种形式的模拟是从基于状态空间的模型分析方法的重大范式转变，该方法跟踪每个个体的每个状态变化。在连续变量的使用上，随机模拟也与离散事件模拟形成对比，后者处理个体数量的离散值表示。传统模拟方法中最接近的比较可能是模型的聚合表示的Monte Carlo Markov Chain模拟4方法在本节中，我们将通过一个简短的示例概述从PEPA模型生成模拟的方法。 下面是一个模拟的PEPA描述- 多客户端和多服务器模型：Client=（compute，T）. 客户端1客户端1 =（延迟，μ）。Client Server=（compute，λ）. 服务器1服务器1=（recover，v）。服务器3 也就是说，将表观速率表示为组分计数和作用速率的函数。J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）9模型的系统方程为：（客户端|| · · · ||客户端）D（服务器||· · ·||服务器）“我的天，N{compute}“我的天，M这描述了等待在服务器上放置计算操作的客户端，然后在尝试另一个服务器计算之前看到延迟。在经历恢复阶段之前，服务器控制交互中的计算速率λ。只有在恢复之后，服务器才能通过再次启用计算操作为另一个客户端提供服务。系统方程描述了系统是如何组成的。有N个并行客户端进程与M个并行服务器组件在计算操作上协作。4.1速率方程本文简要介绍了速率方程的表示法，这些速率方程在很大程度上是基于化学反应方程的。R演化，nA−→mB：n对应于A的copies可以演化为prod的copies-乌特湾 一旦系统中存在n个或多个拷贝的A，该反应就被启用。如果有不止一个被激活的反应，那么它们就会竞相成为第一个进化的反应（一种隐含的竞争选择）。组合，nA+mB：这将A和B的多个拷贝指定为反应物或产物。如果这发生在进化的左手边，那么至少需要n个拷贝的A和m个拷贝的B来实现反应。这个+操作符与PEPA的+操作符不同：实际上，在PEPA术语中，这将表示A组件和B组件之间的协作反应物中A和B的多重性，称为反应的化学计量，可以用来表示PEPA在共享作用上的合作，如在：（AD ···D A）D（BDDB）`{a}{a}xn{a} `{a}{a}xM其中所有n个A组件和所有m个B组件必须同时启用a动作，以便进行合作。4.2仿真生成我们的目标是生成一个模拟文件，输入到Dizzy工具[24]中，该工具传统上用于模拟化学和生物速率反应。在这样做的时候，我们需要维护PEPA语义，这些语义是从多年的计算系统性能研究中收集到的幸运的是，Dizzy工具为我们提供了从标准化学建模范式的质量作用语义迁移的灵活性。这个问题只考虑了模型中的合作行为，在这种情况下，它会影响计算动作的总体速率。生成Dizzy模拟描述的过程如下：10J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）确定状态更改操作。我们有三个这样的动作来修改客户端和服务器组件的状态：延迟，计算和恢复。这些作用成为速率方程的标签。识别源/目标组件状态。对于每个操作，确定将由该操作发生所影响的组件的源/目标状态。例如，延迟动作具有源状态Client1和目标状态Client。也就是说，延迟动作的发生将减少COM的数量。客户端1状态下的ponents，并增加客户端状态下的数量。在有相互作用的地方，我们将有多个源状态和可能的多个目标状态。计算的源状态是Client和Server，目标是Client1和Server1。这意味着在反应或交互发生之前，客户端和服务器状态的组件必须同时存在。结果是客户端1和服务器1的状态分量的比率相同计算反应速率。对于每个动作，我们根据能够执行该动作的组件数量例如，对于动作延迟，如果有n个（客户端1）组件处于客户端1状态，则观察到的动作延迟的总体速率将是n（客户端1）μ。将该源/目标状态提取与速率计算相结合，我们得到图1的等效速率方程。客户端+服务器θ（n（Client））n（Server）λ−→客户端1+服务器版本1n（客户端1）μ客户端1−−→客户端n（服务器1）v服务器1−−→服务器其中θ（x）= 1，如果x>0，否则0。图1.一、多服务器/多客户端PEPA示例作为一组速率方程。图1中的计算动作的θ（n（客户端））n（服务器）λ速率的解释可以解释如下。考虑C客户端使用S服务器来执行计算操作。同步计算活动的总体速率（由PEPA语义根据从协作客户端和服务器提取的表观计算速率定义）由下式给出：⎧λ：C >0min（CT，Sλ）=C= 0=θ（C）Sλ（1）因此，我们可以使用θ（·）函数来计算客户端的数量，以得到标准最小公式的简化表达式。这捕获了模型中的被动通常，我们将应用标准的表观速率公式，因此在主动同步的情况下，我们将使用min（Cα，Sβ）的组合速率函数，用于分别以速率α和β与S服务器协作的CJ.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）11//初始化组件数量Client =N;return M;return 0;return 0;//速率方程延迟，客户端1->客户端，[客户端1 * mu];恢复，Server_1 -> Server，[ Server_1 * nu];计算，客户端+服务器->客户端_1+服务器_1，[ theta（Client）* Server * lambda];图二、多客户端/多服务器示例的Dizzy文件描述4.3头晕格式在得到PEPA模型例子中各个行为的速率方程后，将其转换为Dizzy文件是一个简单的过程这种转换在PEPA中实现。生成的文件如图2所示。在Dizzy格式中，所有速率方程都由动作标记名字在给定的状态n（X）中的分量的数量由初始时的X给出sation块和速率描述。 速率描述本身在方括号[]中给出。5PEPA模型在本节中，我们提出了一个模拟模型的投票协议表示在PEPA。与[6]的模型有许多重大区别。(i) 我们只对一轮选举进行建模，因为我们正在进行价值过程时间序列模拟，而不是执行稳态计算。在[6]中，投票过程被循环，以便模型定义遍历马尔可夫链。在这里，我们有一些组件，它们执行指定的活动，然后终止。我们使用[25]中PEPA中终止进程的定义（用Stop表示）因此，这个模型的终止状态是一个混乱的状态，由选举的终点决定：一些选民可能永远不会登记，一些人可能无法确认他们的选票被正确记录，等等。这与为了使系统不可约或强连通而要求整齐终止（在[6]中需要有意义的稳态计算）形成对比。12J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）defdefdefdefdefdefdefdefdefdefdefdefdefdefdefdef(ii) 与[6]相反，我们使用控制反转模型来控制过程，以确定从一个阶段到下一个阶段的选举进度这导致了模型中对投票者、管理员、收集者和计数器的描述的简化。选择从这些组成部分的定义中移除，并进入元级别的控制过程因此，这两个PEPA模型不存在强等价互模拟关系[7]，而是同一系统的替代模型。5.1在选举我们不提供这里使用的投票方案的完整描述，而是只提供一个大纲，并请感兴趣的读者参考[26]或[6]。电子投票可以分为准备阶段，通过联系管理员结束，通过联系收集者结束投票，以及可能导致或可能不会导致上诉的检查在准备阶段，投票者盲法用于确保选票的匿名性，数字签名用于确保认证。将盲态、签名的选票发送给管理员进行检查，并返回验证。投票人打开这个并检查签名。投票阶段的最后一项活动是将选票发送给收集者。计票开始，当计票员公布选票列表时结束如果选民的投票没有出现在名单上，他们可以在这个阶段提出上诉投票人0投票人0 1投票人0 2投票人0 3投票人0 4投票人0 5选民表决器1投票人1 1投票人1 2投票人1 3投票人1 4投票人2投票人2b第三投票人投票结束=（choose，c1）. 投票人0 1=（bitcommit，b1）. 投票人0 2=（blind 1，b2）。投票人0 3=（blind 2，b3）。投票人0 4=（voter sign，s1）. 投票人0 5=（sendA，s2）。选民0 5b=（sendV，T）。表决器1=（unblind 1，u1）. 投票人1 1=（unblind 2，u2）. 投票人1 2=（verify1，v2）. 投票人1 3=（verify2，v3）. 投票人1 4=（sendC，s6）。投票人2=（检查失败，p × c4）。第三投票人+（check succeed，（1 − p）× c4）. 选民2b=（sendCo，s7）。投票结束=（appeal，a1）. 选民2b=停止J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）13defdefdefdefdefdefdefdefdefdefdefdefdefdefdef5.2管理员的作用一旦选民登记，管理员就变得活跃，并将他们带到他们能够投票的地方。这涉及检查和核实投票资格，然后对选票进行数字签名。管理员最终将盲选票发送回选民。管理员2管理员3管理方4管理员5管理员6管理员7管理员完成=（sendA，T）。管理员2=（检查1，c2）。管理员3=（检查2，c3）。管理方4=（verify，v1）. 管理员5=（admin sign1，s3）。管理员6=（admin sign2，s4）. 管理员7=（sendV，s5）。管理员完成=停止5.3收集选票选票由一个收集员接收。他们的作用是在投票阶段检查选票是否由管理员正确签名如果这一点得到验证，则收集操作员将投票添加到列表中，并使用唯一的参考编号对其进行标记。这份名单将在收集期结束后公布收集器0收集器 0a收集器 0a1收集器 0a2收集器已完成=（sendC，T）。收集器0a=（集电极验证1，v4）。收集器0a 1=（集电极验证2，v5）。收集器0a 2=（add，a2）. 收集器完成=停止5.4计票计票人员的责任是检查选民在选举过程的第一阶段选择的策略是否有效，并为结束选举的最后计票做好准备计数器1柜台1a=（sendCo，T）。柜台1a=（check strategy，c5）. 计数器完成14J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）defdefdef计数器完成=停止5.5选举过程选举过程本身与模型中的其他过程具有不同的特征选举本身不是选举进程中的一个行为体：而是存在于控制模拟阶段的虚拟进程一级，可被视为选举法律框架的一部分。与PEPA网络中的网络结构[27]和PEPA模型中用于见证事件的随机探针[28]都有相似之处，但控制过程与两者都不同，因为它将投票过程分为几个阶段（准备，投票，计数和完成），允许在每个阶段选择活动，并在不合适的地方禁止它们随机探针观察性能重要事件。元级控制过程允许性能重要事件，并生成模拟控制事件（结束一个阶段，开始另一个阶段，并终止整个模拟）。使用扩展了功能速率的PEPA[29]，可以以替代方式实现相同的效果。选举过程将是模型全局状态空间上的一个函数，允许在适当的时间采取适当的行动，否则不允许采取行动。我们在这里选择将该函数表示为PEPA组件，并观察到θ函数通常是实现功能速率的非常合适的方法选举筹备选举投票=（choose，T）. 选举筹备+（bitcommit，T）. 选举筹备+（盲1，T）。选举筹备+（盲态2，T）。选举筹备+（voter sign，T）. 选举筹备+（sendA，T）. 选举筹备+（勾选1，T）。选举筹备+（勾选2，T）。选举筹备+（verify，T）. 选举筹备+（管理员符号1，T）。选举筹备+（管理员符号2，T）。选举筹备+（sendV，T）。选举筹备+（shA，er）。选举投票=（非盲1，T）。选举投票+（未设盲2，T）。选举投票+（验证1，T）。选举投票J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）15defdefdef选举计票选举结束+（验证2，T）。选举投票+（sendC，T）. 选举投票+（集电极验证1，T）。选举投票+（集电极验证2，T）。选举投票+（add，T）. 选举投票+（shC，er）. 选举计票=（检查失败，T）。选举计票+（check succeed，T）. 选举计票+（sendCo，T）。选举计票+（上诉，T）。选举计票+（检查策略，T）。选举计票+（final publish，er）. 选举结束=停止我们所分析的系统是由以下组件中的上述顺序组件组成的选举筹备DL其中：选举人=选民def[N]D选举机构M以及：选举机构=收集器0 [N]||计数器1 [N]||管理员[N]N= 10，000L={choose，bitcommit，blind1，blind2，voter sign，sendA，sendV，unblind1，unblind2，verify1，verify2，sendC，check fail，checksucceed，sendCo，appeal，blind shA，check1，check2，verify，admin sign1，admin sign2，collector verify1，collector verify2，add，callshC，检查策略，最终发布}M={sendA，sendV，sendC，sendCo，sendshC}5.6仿真结果图3至图9显示了从投票模型的模拟中提取的信息在每种情况下，组件的导数（组件的可能后续状态）的数量随时间而变化。为了不使图表过于混乱，我们只显示了定性上不同的导数迹线。在图3中，我们为Administrator组件的不同衍生物提供了一系列模拟第一个组件图是没有看到过渡sendA出Admin的Admin-istator组件的数量。016J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）处于派生状态的管理员组件数10000800060004000200000 5 10 15 20 25 30时间t图三. 管理员组件处于派生状态的收集器组件数10000800060004000200000 5 10 15 20 25 30 35 40时间t见图4。 收集器组件伊斯特拉州。在管理员等待与选民群体的第一个sendA行动同步时，有一个轻微的延迟，但此后人数几乎呈指数级下降。衍生物管理员2和管理员7是组件的瞬态，因此这里的种群几乎接近0。组件的最后一个状态（也是吸收状态）是AdministratorFinished（管理员已完成），这将结束此跟踪中的大部分填充。在定量解释这些结果时，我们可以说，在17秒内，95%的管理员组件达到了管理员完成的吸收状态。类似地，定量的时间性陈述可以从本研究中的其他随机模拟中得出关于给定及时结果的可能性的进一步信息可以从多个模拟中收集，这将产生额外的误差条信息。图4跟踪了Collector组件衍生物的数量随时间的变化，发现了与Administrator类似的种群动态唯一的区别是延迟时间长得多，在这种情况下，在离开初始收集器0这取决于sendC操作，该操作将在Voter生命周期的后期出现，管理员管理员_2管理员_7管理员_已完成Collector_0Collector_0a1Collector_FinishedNumberNumberJ.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）17微分状态中的计数器组件数10000800060004000200000 10 20 30 40 50 60 70 80时间t图五. 计数器组件衍生状态中的选举分量1.41.210.80.60.40.200 5 10 15 20 25 30时间t见图6。 选举组件启动收集器进程。类似地，图5跟踪计数器分量导数随时间的数量。这里唯一感兴趣的是计数器0分量的迹线的非常急剧的下降，这与先前分量的平滑下降不同。我们将此归因于图6中所示的Election组件，该组件控制选举的阶段并具有方齿轮廓。由于将选票发送到计数器并启动计数过程的sendCo操作与Election组件的最后阶段的启动密切相关，因此我们也可以在计数器组件中看到这种急剧的衍生变化的复制。表决器组件的模拟如图7和图8所示。图7显示了表决器到派生表决器1的平滑演变。图8显示了从Voter到VoterFinished整个演化过程中的关键衍生物。同样，导数Voter1和Voter2的曲线结束处的急剧导数变化是由于与控制Election组件的同步。选举和选民之间的这种密切关系可以在图9中更密切地看到，该图显示了同一模拟中的选民和选举计数器计数器_2计数器_完成选举_准备选举_投票选举_计票选举_结束NumberNumber18J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）派生状态中表决器组件的数量10000800060004000200000 5 10 1520时间t25 30见图7。 模拟Voter组件早期演变为Voter1派生状态中表决器组件的数量1200010000800060004000200000 10 20 30 40 50 60时间t见图8。 模拟表决器组件从表决器0到表决器的不同相位完成显然，选民1和选民2阶段的终止归因于选举组件在其状态分别更改为选举投票和选举计数时规定的选举的该阶段的超时。最终选举阶段的结束不会被选民看到，因为它关系到计票的完成选票6执行我们通过扩展开源Dizzy模拟和分析平台[24]，使用我们预先存在的PEPA分析工具PEPA扩展器[21]，实现了我们的新型PEPA随机模拟器。Dizzy是一个带有图形用户界面的Java应用程序，而PEPA则是一个用函数式编程语言Standard ML实现的命令行我们以一种不寻常的方式将这两个工具结合在一起，通过使用MLj编译器将PEPA编译器的ML版本编译为Java字节码，该编译器针对JVM。投票者0投票者0_4投票者0_5b投票投票0投票1投票者2投票者_完成NumberNumberJ.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）19选民对选举状态的导数数10000800060004000200000 10 20 30 40 50 60时间t见图9。选民和选举组件的联合模拟，其中选民阶段遵循选举Dizzy有自己的建模语言，也支持其他建模语言，包括著名的系统生物学标记语言[30]。通过向Dizzy添加PEPA模型，现在可以在Dizzy上评估PEPA模型，并且因为存在从UML到PEPA的映射[31]，所以也可以使用UML建模并使用Dizzy作为分析工具。扩展的Dizzy平台的示意图如图10所示。⇒⇒⇒⇒图10个。Dizzy仿真分析平台上的模型处理Dizzy应用程序处理安全电子投票系统的PEPA模型的屏幕截图如图11所示。Gillespie直接法[ 10 ]和Gibson-Bruck法[ 11 ]的随机模拟器Gibson-Bruck算法的反应数为O（log（M）），因此对于具有大量反应和/或物种的模型，它优于Gillespie算法。我们发现，在实践中，我们的模型，吉莱斯皮图12显示了Gillespie直接法模拟参数对话的屏幕截图（回想一下，我们使用Gillespie选举_准备选举_投票选举_计票选举_结束投 票 0投 票 1投票2投票者_完成头晕分析工具语言工具ODE积分器随机模拟器PepaUML头晕SBMLNumberPEPA系列SBML模型翻译器20J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）见图11。 在Dizzy平台上处理PEPA模型。见图12。使用Gillespie直接法设置参数以模拟PEPA模型。 来自Dizzy应用程序的模拟结果可以呈现为在线查看或以机器可处理的格式存储，例如逗号分隔值。当运行时，该实现生成如图13所示的结果。7结论本文的目的是表明随机模拟为分析大型状态空间随机系统提供了新的可能性。通过系统地将随机过程代数模型转换为一组化学速率方程，我们构建了该模型中给定状态下组分数量的连续近似。这给了我们一个优势，即能够运行一个流程模型的仿真，而使用传统的离散事件仿真技术是完全不切实际的。据我们所知，这是第一次，这种风格的J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）21图13岁在Java图形窗口中以交互方式查看Dizzy应用程序的模拟结果在随机过程代数框架内尝试了模拟为了证明这种方法的好处，我们分析了一个具有10，000个选民代理的安全电子投票协议这个系统有大约1011750个国家，因此不适合现有的基于状态的分析或模拟技术。此外，使用这种技术增加代理群体大小几乎没有开销，而是模拟性能取决于模型生成的不同速率方程的数量的对数确认作者要感谢PASM研讨会的匿名评审员，感谢他们提出的有益和建设性的意见。在为PEPA模型生成随机模拟结果的过程中，我们需要扩展来自Bolouri Group，Institute for Systems Biology的开源Java应用程序 Dizzy来自系统生物学研究所的Stephen Ramsey是Dizzy工具的主要架构师，他对我们的问题非常有帮助我们的学生Adam Duguid和Erika Birse实现了Dizzy的扩展，以合并PEPA的功能，我们感谢他们这样做可从www.example.com获得http://www.dcs.ed.ac.uk/pepa。Imperial PEPA过滤器可从www.example.com获得http://www.doc.ic.ac.uk/ipc。Jeremy Bradley 的 部 分 研 究 得 到 了 Nu Kelleld 基 金 会 的 资 助 ， 资 助 号 为NAL/00805/G。引用[1] K.泽特，“怎电 子 投票威胁民主”有线杂志本发明涉及制品，Mar. 2004年http://www.wired.com/news/ee/0，2645，62790，00.html.22J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）[2] “Machine《连线》杂志电子投票专题报道，4月。2005.http://www.wired.com/news/evote/网站。[3] L. C. Paulson，85[4] G. Lowe，93[5] C. Bodei，M. Buchholtz，P. Degano，F. Nielson和H. R. Nielson，2004年[6] N. Thomas， “Performabilityofasecureelectronicvotingalgorithm，”inProceedingsofthefirstworkshoponPracticalApplicationsofStochasticModelling（PASM2004）（J. Bradley和W.Knottenbelt，eds.），（London，England），pp. 81-93，9月2004.出现在ENTCS中。[7] J. Hillston，A Compositional Approach to Performance Modeling。 剑桥大学出版社，1996年。[8] S. Gilmore，J. Hillston，and M. Ribaudo，449[9] M. 夸 特 科 夫 斯 卡 湾 Norman 和 D. 帕 克 ， Field ， P. 哈 里 森 ， J 。 布 拉 德 利 和 U.Harder ， eds. ） ， 卷2324LNCS，（London），pp. 200-204，Springer，2002.[10] D. Gillespie，“耦合化学物种的随机时间演化数值模拟的一般方法”，J. Comp. Phys. 22，pp. 403[11]M. Gibson和J. Bruck，“具有多物种和多通道的化学系统的高效精确随机模拟”，J. Comp. Phys. 104，pp.1876-1889年，2000年。[12] C. Priami，A. Regev，W. Silverman和E. Shapiro，2001年12月25日[13] A. Phillips和L.Cardelli，发表在Transactions on Computational Systems Biology上。[14] G.克拉克，S。Gilmore，J. Hillston，and N. Thomas，1999年2月11日至19日。第十四届英国性能工程研讨会论文特刊。[15] F. Stathopoulos，2001年[16] G.Cl arkandW.Sanders，“I mplle m m m n t in g a s to o ch i c p r o ce s a l g eb r a w ith in th e M？ o b i u s moded e li n g framework ， ”in de Alfaro and Gilmore [ 32 ]， pp.200-215[17] K. Powell，2002年。[18] R. McNab和F. Howell，Pooley和J.Hillston编），(The爱丁堡大学），pp. 219[19] G. 克拉克，代数性能模型的构造和分析技术。博士论文，爱丁堡大学，2000年。[20] A. Benoit，M.科尔，S。Gilmore和J.Hillston，Jarvis和N. Thomas，eds.），IEEE Computer SocietyPress，May 2005.[21] S. Gilmore和J. Hillston，353-[22] J. Bradley，N. Dingle，S. Gilmore和W. Knottenbelt，（G. Kotsis，ed.），（中央佛罗里达大学），页。344-351，IEEE计算机协会出版社，2003年10月。J.T. 布拉德利，S.T.Gilmore/Electronic Notes in Theoretical Computer Science 151（2006）23[23] J. T. Bradley， S. T. Gilmore 和 N. Thomas ， “How synchronization strategy approximation in PEPAimplementations a acquects passage time performance results” ， in Applying Formal Methods ：Testing，P e r for manc e，and d M /E - C omme r c e（EPE W 2004）（M. 你是我的朋友。），v〇l.3236fLNCS，pp. 128- 142，Springer-Verlag，Oct. 2004年[24] S. Ramsey，D. Orrell和H. Bolouri，“Dizzy：大规模遗传调控网络的随机模拟”，J. Bioinf。比较生物学，第3卷，第2期，第100页。415[25] N. Thomas和J.Bradley，Djemame和M.Kara编），（University of Leeds），pp.143[26] A. Fujioka，T.