紧急属性挑战与突现系统工程

理论计算机科学电子笔记137（2005）163-181www.elsevier.com/locate/entcs紧急属性不细化Fiona Polack，Susan Stepney菲奥娜·波拉克，苏珊·斯特普尼1，2约克大学计算机科学系Heslington，York，YO10 5DD，UK.摘要修饰通常用于从抽象的规范中选出一个可证明正确的发展。涌现系统提出了一个有趣的挑战，在证明正确的发展，因为有一个全球和本地系统的描述之间的不连续性。这是一份立场文件，探讨了与传统精炼模式有关的挑战的某些方面。保留字：涌现，精炼，系统工程。1介绍我们对紧急系统的改进的兴趣与对紧急的工程和可预测性的研究有关。从所需系统的具体化（显示涌现属性），我们希望确定一组相似的具体化的低级组件，这些组件可以可靠地生成所需系统。在这份立场文件中，我们探讨了突现系统的发展如何与经典的细化概念相关联。紧急系统的工程很可能最终是不精确的，需要概率和论证技术以及传统的增量开发。这些问题不在此讨论。1电邮地址：fiona@cs.york.ac.uk，susan@cs.york.ac.uk2这项工作是TUNA可行性研究的一部分，EPSRC赠款EP/C516966/1。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.030164F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163我们使用元胞自动机（CA）生产滑翔机的例子CA可能是最简单的通常研究的紧急系统，因为它的操作环境完全由它的表示和一个单一的更新规则。这为审议发展问题提供了一个出发点，我们的立场可以在此基础上形成。本文首先简要回顾了古典精炼。然后，我们描述了一个模型的涌现，说明了CA;我们强调的问题有关的具体化的涌现系统。在此基础上，我们研究了精化对涌现系统的意义，然后探讨了经典精化和涌现系统开发之间不匹配的原因这使我们能够研究涌现系统的开发可能如何进行，以及它可能在哪里利用至少一些经典精炼的思想2传统的精炼模型传统的或关系的细化模型是发展中一个渐进步骤的正式表达。 关系的细化是根据初始和最终全局状态之间的多对多关系来铸造的。细化是在抽象世界中表达的抽象程序与在具体世界中表达的等价具体程序之间的关系，抽象世界捕获了这种初始到最终的关系[7]。传统上，这种细化的证明是使用“模拟”进行的精化证明表明抽象模型中的功能属性被保留在具体的模型中。非功能性属性，如安全性[9]，不一定会被这样的细化所保留。啊啊G R R G'C CFig. 1.细化的关系模型，与模拟出于本文的目的，我们强调了关系细化模型中的一些隐式约定。编写模型元素的语言包含所有级别和步骤所共有的概念;抽象规范使用F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163165与具体规范和检索关系相同的基本语言概念。请注意，我们这里指的不是一种特定的描述语言（如Z），而是一组共同的概念，这些概念需要表达规范的期望属性，如状态集或状态序列。使用模拟证明了该改进，该模拟在（相对简单的）检索关系中捕获。简单性是一个实用的约束，以增强可证明性。如果精化需要一个更复杂的检索，证明过程可以通过将精化分解为一系列步骤来简化，其中中间规范由更简单的检索链接（如[15，16]）。最终，步骤可以做得很小，以至于它们可以在精化演算中捕获（例如[11]）。“向后”和“向前”模拟的组合这是一个很好的证明，在这些术语中表达了任何这样的修饰[7]。系统的初始化和最终化是全局状态与相应的抽象和具体状态（包括操作的输入和输出）之间类似的3一种涌现突现系统是一个系统，其最终行为与在较低层次上观察到的行为是不连续的。 经常被引用的涌现系统的例子包括蚂蚁（真实的或模拟的）的网络导航，白蚁的建筑，成群和拥挤，例如鸟类或它们的模拟等价物，boids和CA。在描述一个系统时，低级组件代理的行为和交互用某种语言C表示;高级全局行为用某种语言A表示。如果在语言A和C之间存在基本的不连续性，系统就会显示出涌现性（例如，[13]）。例如，一个块中的每个代理可以被描述为向局部感知的质心移动，而感兴趣的全局行为是整个块的速度和大小[12]。正是这种描述语言的不连续性对传统的细化提出了挑战。3.1元胞自动机CA是最简单的涌现系统之一。在本文中，我们在单独的组件，即一个单元格（与状态，更新规则和一组邻居）和细胞的集合的表示CA模型。这样做的好处是使CA更接近于其他形式的涌现系统，在这些涌现系统中，（各种形式和内容的二维或三维空间的）表征与活动实体（蚂蚁、白蚁、boids）是明确可分离166F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163CA细胞是一个有限状态自动机;它的更新规则从细胞的当前状态和其他细胞的一些集合（称为其邻居）中确定细胞的下一个状态。这样的单元可以非常容易地编程，并且完全没有意思;状态的值波动，并且在某个点可能停止波动。当细胞和它的邻居位于某个离散空间中时，细胞成为CA（有限状态自动机的细胞阵列）的一部分。通常，每个细胞的状态由颜色或阴影表示。在这一点上，一些视觉模式可能是明显的，但什么也没有发生。只有当位于空间中的细胞的更新程序被允许在一段时间内重复运行时，涌现的特征才会出现，使得细胞状态的视觉表示形成移动模式3。空间和时间元素的关键性可以通过在不同的空间表示上建立等效单元模型来证明。例如，[8]采用相同的邻域定义和更新规则，并将其应用于二维规则网格和彭罗斯风筝和飞镖网格;他们发现，观察到的CA行为的大多数特征在两种表示上是完全不同的。同样，从不同的初始状态开始的相同的指定产生了非常不同的模式。此外，一些CA构型正在发生变化，所有细胞在少量时间步长内达到静止，而其他细胞则在长时间内进行看似复杂的相互作用。(For CA的讨论和分类，包括CA的其他表示和形式，见例如。[18、19、20]。3.2规范要求如果我们要指定和细化一个突现系统，我们希望能够指定最终系统的特征，然后推导出一些低级组件。然后，我们希望证明（在某种置信水平上）涌现性质是由低级成分建立例如，在CA上下文中，我们可以指定一些滑翔机的需求，如图2所示。我们希望系统至少能可靠地、可预测地产生这种行为模式。传统上将CA设计和编程为单元格网格，并且然后在一系列同步更新步骤上观察CA的行为。然而，当从所需行为的抽象规范开始时，这可能会对实现做出不合理的假设3.很难在一张静态的纸上充分演示CA：有许多在线CA演示，例如www.example.com上的Conway生命游戏自动机的模拟。http://www.math.com/students/wonders/life/life.htmlF. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163167该系统应包括一个区域，一个小的重复模式，或当两个滑翔机相遇时，它们将产生一个滑翔机，朝着其中一个滑翔机的方向运动。图二. 滑翔机需求规格站。规范没有提到网格;在一个区域（如屏幕窗口）上的运动只需要一些相对参考点（例如。边界）。代表性，以及国家指定和更新规则，是需要分析和完善的领域。4可重构系统与涌现系统的特征比较在本节中，我们将考察经典精化的一些常见含义，以阐明为什么它不自然地包含涌现系统的发展。图2中对滑翔机要求的具体说明是相当精确的。它是非确定性的，因为我们没有选择表示（for- mat，状态指定，时间步长等）-事实上，它甚至没有说明系统必须使用CA构建。与经典的改进一样，我们需要通过系统的、可验证的开发过程来澄清这些实现方面。正如在经典的精化中一样，我们希望根据我们对系统和目标介质的了解，以一种允许精化的方式正式地表示规范因此，我们可以从确定CA是这个系统的合理目标媒介开始。一个基于我们对古典精炼的了解的天真的发展计划是，• 以适当的形式表示具体化;• 以适当的形式表示CA;• 来表示在两种形式主义之间映射的检索关系为了表达这个规范，我们需要定义滑翔机（它有一个面积和一个运动矢量），两个滑翔机碰撞的条件，以及碰撞的后果。为了表达CA，我们需要将cell（其状态，更新规则和邻居集）形式化，然后将cell集合的表示形式化，并同步触发所有更新规则。168F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）1634.1细化以减少不确定性从抽象到具体的细化减少了非决定论。滑翔机规格的非确定性通过以便于表示运动的方式来细化区域来减少，即通过引入相对于运动被感知的东西。一种常见的方法是使用离散化的空间表示，允许对位置进行量化。例如，规则或不规则的网格允许使用某种形式的坐标来记录滑翔机的形状和相对运动在确定了滑翔机在窗口中的表示之后，我们现在探索这与细胞和细胞收集模型的关系我们观察到，细胞模型并没有找到一个更确定的实现目标，而是比离散化的空间表示更不确定• 单细胞模型只需要固定数量的相关（相邻）状态，以便计算细胞的下一个状态• 细胞集合的模型已经将邻居的身份绑定到特定的细胞组，特定的细胞将总是从该特定的细胞组计算其下一个状态-一些非确定性已经被去除;• 现在，我们需要将邻里关系与特定的空间布局联系起来，以便将邻里关系等同于（以某种方式确定）空间连续性-更多的非确定性已经被删除。检索带我们到达的中间层次似乎处于比目标媒介和原始滑翔机规范更低的抽象层次上-与经典细化相反，中间层次处于中间抽象层次上。4.2数据和操作细化一个简单、抽象的数据可以被系统地提炼成一个更精细的结构。抽象数据总是可以通过检索关系提取，这对于开发人员证明系统的输出（在接口处适当过滤或最终化）与指定的抽象数据相同是必要的。类似地，抽象操作可以被细化，本质上是通过操作内部的任何转换来保持操作的接口不变（再次，适当地过滤）。当细化滑翔机规范时，表示为CA的紧急结果，第一个问题是确定可以细化哪些抽象数据。第二个问题是确定哪些抽象操作可以被细化。滑翔机需求中的数据，图2似乎是窗口，滑翔机我们已经注意到，我们可以通过以下方式减少非决定论：F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163169使用离散化的空间表示;在数据细化方面，我们可以根据这种表示来细化窗口和滑翔机将一个窗口重新定义为一个网格的表示（即使是不规则的，或者在一定范围内，多维的）似乎已经足够传统了。然而，对已知滑翔机的简要研究表明，它们不能单独被定义为空间定义。此外，所提出的减少非确定性需要引入一个时间元素，以及离散化的空间表示。例如，康威此外，初始配置是至关重要的：必须有没有其他初始配置可以产生这种滑翔机图3.第三章。一个完整的循环简单的游戏生命滑翔机滑翔机规范中的操作可以被识别为滑翔机运动，滑翔机碰撞，滑翔机解决方案。抽象地说，这些都是简单的操作。然而，即使在细化表示的层次上，也很难表达这些操作。滑翔机的移动可以用一组特定表示的网格位置上的边界框的移动来表示，但即使这样也是不直观的：我们希望产生矢量移动，但定义这个矢量的只是滑翔机的累积移动-在四个时间步长内，生命游戏滑翔机的边界框（1）在一个方向上移动一个位置，（2）不移动，（3）在正交方向上移动一个冲突和解决并不容易。事实上，试图将滑翔机的运动细化为具体的操作是错误的，因为运动以及随之而来的碰撞和解决是CA的涌现属性，而不是我们希望编程到解决方案中的东西。这是关键点。在紧急系统中，“抽象”操作没有任何对应的“具体”操作。没有[4]如果我们允许一般的变换，滑翔机可以在三个步骤中被检测到，因为步骤三和步骤四是步骤一和步骤二的反射，并且运动空间是适当对称的。170F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163单元应包括状态和更新操作。更新操作将基于其（固定）邻居集的值计算单元的下一个状态。抽象和具体之间的简单关系，在一份详细的证明声明中。5重新审视精炼概念在第2节中，我们对经典关系修正进行了各种观察。现在，我们在涌现系统的背景下重新审视这些观察。5.1语言这里考虑语言的两个方面：语言的形式和 语言的广度古典精炼的成分都以一种共同的语言形式表达出来。具体的语言名称定义了数据结构，但是名称所表示的概念可以用抽象语言来表达--这就是为什么检索关系是形式上可表达的;它通过两个模型的公共语言转换将一个命名组件模型转换为另一个命名组件模型在突现系统中，描述抽象系统和具体系统的语言是不同的。正如在对细化可能性的讨论中所示，滑翔机的具体化（图2）使用了一种相对运动的语言--穿过一个区域意味着空间和时间上延伸的存在和速度的概念相比之下，图4所示的细胞的具体化指的是状态和操作--这是计算机系统和计算机编程的典型词汇。因此，在开发涌现系统时，我们试图将相对运动语言（滑翔机）中的一个具体化与计算语言（细胞）中的一个具体化见图4。 CA细胞规格如果我们转向表征的方面，并将细胞的具体化扩展到细胞的集合（图5），我们发现一个词汇表，它使细胞具体化的状态概念更加明确（状态值具有不同的表征）。邻居的概念也更加明确，但这需要改变词汇的空间布局。这让人想起了滑翔机规格的词汇。集合规范还明确引用了时间步长，这是一个隐含的概念F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163171元胞自动机应是细胞集合的表示。该表示法应根据每个细胞的内部状态表示每个细胞。对于每个单元格，其相邻单元格应是连续单元格的固定模式。元胞自动机系统应通过用所有细胞的下一状态的表示替换所有当前细胞状态的表示来表示所有细胞的同步更新在滑翔机的规格。然而，在单元格或集合规范中没有任何内容可以与滑翔机规范的关键概念，运动有关。CA的细胞绝对不会移动。图五、将CA指定为细胞的集合转向语言的范围，我们观察到，经典的修饰涉及两个具体的计算。我们可以用许多方法来精化抽象体系这一事实是无关紧要的;精化关系决定了抽象具体化的一种具体的具体变换事实上，甚至语言中用于表达抽象状态的部分也是有限的-在Z中，我们省略了系统的所有并发和时间方面;在CSP中，我们省略了系统状态的许多细节;在Circus中，我们忽略了非功能方面，如系统性能和安全性。在涌现中，好像语言不连续性不是足够的问题，我们发现许多CA本身就是图灵完备语言（见[14，3]）。抽象系统的语言也比古典精炼中使用的形式语言具有更广泛的范围;特别是，任何涌现系统的具体化都可能需要时间、空间和相对运动的物理概念，以及跨越时间和空间的可检测模式的概念。即使有一条通往共同语言定义的道路，但搜索空间的大小必然会严重危及对它进行细化的潜力。5.2细化关系在经典的情况下，通常有一个单一的细化关系（它可能由几个步骤组成）。甚至像Mondex智能卡开发[15，16]这样的大型工业精炼也可以通过单一的中间状态使用精炼。在突现系统中，对精化语言的考虑表明，很少有精化可以表示为一个 步即使在这个非常简单的例子中，滑翔机的语言，细胞和细胞172F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163滑翔机语言滑块规格细胞语言小区规范修订的滑动器规范小区邻域规范代表性规范系统规范表示语言图六、滑翔机系统研制中的建议要素收集表明，这一系统的完善将有许多步骤，其中一些具有概念的部分交叉。相互关联的要素可如图6所示。有些可能性是显而易见的--我们也许能够在一个表示上将细胞细化为一个细胞，在同一个表示上将滑翔机细化为滑翔机，然后使用状态和运动的物理学来联系这些规范。然而，很明显，没有单一的细化关系。5.3初始化在经典的可重构系统中，初始化为系统状态的每个元素分配一个符合状态不变量的起始值。形式主义者总是寻求一个简单的初始化，通常将每个集合设置为空，每个数值设置为0，只要这是系统的合法状态。它假设系统状态可以通过系统操作来构造（尽管很少考虑任何系统状态从其初始化的可达性）。在可精化系统中，抽象系统初始化就像任何其他操作一样被精化（图1）。紧急系统的初始化并不那么简单;我们有初始化什么的问题最抽象的状态（滑翔机的需求）可以在一个系统中初始化，在这个系统中，离散元素的运动可以被表达出来。例如，在gen.F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163173可以在台球桌上实现，其中初始化是设置一个或多个台球的运动。然而，抽象的（独立于实现的）初始化很难想象，因为滑翔器操作的定义依赖于所选表示的定义。对于CA，指定允许一个细胞及其邻居的状态的常规初始化;当细胞及其邻居被转换为表示时，表示被初始化，它们的初始化决定了初始着色。或者，可以用特定的阴影图案来初始化表示，并且从这是当它们位于表示上时这种初始化本身并不能保证出现哪怕一个滑翔机。我们可以保证初始化单元集合以产生滑翔机的唯一方法是通过“操纵”初始化到特定表示的已知滑翔机的相位布局之一，并确保滑翔机周围“足够的空间”，使其能够持续“足够长的时间”，以便任何探测到滑翔机的东西都能注意到它的我们需要某种方法来初始化整个系统（细胞，集合和集合的离散空间表示），因为CA行为是由起始状态决定的。然而，无论是CA的具体化，还是滑翔机系统的具体化，都没有给出任何从这里识别的组件找到这个起始状态的5.4定稿在经典系统中，终结决定了什么是（或应该是）被观察到的系统输出。Finalization去掉了具体数据的额外结构，因此系统只返回全局指定中所需的数据。(See[4]讨论终结及其在描述可观察事物时的局限性，即使在经典情况下终结是系统的最终状态。一般来说，突现系统是一个非停顿系统，它的终结通常没有定义。然而，如果一系列输出是无干扰的，则终结可以被视为非停止系统的一系列输出的在连续涌现系统中有许多终止子计算把终结看作是从一个组件向整体提供某种东西的机制（与经典的子系统类比），终结可以应用于每个子计算。例如，一个单元在一个时间点更新。finalization确保新状态被传递给表示。 代表的终结在一次（集体）更新完成时，确保了整个改变的表示被瞬时地揭示。174F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163这些似乎是可以接受的最终化实例，特别是如果细胞、细胞集合和表示规范被经典风格的细化所包围然而，这种终结无法揭示系统是否产生了所需的高级行为，即滑翔机的产生和相互作用。最接近于整个滑翔机系统的终结的事情是在足够的空间和时间范围内观察系统的代表性方面，从而可以观察到所需的滑翔机行为。因此，单个抽象滑翔机操作（运动）被检测为一系列具体滑翔机操作（运动步骤）的结果把系统的“终结”看作是对系统的一种具体观察，这就把我们引向了实现整个突现系统所需要的另一个要素。滑翔机的基本运动必须能被某种监控操作检测到。探测所需的滑翔机需要：• 一个可以识别任何滑翔机的时空特征的监视器• 一个可以识别两个滑翔机时空会聚的监视器;一个侧面的观察（不一定要显示给观察者）必须确定两个会聚滑翔机• 一个监视器，它寻找一个单一的滑翔机从碰撞中出现，并确定它确实是与它的祖先之一发生事故紧急系统中的监控器可以被认为是一种持续时间的终结（一种观察视角）。请注意，除了监视表示的时空特征之外，这些观测都不做任何事情。甚至第二个监视器的副作用也不会影响CA或其表示;各个单元格的规则决定了第一次“碰撞相互作用”之后的时间步长中发生的事情5.5对核证机关级别性质的观察在表达CA的组件时，我们注意到每个级别（系统，表示，细胞）在某种意义上表达了下一个级别的衍生物。因此，细胞是一维的;表示引入了多维空间;系统引入了时间维度。在该表示中，每个细胞获得一个位置;在系统中，细胞块似乎具有速度。此外，在改变CA各层次的语言时，我们观察到不同的身份出现：• 细胞只是一个原子它只能通过测量其状态来与任何其他细胞区分开;可能有许多细胞具有相同的状态;没有同一性的感觉F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163175• 为了将像元及其邻居与表示联系起来，像元获得身份;身份是（或可以从）表示上的像元的离散位置;正是这个身份允许一个像元的邻居成为CA• 当系统运行时，观察者（模拟的观察者，或者，如上所述，监控终结操作）识别在表示上具有相同状态指定的单元组最后一点是识别突现的关键（这里是指随时间持续存在一些CA在许多时间步长内产生大量的活动-短暂的滑翔机，振荡器和其他CA结构，变得短暂可见，然后被不太相干的结构吸收;有时，波模式或布朗运动出现在CA中，可能会分解为一些振荡残差。随着时间的推移，如何识别和监测细胞群对于识别CA所需的紧急特征至关重要。识别可能无法在表示级别实现-为了检测系统随时间的平滑移动，监视器可能需要在另一个不连续级别（如视频中的移动跟踪）的外部。5.6一个现实的检查这里所探讨的具体情况，是对涌现的所有计算机模拟中最简单的一个的最清晰的涌现性质之一的描述。CA用于计算;其应用包括并行计算、气体扩散模拟、铁磁性、渗流、结晶、森林火灾传播和城市发展以及图形生成等概念性工作。To Escheroli使用CA作为微分方程5的替代。 在这种情况下，CA要求要复杂得多。 我们可能会，例如，需要一个滑翔枪，一个基于CA的传统计算机电路模型的关键组件。图7给出了一个可能的规范。图8示出了在二维规则网格上的生命游戏滑翔枪的初始状态，即在滑翔机生产之前枪本身的阶段之一; CA行为包括在网格两侧的一对四单元图9示出5摘自http：//www.rennard.org/alife/english/acintrogb02.html，2004年12月17日查阅176F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163滑翔枪应发射一串滑翔机，这些滑翔机以规则的间隔在同一路径上行进。 滑翔枪应产生这样的滑翔，直到由外部事件终止;不应有内部中断发射。图7.第一次会议。一门滑翔枪的规格一个不同阶段的枪（两个边缘块是如前），一个新兴的滑翔机和三个已经发射滑翔机。图8.第八条。游戏的生命滑翔枪：初始设置图9.第九条。游戏的生命滑翔机枪：快照与四个滑翔机我们把通过改进这样一个系统来发展这个系统作为一个练习留给雄心勃勃的读者。6设计应急系统目前，紧急系统是通过偶然或试错发现的。系统开发是可能的，使用遗传算法（GA）来F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163177育种标准（[10]回顾了这一领域的工作）。然而，也没有遗传算法的工程指导-CA的GA开发依赖于试错法，例如，表示的接近程度的测量使CA设计更加严格的主要研究从已知的CA模式开始，而不是从（紧急）系统规范开始例如，[5]建立在CA和紧急系统分类的一系列工作基础上，开发了CA的计算力学，以关注GA的进化。虽然这项工作在数学上很有趣，但对于系统开发来说，它似乎等同于研究如何在一个特定的范例中搜索所有可能的计算机程序，以便找出如何实现特定问题的解决方案进化CA相对于事故和人为试错的唯一优势是，它有更好的机会在可接受的时间内自动收敛到可接受的解决方案然而，古典精炼也是一个试错的过程（尽管有些形式主义者试图说服我们不是这样）。尽管出版的插图简洁，但现实是一个反复的猜测工作，关键是由猜测者的经验指导。教科书以调整抽象规范而闻名，因此细化是干净的。紧缩[2]承认，在现实中，干净的细化是很少可能的，而向前和向后细化到一个发明的中间状态提供了一个试错的方法，当没有简单的直接路线从（真正的）抽象规范到所需的具体模型。作者还研究了（不同层次的）精化模式[17]，基于模板的精化[1]，以及证明和精化的进化方法。经典改进的猜测似乎比涌现系统开发的猜测问题少得多，因为猜测的范围受到规范语言和所处理问题的（相对）简单性的限制。我们能否设计出类似的方法来约束涌现系统的抽象和具体描述的不同语言，而不失去表达系统概念的能力6.1应急系统从上面的分析中，出现了一些指导方针这些给出了（a）如何约束或组织紧急系统规范的语言以支持开发，以及（b）常规细化可能适用的程度。在第5节中，我们考虑了精化对突现系统的意义，并对所考虑的CA进行了概念上的分解。CA系统似乎比其他形式的涌现系统更简单178F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163系统规格说明语言系统规范组件语言功能组件规范环境规范环境组件集成环境综合规范集成环境语言见图10。 图6的概括这首先是因为细胞状态和操作的简单性，其次是细胞相互作用的环境的简单性，作为对细胞执行的操作没有直接影响的视觉表示该模型具有一般性，如图10所示。我们认为某些链接（双头箭头）通常可能具有经典（或至少严格）细化的潜力。单头箭头连接系统元素的语言不连续性。这种元素分解有可能最大限度地减少语言不连续性的影响和范围。因此，我们的前两个指导方针是识别紧急系统的三个关键元素--所需的系统规范、功能组件（或实例）规范和集成表示规范;并识别具有公共词汇表的元素。 接着，确定中间元素-抽象系统规范和功能组件的细化（可能是细化）在集成环境方面。实现图10的不可再固定链接的见解来自第5节中对最终化的考虑。我们提出了指导方针，建立如何检测出现。这需要开发人员考虑如何监控紧急系统以及必须检测哪些行为我们还没有研究过这部分问题，但最初的印象是，由于涌现依赖于参照系的变化，F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163179对于观察者来说，系统很可能很难指定和细化监控器;监控可能会抓住元素和整个系统之间的语言不连续性问题。与突现系统初始化有关的唯一指导原则与可再激发系统的指导原则是相同的--建立系统每个组成部分的初始状态。大多数系统中的某些组件很容易初始化（因为它们是简单的操作组件）。然而，某些组件（如CA的起始状态）不能被概括;必须强加一个已知的起始状态，以产生所需的目标具有负反馈或构造规则的涌现系统可能更容易初始化，因为所需的行为发生在吸引力的主导（或唯一）流域中，系统从任何起始状态收敛到该状态。然而，对系统行为的要求越精确，初始化就越难实现。因此，任何boid模拟都可能发生碰撞，但只有某些起始状态才会产生特定大小、方向和速度的碰撞。事实上，情况很糟糕;生物学有强有力的证据表明，一个复杂的系统不能在一个状态下“初始化”，从而导致一个期望的形式，而是必须“成长”。例如，通过简单地引入一群物种来构建一个复杂的生态系统是不可能的。看起来，“稳定的”突现系统所占据的相空间的部分7结论我们提出了一个紧急系统的发展的立场，使用从经典精炼获得的见解。我们试探性地发展我们的立场，从一个系统规范，可以实现CA的分析。我们的工作还处于早期阶段，但似乎正在产生一种可推广的方法来对紧急系统进行“架构”改进，该方法考虑了语言的不连续性和这些系统的元素之间的抽象层次的变化。我们的方法不同于其他尝试确定紧急系统的发展，因为，而不是从已知组件构建紧急系统，我们从所需系统的规范开始，然后尝试系统地确定一个组件和集成环境，能够形成所需的属性作为紧急事件。很可能，所有为涌现而设计的尝试都将依赖于180F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163特定的紧急行为;语言的不连续性的差距，在DEVELOPMENT将弥合实例化适当的模式。我们需要尽量缩小差距，使所需的模式几乎确定通过间隙的形式，从而避免了例如CA计算方法的特殊性。引用[1] N. 再见，S。 Stepne y和F. POLACK. 模块化UML语义：基于模板和泛型的Z2003年，在FME2003上的组件软件的形式方面研讨会，比萨，意大利[2] R. Banach和M.波普莱顿精简、改进和模拟。在ZB 2000，LNCS的第1878卷，第304斯普林格，2000年。[3] E. R. Berlekamp，J. H. Conway和R. K.家伙数学游戏的制胜之道第2卷：游戏特别，第25章。中国科学院出版社，1982年.[4] J. A.克拉克，S。Stepney和H.奇弗斯打破模型：安全攻击的终结和分类。技术报告YCS-2004-371，计算机科学系，约克大学，2004年。出现在Refyne[5] J. P. Crutch Field，M. Mitchell和R.达斯 集体计算的进化设计在细胞自动机中。在J. P. CrutchField和P. K. Schuster，editors，Evolutionary Dynamics. 探索选择，中立，事故和功能的相互作用。牛津大学出版社，2002年。[6] M.迦纳数学游戏：约翰康威的新纸牌游戏“生活”的奇妙组合。美国科学，223：120[7] JifengHe，C. A. R. Hoare和J. W. 桑德斯 数据细化（结果）。在ESOPSpringer，1986年。[8] M. Hill，S. Stepney和F.湾 不规则拓扑上的生命游戏。 在准备过程中，2005.[9] J. 雅各布关于安全性的基本定理计算机安全杂志，1（4）：385[10] M. 米切尔，J。P. Crutch field和R.达斯进化细胞自动机与遗传算法：最近的工作回顾在96年的EvCA俄罗斯科学院，1996年。[11] C. Morgan. 从规范编程。 Prentice Hall，第二版，1994年。[12] C. W.雷诺兹Flocks ，herds ，and schools：A distributed behavioral model（SIGGRAPH'87）. 计算机图形学，21（4）：25[13] E. M. A. Ronald，M. Sip p er和M. S. 我来了。设计，观察，惊喜！ 一个测试的出现。《艺术生活》，5（3）：225[14] A. R.史密斯简单计算-通用细胞空间。Journal of the ACM，18（3）：339[15] S. Stepney和D.库珀 工业产品的形式化方法。 在ZB2000中，第1878卷LNCS，第374斯普林格，2000年。[16] S. Stepney，D.库珀和J. C. P·伍德考克电子钱包：规范，完善和证明。技术专著PRG-126，牛津大学计算实验室，2000年。[17] S. Stepney，F.波兰人和我。托恩 Z：five插图的轮廓图案语言，两张桌子。ZB2003，LNCS第2651卷，第2Springer，2003年。F. Polack，S.Stepney/Electronic Notes in Theoretical Computer Science 137（2005）163181[18] S. Wolfram元胞自动机的统计力学。Reviews of Modern Physics，55：601[19] S. Wolfram元胞自动机计算理论。数学物理通讯，96：15[20] A.文斯克自动分类细胞自动机：寻找滑翔机，过滤和关联时空模式，吸引子盆地和z参数。Complexity，4（3）：47-66，1999.