Circus语言在安全关键型应用中的应用

理论计算机科学电子笔记95（2004）3-22www.elsevier.com/locate/entcs将Circus用于安全关键型应用J. C. P. Woodcock1，2肯特大学计算机实验室英国摘要Circus是一种统一了Z、CSP和精化演算的语言，我们描述了它在安全关键系统开发中的应用。我们用一个片段来展示《马戏团》的描述力。 我们使用Circus的refinement caclus来在开发中带来语义鸿沟，在那里我们消除了一种抽象事件。关键词：编程的统一理论，Z符号，通信顺序进程（CSP），细化演算，Circus，同步协议。1介绍Circus符号[31，33，12，13]用于安全关键系统的开发和验证。它是Z [6，28，29，34]，CSP [15，22]，Z精化演算[7，11]和保护命令语言[14]的语义复合，提供了一个框架来讨论基于状态的反应式系统的正确性;扩展正在开发中，包括面向对象[10]，时间[25，26，27]，概率和锁步同步。在本文中，我们通过讨论一个案例研究来说明Circus的使用：蒸汽锅炉，现在是形式方法的标准基准[5，1，2]。特别是，我们关注一个有趣的“语义鸿沟”。 在CSP中，有时会采用一种抽象，其中原子同步可以是系统范围内的，在许多进程之间，而不是仅限于两个参与者。1WMF' 200 3 F或M M e t h o d s E u rope L ec t ur er r（www.fmeurope.or g）。2电子邮件：J. C. P. kent.ac.uk1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.04.0034J.C.P. Woodcock / Electronic Notes in Theoretical Computer Science 95（2004）3-^我们处理一个简单的例子，这种现象，这有助于显示权力的马戏团2马戏团Circus中的进程是反应性的，封装状态变量;反应性行为使用CSP描述，状态及其转换在Z中描述。《马戏团》特别注重技巧的精炼[8，9，24]。一个目标是使用Circus来计算反应系统，其风格让人想起Back [4]，Morgan [19]和Morris[20]的顺序精化演算作为Circus流程的一个简单示例，考虑银行账户的建模。环境可以通过四个通道与此过程交互：打开帐户;检查当前余额;存款;以及取款。开立账户时，进行初始存款并设定透支限额描述以声明这四个通道及其类型。通道打开：N×N;余额、存款、取款：N该流程由一系列介绍状态和状态上的各种操作的段落组成;这些声明以Z和CSP的混合形式给出，并通过流程的封装来保护其免受外部世界的影响拉伸行为由主作用量给出进程BankAcc=开始stateAcc=^[b：Z; o，f：N|f= o + b]JN|bJ= init b？ oJ=init o？]Init=^[Acc;initb？，inito？：Deposit=^押金？v→b：=b+vN·a≤fb：=b−a）Deduct=^（a：Wi thd raw=^Wi thd raw？v→Deduct（v）平衡 = 平衡！b→跳过主要端开着吗（init b，init o）→Init;µX·（存Q取 Q余额）;X^J.C.P. Woodcock / Electronic Notes in Theoretical Computer Science 95（2004）3-5银行账户的状态包含余额b、透支限额o和可用资金f，可用资金f总是固定为余额和透支限额之和。o的值是一个极限，从这个意义上说，f永远不能变成负数。主要行动是确保交流-计数在使用之前被打开。环境必须提供初始余额和透支限额，然后根据初始化模式Init更新状态。请注意，通信绑定的变量（init b和init o）被称为Init的输入。接下来，该过程反复向环境提供操作选择：存款、取款或检查帐户余额。存款操作由存款通道上的通信激活;余额根据ingly。 Withdraw与此类似，只是该操作使用了另一个参数化的actionDeduct，其中包含一个保护：如果要扣除的金额大于可用资金，则操作死锁。这个反应行为的例子是不可能用牛津风格的Z来表达的[34]。Circus [33]的语义遵循Hoare& He的程序设计统一理论[ 16 ]：语言中的每个构造都以塔斯基关系演算的字母扩展中的谓词风格被赋予指称语义。该语言对应于他们在命令式、反应式子理论中的模型，并为广泛的精化演算提供了设置3安全关键应用：蒸汽锅炉在[5]中给出的问题是对蒸汽锅炉进行建模，其中水以测量的速率从锅炉中移除，并由四个泵的动作来代替，所述泵从蓄水池中输送供给。这些装置是核反应堆系统的重要组成部分。蒸汽锅炉的控制器的任务是将锅炉的水位保持在范围N1内。.N2，并关闭系统，如果有一个风险，水位可能会超出较宽的界限M1。. M2。如果超出了较宽的界限，那么就有可能使锅炉溢油或使其烧干，这两种情况都可能导致事故，造成不可接受的后果。在[32]中，马戏团被用来描述蒸汽锅炉。在那篇论文中，在处理来自传感器的复杂数据的消息和控制锅炉操作的更简单的有限状态机之间进行了有趣的分离，以一种让人想起抽象解释的方式。这将验证控制器接口的问题验证其正确性。在本文中，我们使用基于O'Halloran [ 21 ]的形式化在他的工作中，识别关键需求的方法是表达6J.C.P. Woodcock / Electronic Notes in Theoretical Computer Science 95（2004）3-功能要求作为“如果a，则b“形式的触发规则由这些触发规则定义的隐式推断引擎是非单调的，因为随着系统的发展，它必须忘记先前推断的事实。蒸汽锅炉厂的模型和推理机共享通信信道，其表示与真实系统中的致动器和传感器的通信。该设备由许多组件组成，我们简要介绍其中一些组件：蓄水池，锅炉和传感器。水库是水泵供水的水体模型并且根据系统的动力学，锅炉通过加热变成蒸汽。首先，水体中的量，即状态变量L，被设置为N1和N2之间的任意初始水平。工艺用水=开始主varset：PSource，L：N·set：= Source; L：∈N1.. N2;µX·minLmaxwrite？<

下载后可阅读完整内容，剩余1页未读，立即下载