铁路联锁系统状态图地理与功能建模：形式方法和工具组的意大利比萨经验总结

理论计算机科学电子笔记133（2005）3-19www.elsevier.com/locate/entcs联锁系统状态图的地理与功能建模Michele Banci1形式方法和工具组意大利比萨AlessandroFantechiDipartimento di Sistemi eInformaticaUniversit`adegliStudidiFirenze意大利佛罗伦萨摘要计算机控制的铁路联锁系统（RIS）的发展已经看到了越来越多的兴趣，在使用形式化方法，由于他们的能力，精确地指定的逻辑规则，保证通过铁路站场的列车的路线的安全建立最近，出现了一种趋势，即使用状态图作为标准的形式主义来产生RIS的精确规格本文介绍了一种使用状态图对铁路联锁系统进行建模的经验我们的研究从“地理”、分布式的角度解决了这个问题：也就是说，我们的模型是由单个物理实体（点、信号等）的模型组成的它们共同实现联锁规则，而没有任何集中的规则数据库，另一方面，这是实现这种系统的典型方式（我们称之为我们的方法的主要目的之一是验证其减少重新验证中的错误的能力。的情况下，物理modifications的院子里，我们展示了如何的地理方法可能会减少这种e-ort，只需要重新验证的那些软件模块，实际上是一个由变化所影响。关键词：铁路信号，联锁，安全关键系统，正式规范，状态图，验证。1电子邮件：michele. isti.cnr.it2电子邮件地址：fantechi@dsi.unifi.it1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.0554M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）31介绍铁路联锁系统（RIS）是一个复杂的装置，用于安全地建立列车通过铁路站场的路线。电子信号系统已经取代（实际上仍在取代）旧的机械联锁系统，因为它们在以下方面具有优势• 对操作员故障的依赖性较小• 自我诊断系统检查，以提高可靠性;• 集成和集中系统的可能性。通常，RIS会接收路由请求;对该请求的应答必须经过一系列检查和操作：• 如果轨道区段元素被占用，则不能锁定进路• 如果路由的任何部分都没有被锁定，则路由可用• 如果路由可用，则将其锁定;• 锁定路线意味着其所有轨道元件都被锁定;• 当路由被锁定时，用于该路由的信号可以被切换到绿色，并且然后肯定地确认原始路由请求这些检查和行动的目的是确保没有列车可以驶入另一列车占用的路线。从这个检查和动作列表中可以明显看出，形式化方法在RIS开发中的应用，并且有大量关于联锁系统形式化的文献（例如，参见[1，3，7]）。事实上，CENELEC EN50128铁路行业软件开发指南[5]建议在安全关键计算机控制系统的开发中使用形式化方法然而，我们可以观察到在联锁系统领域的最后几年的新趋势。最近欧洲内部市场的开放已经结束了国家铁路公司和国家铁路行业之间传统的严格合作，在某种意义上，对精确规格的需求有限，因为每一个误解最终都通过电话解决在RIS的情况下，原理图式，一种梯形的，基于继电器的语言，广为铁路工程师所知，构成了描述联锁系统的通用参考语言，因为联锁是基于继电器的[8]。在引入基于计算机的RIS时，一些行业已经定义了他们自己的方法来产生基于计算机的联锁，或多或少形式化，通常基于某种逻辑形式主义或语言，但无论如何，他们都被限制将自己的开发/规范方法/语言与原理图相关联，M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）35国家通信工程师公司另一方面，开放的、保护较少的市场导致了以前的民族工业的重组和合并，成为几个跨国公司，这些公司现在需要合并关于连锁生产的不同技术。在一个开放的市场中，必须更加依赖精确的合同规范来定义每个相关方的责任;此外，铁路行业的跨国规模要求联锁系统及其合同规范的标准化，以便向欧洲范围内的几家公司提供相同的产品。Euroin-terlocking项目由欧洲主要铁路公司的一个财团发起，旨在开发欧洲一级的标准联锁系统，以通过标准化降低公司的投资和维护成本。在这个项目中，一种趋势已经发展到使用有限状态机来建模联锁规则[15]。特别是，一种更丰富的机器形式，即Statecharts[9，11]，被认为适合于表达联锁系统典型的检查和动作序列。UML方言[16]和Statecharts的Statemate方言[12]都被考虑过。本 文 遵 循 这 一 趋 势 ， 描 述 了 铁 路 联 锁 系 统 建 模 的 经 验 ， 使 用Statecharts。我们的研究从“地理”的共同实现联锁规则，而没有任何集中的规则数据库，这是解决问题的典型方法，我们称之本研究的主要目的是调查地理方法的可行性，并将其与功能方法进行比较;我们有兴趣评估的最有趣的问题之一，实际上已经推动了我们的工作，就是验证地理方法在对场地进行物理修改的情况下减少重新验证工作的能力：实际上，为了遵守严格的安全指南，场地物理配置的微小变化通常需要全新的验证工作，例如，由于对所有软件模块所使用的单个中央结构所做的改变，通过扩展的测试程序。我们展示了如何地理图形的方法可以减少这种电子邮件，只允许重新验证那些软件模块，实际上是一个由变化所引起的6M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）32地理和功能建模RIS是一种嵌入式系统，可确保火车站设备的安全运行。这样一个系统控制着信号和轨道点的布置，这些信号和轨道点是相互连接的，它们的功能将相互继承按适当的顺序，并定义了联锁规则，以保证安全操作。RIS的一个简单（最简单）示例，我们将在本文中用作案例研究，参考图1所示的布局，并基于真实的意大利联锁系统[4]。Fig. 1. 最简单的铁路站场布局。联锁规则显然是系统的核心，因此它们的正确性是形式化规范要解决的主要目标。该规则旨在只允许车站内道岔位置、信号和列车的安全组合由联锁系统处理的信号指示控制进路的正确使用，授权列车在联锁范围内移动。规则通常强制执行预定义的动作序列：发出路线请求命令通常首先触发检查路线中涉及的所有轨道元素是否空闲;在这种情况下，发出命令用于定位该路线的点并锁定轨道元素。该阶段之后可以是对被命令元件的正确状态的全局集中控制，之后路线被锁定并且路线的信号指示被设置。2.1功能处理法大多数基于计算机的联锁系统使用（在其实现和/或正式规范中）某种形式的集中式数据库，其中存储联锁逻辑的规则这种方法的主要特点在于通过采用专注于功能的设计方法来生成规则，例如开关点检查功能，路线设置功能或路线验证[8]。这就是为什么我们称这种方法为“功能性”。这些功能是基于“条件表”（控制表）设计的M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）37表示在信号从红色切换到绿色以允许列车进入轨道区段之前必须满足的所有条件[14]。在这种设计方法中，忽略了堆场设备的放置，设备在堆场上的地理位置与RIS中实现的控制功能之间不存在直接的相关性。由于这个原因，识别系统中受外部事件刺激的部分是一项艰巨的任务。2.2地理方法不同的方法可以考虑将互锁规则的知识分布到对物理元素的地理位置进行建模的对象地理规范的一个例子是EURIS语言（欧洲铁路联锁规范），这是一种用于铁路控制系统的视觉和图形规范语言[2，6]。使用这种语言，可以以基于组件的方式构建从站的布局到模型的控制系统。EURIS规范语言，在1992年，西门子公司使用该标准，用于指定使用相同通用规范组件的不同铁路站场。实际上，它由一组标准化的铁路控制组件[18]组成，这些组件应该很容易组合在一起，从而提高开发速度并允许组件的重用。每个元素内部都包含一组规则，这些规则能够根据不同的布局配置进行调整。由于EURIS是一种图形语言，另一个优点是规范易于阅读，因为它们直接表示庭院中元素的物理位置。2.3再验证乍一看，铁路站场的布局似乎是固定的，不能改变。实际上，布局可以在施工期间改变，以使院子的部分操作，或在维修工程或扩建之后。在联锁系统的寿命中，这种情况可能会发生几次，无论如何，联锁系统的寿命跨越几十年。基于计算机的RIS与基于继电器的RIS相比具有明显的优势，任何变化都可以通过软件的变化来解决。然而，在开发这款安全关键软件时遵循的严格准则需要进行昂贵的验证活动：对软件的任何更改都需要重新验证活动。因此，采用能够减少此类工作量和成本的方法和技术是一个重要的工业目标。在本文中，我们研究的影响，地理方法的具体化的一个区域创新系统可以在这一特定方面：的想法是，不断变化的8M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）3布局的一部分仅影响那些在地理上靠近改变的软件对象的软件对象。因此，只有被排除的才需要重新验证。3StatechartsStatecharts形式主义[9]是有限状态机（FSM）的经典形式主义的扩展，允许层次并行交互状态机被指定。从单个机器的一个状态到另一个状态的转换（状态图）是由触发事件驱动的，触发事件可以引用其他机器的状态或全局变量;因此，状态图之间的通信活动在转换期间，操作生成事件，这些事件由其他转换或全局变量上的条件触发。仅由一个外部事件生成的内部事件链是可能的。Statecharts的层次结构特征允许将系统切片为定义良好的子系统，从而降低复杂性，并允许构建具有并发部分的结构化模型。该系统可以分解使用AND状态，它演变奇异和并行的方式。Statecharts有两种主要的方言：UML（统一建模语言）状态图[16]和Statemate Statecharts [10]。3.1Statemate工具在本文中，我们遵循Statemate Statecharts风格。I-Logix State- mate工具[17，13]支持编辑图形化的Statecharts符号，但更重要的是允许执行和图形化模拟完整的系统规范，允许探索确定系统正确性的任何场景，并评估规范是否符合要求。Statemate模拟器允许执行模型，允许验证检查系统动画的行为。此外，它允许动画面板有一个模型行为的证据，所以我们可以很容易地生成“假设”的场景。Statemate还提供基于模型的基于C或基于Ada的原型源代码的自动生成。Statemate最近的另一个重要的附加组件（到目前为止，我们还没有在这个经验中使用过）是一个强大的模型检查器，这显然是一个优势，可以在指定正确性方面获得信心。M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）39Statemate的这些特性使其在w.r.t.基于UML的工具，只允许编辑状态图[7]。Statemate工具还支持另一种图表，这对构建结构化系统很有用：活动图。活动图可以看作是多层次的数据流程图.活动图描述了将系统的功能分解为功能或活动，并组织成层次结构。该层次结构详细描述了系统能够执行的功能组件或活动，以及这些组件如何通过它们之间的信息流进行通信。每个活动的行为都使用状态图来描述。在这项研究中，活动被用来表示在院子里的分布式设备，因此，一个控制- ling状态图是与每个设备。这些图表比状态图更灵活，因为它们可以动态地激活和停用，这是状态图不可能做到的。每个活动都是一个具有适当功能的子系统，依次用状态图表示。4Statecharts地理模型本文提出了一种从联锁系统的布局设计到联锁系统的操作规范设计的方法。这种方法类似于EURIS语言中使用的方法[2]。在这项工作中，我们专注于一种方法，不使用任何形式的全局汇总变量，这是通常的函数方法。术语汇总变量指的是其值取决于一组其他单个变量的值的变量，每个变量与布局的物理实体。例如，我们可以考虑与路线相关联的变量，当且仅当记录属于该路线的轨道电路的占用率的变量中的至少一个被设置为真时，该变量为真。使用汇总变量虽然有助于抽象系统的某些全局方面，但会使模型与物理拓扑更加疏远。本文中讨论的经验实际上是在同一联锁系统的Statemate状态图建模之前，使用经典的功能方法：专用模块用于记录命令进路;这些模块负责检查相关轨道电路的占用情况，遵循作为输入的条件表相反，我们将看到，在我们提出的方法中，每个专用于管理每个轨道电路的模块都有责任检查其与com的兼容性10M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）3命令路线。同样，功能对象执行的所有活动都已分配给这些地理对象。因此，例如对特定道岔点的正确位置的控制是从所有感兴趣的元件执行的，而不是由专用于管理所有道岔点的单个对象执行的。图二. 路由的一个例子模型中的每个对象都实现只对该对象感兴趣的规则。例如，如果我们考虑图2中的三个信号，模型将为每个信号量包含一个对象。与信号灯4相关的对象（其允许列车在右方向上移动）应控制信号灯3（右）和2（左）的红灯被点亮，并且绿灯被切换为关闭。该控件不查看全局汇总变量（在示例中，该变量将显示路由是空闲的），而是与控制其他信号量和设备的对象进行通信。这样，我们得到了一个模型，其结构反映了铁路站场的布局。这对模型的可读性有积极的影响，并对模型中只隔离那些对物理布局变化感兴趣的对象的可能性有积极的影响。另一方面，我们放松了通用性：在函数方法中，处理所有开关点的模块可以是通用的，并且是条件表嵌入了关于铁路站场的特定规则的知识。我们的对象没有在任何不同的地理布局（如EURIS）中可用的通用行为：我们必须为任何不同的站点重新设计它们，尽管遵循具有预定规则的预期模式。这种做法的后果是：• 模型的结构应反映场地的地理拓扑结构。• 模型的元素应该复制物理的行为M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）311院子的组成部分• 模型的元素应该嵌入所有与相应物理组件相关的逻辑规则（以避免使用求和变量）。这种模型能够最小化对象之间的相互依赖性。对象不可能是完全独立的;事实上，互锁系统根据定义是一个必须控制对象之间相互关系的系统。然而，地理模型最大化了独立性：在院子里有独立性的地方，我们希望它在模型中得到反映4.1分层模型的结构该模型是按照RIS的分层体系结构构建的，该体系结构由三层组成：命令（人）层、逻辑层和物理层（图3）。第一层（命令）专用于与图3.第三章。分层互锁架构的图示操作员或其他系统，向RIS发送命令在最低层（物理），有堆场设备和设备，它们必须由RIS指挥和控制。该级别由实际设备接口组成，实际变量用于控制调车场。中间层是RIS的核心，其中规定了联锁规则。它由每个物理设备的单独对象组成。12M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）3图4显示了对象如何与命令和物理层互连。任何对象的状态都与物理设备的实际状态一一对应。与特定路由相关的每个对象都能够接收请求该路由的命令，在这种情况下，它会对物理层和逻辑层的其他对象执行适当的检查。当一个路由reservation命令是由外部系统（也是人类）发送，这条消息被发送到所有的对象相关的路线。 然后所有对象都求值 它们的规则相互作用以确认接收到的命令。见图4。 对象间通信的说明。因此，在每个对象内部，通常以经典函数方法为中心的逻辑是分布式的：不存在协调对象。4.2Statecharts模型如图3和图4所示，该系统结合了地理要素。每个地理要素都由使用Statemate状态图形式主义指定的活动图定义。如图5所示，模型的主要层次由一个活动图表组成，该图表由几个活动组成，这些活动与放置在院子里的物理对象严格相关。在较低的级别上，每个块都由一组嵌套的子活动和实现联锁规则的状态图组成。我们可以注意到，这一层的拓扑结构与堆场的地理布局完全对应（参见图1）。M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）313图五、状态图模型的第一层和内部活动图的分布活动之间的交互可以通过发出事件信号（包括变量值变化）来发生，或者通过直接寻址，即指定目标，或者通过广播。在我们的模型中，每个元素（变量、事件等）都有一个可见的作用域。 元素的作用域可以由用户显式定义：元素值的每次更改都会广播到元素范围内的所有活动和状态图因此，共享变量被用来实现对象之间的通信：每个块都检查附近其他对象的状态，并检查它们的一些状态变量。描述活动行为的状态图（控制活动图）的示例如图6所示，其中说明了轨道电路管理器：该图显示了逻辑状态的使用，例如用于保留对象的逻辑状态。之所以需要这些局部状态，是因为我们没有任何全局对象来记录哪些元素正在使用，因此控制逻辑是分散的。我们可以注意到，图表通过查看共享变量与大量其他对象（如信号量和其他不同的轨道电路）进行通信。事实上，很明显，连锁规则是如何分布在每个活动图中的转换条件图7表示控制绿灯的状态图：当操作员（人或系统）发出命令时，该状态图和所有其他状态图控制与之相关的轨道电路被保留，与之不兼容的轨道电路被释放。这个例子也证明了共享变量的大量使用虽然14M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）3见图6。 轨道电路状态图图7.第一次会议。控制信号灯绿灯的状态图每个图表都与其他图表并行工作，它们通过大量使用共享变量而严格相互关联。M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）3155职能办法和地域办法的比较在建模活动结束时，我们已经能够使用Statemate模拟器工具模拟整个系统，该工具允许通过使用适当创建的面板直接交互（图8）。我们使用了与我们为同一RIS构建的配套功能模型相同的模拟场景，建立了地理和功能方法的相对一致性。见图8。 控制面板。从状态图模型中，还可以使用自动代码生成器工具生成C或ADA代码，该工具是Statemate工具的一部分。由于模型的详细性质，生成的代码可以立即使用，而不需要任何其他翻译成低级语言。所得到的代码与地理模型共享软件模块和调车场设备之间的对应关系。比较这两种规范，功能设计方法比地理设计方法更紧凑，需要更多的冗余控制，但也不太可读，因为将变量融合到全局汇总变量中，这些变量维护关于对象的信息，而不一定相互关联。另一方面，由地理方法表现出的控制的冗余可以被认为是积极的安全措施：只有当所有控制都成功时，才做出关于建立路线的决定;控制是冗余的，但是多样的，因此它们构成了对软件故障的保护。16M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）35.1再确认活动我们对地理方法的主要兴趣在于，当场地进行改造时，可以减少所需的重新验证时间主要的问题是：“我们必须重新验证整个系统吗？或者有可能了解实际发生的变化，从而限制重新验证的可能性？实际上，在地理方法中，在联锁系统的某些部分发生变化的情况下，可能存在不需要因为它们不受所做的修改的影响，既不直接也不通过传播。由于每个对象独立地执行其控制，并且系统不使用全局汇总变量，因此我们可以断言这些对象不必重新验证。修改后的对象需要重新验证，例如使用新的测试场景或修改现有的测试场景。5.2互动桌为了选择需要或不需要重新验证的对象，对于一个变化，我们应该遵循对象之间的相互关系，这些对象从与变化所影响的物理设备直接相关的组件传播变化的影响。这些对象之间的相互作用很容易在一个相互关系表中说明，该表是表1中所考虑的案例研究的示例。这样的表格显示了路由（列）和设备（行）之间的关系。对于每条路由，都有一组设备和设备用于建立路由命令，反之亦然，一个设备可以由一个或多个路由使用。相互关系表通常是一个有用的工具，它允许将一个对象与另一个对象相关联。然而，它之所以有用，只是因为我们以地理方式实施了该模型。如果我们为一个功能设计的模型定义一个类似的交互表，我们会发现对象之间将存在100%的相关性，这是由于单个中心元素（条件表）的依赖性可以从地理模型中提取相互关系表：例如考虑图7中的图表，我们可以立即注意到信号量SE 1-A-D-GREEN（表1中的SE 1-G）与路由1-3和1-4之间的相互关系，路由1-3和1-4又与一组其他对象（例如CDB-10、CDB-11等）相互关系。M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）317设备航线1-31-42-32-43-14-13-24-2CDB-10XXXXXXCDB-11XXXXXXCDB-20XXXXXXCDB-21XXXXXXCDB-IXXCDB-IIXXBA-1XXXXBA-2XXXXSW1-RXXSW1-NXXSW2-RXXSW2-NXXSE1-GXXSE1-RXXXXXSE2-GXXSE2-RXXXXXSE3L-GXSE3L-RXXXXSE3R-GXSE3R-RXXXXSE4L-GXSE4L-RXXXXSE4R-GXSE4R-RXXXXCDB-IIbisXX表 1系统的相互关系表让我们考虑以下对受控铁路站场进行更改的示例：将物理元件CDB-II拆分为两个不同的元件，分别命名为CDB-II和CDB-IIbis。新元素（CDB-IIbis）添加在表的末尾：遵循与新添加的设备相关的路由，我们可以轻松识别哪些是它们感兴趣的设备（表1中的灰色区域）。如表1所示，添加CDB-IIbis元素涉及1-4和2-4路由，因此我们必须仅修改这些路由感兴趣的对象;在本例中，24个设备中有17个设备：只有70.83%的系统对修改感兴趣：这表明重新验证e排序可能节省30%。18M. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）3从这个观点来看，当改变只影响布局的边缘部分时，即某些设备实际上只被少数路线使用时，优势更大关于这些考虑到更大设计的可扩展性，尽管我们没有进行进一步的实验，但是我们可以观察到，在实践中，在铁路站场中具有对许多路线通用的单个设备是不方便的，因为这限制了站场在安全同时设置的路线的数量方面的容量：路线之间的独立性确实是站场本身设计中的主要目标6结论我们所介绍的经验是一个更广泛的研究项目的一部分，旨在通过不同的Statechart方言和支持Statecharts的不同商业工具来研究RIS的设计，例如State-Stateow（MathWorks），TelelogicTAUGeneration2（ Telelogic ） ， Real-Time Studio （ Artisan Software ） ， visualSTATE（IAR Systems）。我们在本文中集中讨论了采用地理方法的可能性，其主要目的是调查在发生变化的情况下减少重新验证的可能性在这个方向上，我们需要验证更大设计的可扩展性。此外，我们需要评估这种方法的适用性，一方面（通过模型检查器，例如集成在Statemate中的模型检查器，或其他学术工具），另一方面，从物理布局的规范自动生成状态图模型引用[1] S. Bacherini，S.比安基湖Capecchi，A. Felleca，A. Fantechi，E.斯皮尼奇使用SDL建模铁路信号系统，铁路运营和控制系统正式方法研讨会（FORMS 2003），匈牙利布达佩斯，2003年5月15-16日[2] J. Berger，P. Middelraad和A.J. Smith。欧洲铁路联锁规范。UIC，Commission 7A/16，1992年。在IRSE Proceedings 1992/93，第70[3] A. Cimatti，F. Giunchiglia，G. Mongardi，D. Romano，F. Torielli和P. Traverso，1998年，使用模型检查的铁路联锁系统的形式化验证，形式方面 of Computing，1999，361-380.[4] P. E. Debarbieri，F. Valdambrini，E.安东内利A.C.E. I每个行的操作都有一个简单的二进制文件，方案I-0/19 。CIFI Collana di testi per la Recruitizione agli esami di abilitazione ，Quaderno 12，1987.[5] 欧洲电工标准化委员会，2001，EN 50128，铁路应用通信、信号和处理系统铁路控制和保护系统软件。[6] W. J. Fokkink，P. R.何志华，1998，连锁系统的验证：从控制表到梯形逻辑图，第三届工业关键系统形式化方法研讨会论文集-FMICSM. Banci，A.Fantechi/理论计算机科学电子笔记133（2005）319[7] 联合Foschi，M. Giuliani，A. Morzenti，M. Pradella，P. San Pietro. 正式方法在铁路运输业软件采购中的作用，铁路运营和控制系统正式方法研讨会（FORMS 2003），匈牙利布达佩斯，2003年5月15日至16日。[8] B. Fringuelli，E. Lamma，P. Mello，G.桑托基亚基于知识的铁路车站。在IEEE智能系统，卷：7，问题：6，12月。1992年，第45-52页。[9] D.哈 雷尔Statecharts ： A Visual Formalism for Complex Systems.Sci. Comput. 编 程8（1987），231-274.[10] D. 哈雷尔Lahover，A.Naamad，A.Pnueli，M.波利蒂河Sherman，A.施图尔-特劳林M. 张文，《复杂反应系统的开发环境》，北京大学出版社，2000年。1990年4月，第4页。403-414.[11] D. Harel，A. Pnueli，J. Schmidt和R.谢尔曼关于Statecharts的形式语义学，Proc。第二届IEEESymp.《计算机科学中的逻辑》，Ithaca，NY，1987，pp.54比64[12] D. Harel 和 M. Politi ， Modeling Reactive Systems with Statecharts ： The STATEMATEApproach，McGraw-Hill，1998.（早期版本名为：STATEMATE的语言，I-Logix，Inc.，Andover，MA，1991.）[13] J. Klose，W.陈文，2001，基于STATEMATE验证环境，系统设计中的形式化方法，19（2）。[14] G.科尔克形式化方法：从用户角度看铁路环境中的可能性和困难。工业关键系统形式方法第三届国际研讨会论文集，1998年5月25日至26日，1998年。[15] 尼克劳斯·H Küoenig，StefanEiner欧洲交互式功能需求方法（EIFFRA），铁路运行和控制系统形式方法研讨会（FORMS 2003），匈牙利布达佩斯，2003年5月15-16日[16] 对象 管理 组， 1999,统一建模语言规范，版本1.5http://www.omg.org/technology/documents/formal/uml.htm[17] Statemate Magnum模拟参考手册。 I-Logix Inc.美国马萨诸塞州伯灵顿，2003年。[18] Fokko van Dijk ， Wan Fokkink ， Gea Kolk ， Paul van de Ven and Bas van Vlijmen ， 1998EURIS，分布式互锁的具体化方法，计算机科学讲义，第1516卷。