多列车多轨道系统的控制器设计与形式化分析方法

理论计算机科学电子笔记50卷。1（2001）{Proc.ATMOS 2001网址：http://www.elsevier.nl/locate/entcs/volume50.html15页多列车多轨道系统的控制器设计1迪帕克·卡普尔2新墨西哥大学Victor L. Winter和Raymond S.Berg3桑迪亚国家实验室摘要讨论了多列车多轨道铁路系统控制器的形式化分析与综合方法。该研究的动机是一个案例研究，涉及湾区快速交通（BART）系统。 总体目标是设计一个列车加速控制功能，使列车能够安全放置，但也增加了系统的吞吐量。 使用的建模语言指定的安全性能和控制功能进行说明。HATS系统支持的程序转换方法被用来从控制器的高级规范生成高效的实现。该实现可用于模拟控制器行为，从而进一步增强设计的可信度。 优化变换的性质可以使用基于重写规则的归纳定理证明器重写规则实验室（RRL）来验证。1介绍和动机本文综述了形式化方法和程序转换方法在多列车多轨道系统控制器分析与综合中的应用这项研究的动机是一个涉及湾区快速交通（BART）系统的案例研究[10]。的总体目标在下一节中简要讨论的BART案例研究是开发列车（加速）控制功能，使列车能够安全地间隔得更近，从而增加系统的吞吐量。我们的主要目标是开发一个合适的模型，允许这样一个系统所需的安全属性的正式定义，然后对这些属性的列车模型1 这项工作得到了美国能源部根据合同DE-AC 04 - 94 AL 85000的支持。桑迪亚实验室（Sandia）是一个多项目实验室，由洛克希德·马丁公司下属的桑迪亚公司为美国能源部运营。2 Deepak Kapur也得到了NSF资助的部分支持CCR-9996150和CDA- 9503064。电子邮件地址：kapur@cs.unm.edu3 电子邮件：vlwinte@sandia.gov，rberg@sandia.govc2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2ATMOS 2001 {D.卡普尔河谷Winter和R.Berg本文的结构如下。在概述了BART系统之后，讨论了形式模型和建模语言;更多细节可以在[5] 中找到。引入了两个关键结构：proles 和constraints。Prole是元组的序列，其中每个元组由位置元素和相关联的速度元素组成。一个约束建立在一个prole的概念上，通过使用prole中的元素来定义位置-速度平面中的一个满意区域。列车、轨道、车站和信号都可以用Proles建模，其相关的安全属性可以通过相应的约束来建模。一个列车的运行过程是由一个全球时钟来索引的。火车的行为是由它前面的火车在轨道上的行为决定的。Proles讨论在离散以及连续的条款，相对于位置和速度。离散过程是必要的，因为这是从传感器获得数据的方式。引入连续过程有两个原因：（i）物理列车系统是连续的，以及（ii）因此，大多数安全属性可以直接根据基于连续过程的约束来表示。接着讨论了离散型和连续型之间的映射。定义这些映射的假设和他们的正义相对于安全性质进行了讨论。第4节讨论了控制器算法的设计。给出了控制函数的具体形式。然后，使用HATS将此规范转换为有效的实现，HATS是由Sandia国家实验室的高完整性软件（HIS）计划开发的程序转换系统。净化海港计划的简介载于第五节。通过讨论控制器规格上使用的优化变换，说明了系统的一些特性。 第6节是使用自动推理工具和模拟相结合的模型的验证。基于重写规则的归纳定理证明器重写规则实验室（RRL）[4]用于验证用于从规范生成有效实现的优化转换的正确性;仿真用于通过执行不同的场景来增强设计中的置信度值得一提的是，在这个扩展的AB-由于篇幅的限制，本文是非正式的;有兴趣的读者可以通过查阅[13]获得更多的细节，包括形式定义、定理和性质的精确陈述以及证明。2BART概览BART在旧金山湾区提供重型通勤铁路服务。通常有超过50列火车，大多数由10节车厢组成，正在使用。汽车由1000伏直流电驱动的电动机驱动，“第三轨道”，并使用再生和摩擦制动器。该系统是自动控制的，并且机载操作员在正常操作中的作用有限（例如，当站台空无一人时，他们会向系统发出信号，以便火车可以离开车站，也许在某些特殊情况下，他们会拉下紧急刹车。除了一些小的例外，BART系统由双轨组成：32ATMOS 2001 {D.卡普尔河谷Winter和R.Berg一个轨道朝向一个方向而一个轨道朝向另一个方向（即，这条赛道不是一个循环。）每列火车的前部和后部都有一个加速控制器。在线路的末端，前后控制器被重新定义，列车朝另一个方向行驶。为了服务更多的乘客，BART需要更有效地利用轨道的某些部分。向这些部分添加新的轨道，例如，在旧金山市中心的海湾下和地下铺设一条管道，将是非常昂贵的。出于这些考虑，决定通过将列车间隔得更近来解决吞吐量问题2.1联锁列车控制的另一个主要方面是联锁-管理轨道开关和进入轨道段的相关信号。在BART，联锁由独立于列车（加速）控制的系统处理。列车控制员只会在不同的轨道位置看到“go”或“stop”指示灯，并且只有在允许的情况下才应该进入“gate”。联锁系统的责任是，如果信号发生变化，接近的列车停止为时已晚，联锁系统不应移动道岔在车站站台停车就像在大门前停车一样，尽管有一些额外的控制来确保终点站在精确的位置。3形式化模型我们将多轨道、多列车系统定义为由共享非重叠轨道的一个或多个列车列车必须在轨道上行驶，但须受某些限制，例如在适当情况下在指定车站和信号处停车我们开发了一个模型，一列火车在一条轨道上运行。使用组合性，该模型可以轻松地扩展到单个轨道上的多个列车以及多个轨道。因此，需要考虑一个给定的列车（称为目标列车），并分析其行为相对于它前面的列车在轨道上（称为引导列车）。虽然该模型是实际列车系统的近似值，但它始终捕捉到了列车的显著特征，例如列车从一个加速度到另一个加速度的变化速度以及加速度限制。这些值可以根据列车的当前速度和加速度来确定。通过捕获这种信息，该模型反映了由电动机驱动的大型重物（如火车）的运动所遇到的物理极限。由于使用特定列车技术意味着列车控制中的特定粒度，因此感测/反应周期时间也反映了这些限制。类似地，轨道段的最大速度与一组安全约束一起直接影响列车可以在无人监督的情况下行驶多长时间，因此也约束感测/反应周期的持续时间。在我们的分析中，离散全局时钟时间以该单位测量;在仿真中，假设为1秒间隔。以下事件被认为是灾难性的。4ATMOS 2001 {D.卡普尔河谷Winter和R.Berg(i) 一列火车与另一列火车相撞。(ii) 列车没有在信号或车站停车(iii) 火车超过轨道速度限制（有脱轨的危险）。(iv) 列车不必要地紧急停车。但是请注意，我们认为列车响应异常环境条件（例如，列车在列车前方脱轨假设描述列车状态的传感器在某些已知的误差范围内是正确的，加速命令由电动机正确在这些假设下，事件（i）、（iii）和（iv）可以通过正确的控制函数来避免。假设联锁系统在适当的时间设置信号，则对列车行为做出以下假设：火 车不能瞬间停止;相反，火车需要时间和距离基于其速度和加速度停止。然而，牵引列车的脱轨可能在时间和位置上瞬间发生（参见下文关于模型保守假设的加速度值必须随时间“斜升/斜降”。关于引导列车的行为可以做出有限的假设（例如，它可能脱轨）。给定列车速度s和当前加速度acc，函数NA（s; acc）基于物理加速度列出下一个时间周期中的可能加速度值。假设存在列车模型（参见[10]，了解此类函数的详细解释）。3.1Proles有两个构造，proles和constraints，对列车系统中的组件进行建模。曲线描述了位置和速度之间的关系，其中位置和速度由离散（连续）曲线的离散（连续）时间索引。我们假设有一个全球时钟，由给定轨道上的所有列车、信号和车站共享。给定时间t和火车i，第i列火车的曲线给出了它在时间t的位置和速度。Proles可用于在位置-速度平面中对离散/连续轨迹进行列车系统中的组件建模如下：列车状态-列车状态由位置、速度、加速度三要素组成。train behavior（列车行为）-位置单调递增的列车状态序列。行为序列中的状态由离散时间索引，因此描述了列车在特定时间点的状态离散的列车分布-离散的列车分布是位置-速度元组的序列，并且通过从行为的列车状态中删除加速度参数而从列车参数中获得。离散的列车分布的元素由离散的时间索引。5ATMOS 2001 {D.卡普尔河谷Winter和R.Berg连 续的列车曲线-连续的列车曲线是一组位置-速度-时间三元组，其中位置、速度和时间在有界值范围内是连续的。4track prole-轨道被建模为位置-速度元组的序列，该元组在位置上单调增加，指定轨道上相应速度限制进入的位置。该速度限制延伸到下一个轨道段元组的位置。我们假设轨道段具有与它们相关联的恒定速度限制，因此随时间不变。这种时间不变性使我们能够以一种有意义的方式比较离散的列车proles与轨道proles交 通信号过程和车站信号过程。这些通过位置-速度元组的序列来建模，其中与位置相关联的速度可以随时间波动。 例如，如果信号是绿色的，则信号位置处的速度是该轨道段上允许的最大速度;如果信号是红色的，则信号位置处的速度为0。车站信号也有类似的限制。 在模型中，它是-假设列车联锁系统将适当地操作，避免在列车如此接近信号以致于在不使用紧急停止的情况下它可能不能服从改变的信号的情况下continuous component prole-连续组件prole是一个集合当轨道曲线、列车信号曲线或车站信号曲线用作构造连续曲线的基础时，所产生的位置速度元组。在这些类型的连续proles中，位置和速度值是连续的，并且在值的范围内有界3.2安全性：一个连续的属性由于传感器输出是以离散时间间隔测量的，因此列车系统的组件可以使用离散特性最直接地建模。我们现在面临的任务是正式定义与此模型相关的各种安全属性。这里的问题是，安全属性是描述物理列车系统的行为的连续属性，而不是由感测/反应回路引起的离散视图。安全特性可以通过陈述各种离散特性之间的关系来间接地定义。然后，我们必须从一组给定的离散关系中推断例如，考虑最简单的安全属性之一SP，列车不应超过其行驶的轨道段的速度限制。第一次尝试用我们的离散模型来说明这个属性可能会导致以下结果：令t_ack=（seg_pos_l;s_e_g_speed_l）;;（seg_pos_n;seg_speed_n）>表示（离散）trac_k_prole，并且train_i=<（p_i;s_i）;;（p_m;s_m）>表示对象train_i的prole。4 我们可以把一个连续的火车轮廓作为一个位置-速度元组，由连续时间索引，很像一个离散的轮廓。6def2轨道段速度列车行为安全违法位置ATMOS 2001 {D.卡普尔河谷Winter和R.BergFig. 1. 违反轨道速度限制安全速度（列车;轨道）= 8（1j< n^1tm）：t rac k[j]=（段位置1;段速度1）^t rac k[j+1]=（段位置2;段速度2）^traini[t]=（p;s）^（段位置1p<段位置2）！s段速度1：这里的问题是是否安全速度（火车;轨道），SP？如连续图所示，谓词并不涵盖所有情况。上面给出的安全速度谓词可以扩展到覆盖所示的情况，但问题仍然存在：“是否覆盖了所有情况”？在一个连续的框架中，可以直接说明这样的安全属性。假设目标列车的初始状态满足轨道段速度限制，其行为曲线满足轨道段速度限制所施加的约束，在位置-速度平面中不存在属于轨道的连续表示和列车行为曲线两者的点（即，不发生交叉考虑到安全属性可以在连续框架中陈述的优雅性，我们通过定义将离散proles转换为连续proles的映射将我们的模型扩展到这个框架中，反之亦然。这种映射使我们对模型中相邻离散点之间存在的间隙中发生的事情有了明确的、保守的理解（见3.3节），正是基于这种理解，我们通过满足约束算子正式定义了安全性如第3.5节所3.3连续列车系统提供的传感器信息为我们提供了一个精确的（在给定误差幅度）描述列车在离散1 二的间隔如何在这些离散点之间建立行为模型？问题是，这些离散点之间的列车的连续行为我们通过陈述连续列车proles必须满足的属性来解决这个模型限制，以便与系统提供的离散传感器读数一致，因此，从而约束这些行为。设tp=（p1;s1）;（pn;sn）>表示对应于0的离散分布7def

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