首页/论文/1106.4098

arXiv 1106.40982011-06-21cs.LOcs.SE

事件B细化的CSP解释

A CSP Account of Event-B Refinement

Steve Schneider, Helen Treharne, Heike Wehrheim

备注：: In Proceedings Refine 2011, arXiv:1106.3488
发表信息：: EPTCS 55, 2011, pp. 139-154
DOI：: 10.4204/EPTCS.55.9

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

事件B通过细化为逐步的系统开发提供了一个灵活的框架。该框架支持以下步骤：（a）细化事件（逐个），（b）拆分事件（逐个），以及（c）引入新事件。此外，在每一个步骤中，事件都可能被预见或收敛。所有这些步骤都附有确切的举证义务。尽管如此，仍然不清楚Event-B机器和它的细化之间的确切关系-在面向行为的语义方面。在本文中，我们给出了CSP帐户的事件-B细化，与治疗的第一次分裂事件和预期的事件。为此，我们定义了一个CSP语义的事件-B，并显示如何不同形式的事件-B细化可以被捕获为CSP细化。

英文摘要：

Event-B provides a flexible framework for stepwise system development via refinement. The framework supports steps for (a) refining events (one-by-one), (b) splitting events (one-by-many), and (c) introducing new events. In each of the steps events can moreover possibly be anticipated or convergent. All such steps are accompanied with precise proof obligations. Still, it remains unclear what the exact relationship - in terms of a behaviour-oriented semantics - between an Event-B machine and its refinement is. In this paper, we give a CSP account of Event-B refinement, with a treatment for the first time of splitting events and of anticipated events. To this end, we define a CSP semantics for Event-B and show how the different forms of Event-B refinement can be captured as CSP refinement.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

CSP-Agda的跟踪和稳定故障语义

Trace and Stable Failures Semantics for CSP-Agda

CSP-Agda是一个库，它使用共归纳数据类型在交互式定理证明器Agda中形式化进程代数CSP。在CSP-Agda中，CSP过程是一元形式的，支持过程的模块化开发。本文在CSP-Agda中实现了CSP的两个主要模型：跟踪和稳定故障语义，并定义了相应的精化和等价关系。由于一元设置，需要进行一些调整。作为例子，我们证明了外选择算子w.r.t. CSP-Agda中的跟踪语义，以及对W.R.T.稳定失效语义是一个偏序。所有的证明和定义都在Agda中进行了类型检查。代数定律的进一步证明将在CSP-Agda存储库中提供。

2017-09-14cs.DCcs.LOcs.PL

从因果语义到持续时间时间模型

From Causal Semantics To Duration Timed Models

交错语义与动作细化和持续时间动作都不兼容。由于许多真正的并发语义是一致的w.r.t.行动细化，特别是因果关系和最大化的，这给我们提出了挑战，研究密集的时间行为-其中的行动是任意固定的持续时间-在因果关系语义的Da Costa。我们扩展了因果转移系统的时钟和时间约束，从而我们得到了一类时间自动机的动作不需要是原子的。我们定义了一个实时的扩展的形式化描述技术CSP，称为持续时间CSP，归因于持续时间的行动。我们给出了duration-CSP的操作时间因果语义及其在时间因果变迁系统类上的指称语义。之后，我们证明了这两个语义是等价的。最后，我们扩展的持续时间CSP语言的细化操作$ρ$ -允许替换一个动作的过程-并证明它保留了定时因果互模拟。

2010-04-13cs.LO

并发模型之间的转换

Translating between models of concurrency

Hoare的通信顺序过程（CSP）承认与van Glabbeek频谱密切相关的语义模型的丰富宇宙。在本文中，我们研究有限观测模型，其中至少有六个已确定的CSP，即痕迹，稳定故障，复活，接受，拒绝测试和有限的线性观测。我们将展示如何使用最近推出的\emph{priority}运营商转换到跟踪细化（语言包含）测试在这些模型中的细化问题。此外，我们能够将其推广到任何（理性的）有限观测模型。除了理论上的兴趣，这是具有实际意义的，因为国家的最先进的细化检查工具FDR4目前只支持两个这样的模型。特别是，我们研究如何有可能检查细化的离散版本的定时故障模型，支持定时CSP。

2019-04-22cs.FLcs.LO

tock-CSP中的优先级

Priorities in tock-CSP

$tock$ -CSP编码嵌入了一种丰富而灵活的方法来建模CSP中的离散时间行为，其中事件$tock$被解释为标记时间的流逝。模型检查器FDR为$tock$ -CSP提供定制的支持，包括通常用于确保最大进度的优先级运算符，其中时间仅在内部活动稳定后前进。优先级也可以作为一个建模结构使用。然而，它的操作语义只适合于CSP最有区别的语义模型：有限线性模型。为了在$tock$ -CSP设置中实现合理和组合推理，我们计算优先级的指称定义。为此，我们建立了一个有限线性模型的专业化之间的伽罗瓦连接，$tock$和$\checkmark$，信号终止，作为特殊事件，和$\checkmark$ - $tock$ -CSP，一个模型为$tock$-CSP，捕获终止，最后期限，是足够的推理定时细化。我们的结果是机械化使用伊莎贝尔/HOL。

2019-07-18cs.LO

第18届精炼研讨会论文集

Proceedings 18th Refinement Workshop

精化是软件工程形式化方法的基石之一。细化是从抽象规范通过一系列基于抽象的步骤来开发更详细的设计或实现的过程，这些步骤相对于原始规范保持正确性。对Z、B、VDM和CSP等语言基础的研究使它们在某些工业部门得到了广泛的使用，例如，那些有安全或安全关键问题的人。除了精确的规范，形式化方法还允许精确和可验证的开发的可能性，正如精化的概念所捕获的那样。第18届精炼研讨会作为FLoC 2018的一部分在英国牛津举行。

2018-10-20cs.LOcs.PLcs.SE

使用交互树对RoboChart进行形式化验证的动画

Formally Verified Animation for RoboChart using Interaction Trees

本文使用交互树为RoboChart提供操作语义，在Isabelle中实现并生成可执行动画，通过化学探测器和巡逻机器人案例验证了动画场景是CSP指称语义的迹细化，确保了方法的正确性。

2023-09-13cs.LO

更多相关论文收起更多论文

天使进程

Angelic Processes

在系统的正式建模中，恶魔和天使的非决定论作为抽象机制发挥着根本性的作用。选择的天使般的本质与尽可能避免失败的属性有关。作为一个概念，天使选择首先出现在自动机理论和图灵机中，在那里它可以通过回溯来实现。它传统上是在精化演算中研究的，并已被证明在各种应用和精化技术中是有用的。最近，它已经在关系，多关系和高阶模型中进行了研究。它已被用于建模用户交互，游戏般的情况下，定理证明策略，约束满足问题和控制系统。当考虑状态丰富的反应系统的正式建模，这似乎只是自然的，这两种类型的非确定性的选择应该考虑。然而，尽管在进程代数的背景下，即通信顺序进程，天使般的非决定论的几个治疗，对应的天使般的选择的精化演算一直难以捉摸。在这篇论文中，我们开发了一个语义的关系设置霍尔和他的统一理论的编程，使天使的非决定性的特征在CSP。由于CSP进程通过设计，即前置和后置条件对，在UTP中给出语义，我们首先介绍了天使设计的理论，和一个同构的多关系模型，这是适合于表征进程。然后，我们发展了一个理论的反应天使设计，通过加强健康条件的CSP。最后，通过引入一个分歧的概念，可以撤销的历史事件，我们得到了一个模型，天使的选择避免分歧。

2015-05-28cs.LO

跳过细化

Skipping Refinement

我们引入跳跃细化，一个新的概念的正确性推理优化反应系统。使用精化对反应式系统进行推理涉及定义抽象的高级规范系统和具体的低级实现系统。然后，我们可以看到，实现所允许的每一个行为也都是规范所允许的。由于抽象级别的差异，通常情况下，实现需要许多步骤来匹配规范的一个步骤，因此，直接考虑口吃对于细化非常有用。然而，一些优化的实现实际上可以一次执行多个规范步骤。例如，存储器控制器可以将命令缓冲到存储器，并且在稍后的时间同时更新多个存储器位置，从而跳过抽象规范的若干可观察状态，这一次仅更新一个存储器位置。我们引入跳跃仿真细化，并提供了一个健全和完整的表征组成的“本地”证明规则，适合机械化和自动化验证。我们目前的案例研究，突出跳过细化的适用性：JVM启发堆栈机，一个简单的内存控制器和标量向量编译器转换。我们的实验结果表明，目前的模型检查和自动定理证明工具很难自动分析这些系统使用现有的概念的正确性，但他们可以分析系统，如果我们使用跳过细化。

2015-02-10cs.LOcs.PL

重新定义临界峰- $Φ\sqcup Ψ= \top$

Critical Peaks Redefined - $Φ\sqcup Ψ= \top$

假设一个集群是一个术语，其中出现了一些模式。我们给出了两个帐户的集群，几何一组（节点和边缘）的位置，和一个归纳的一对术语的差距（二阶变量）和模式替换的差距。我们表明这两个概念的集群和相应的细化/粗化订单，同构。这为集群配备了一个晶格结构，我们将其提升到（并行/多）步骤，以产生临界峰概念的另一种解释。

2017-08-25cs.LO