没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记128(2005)179-194www.elsevier.com/locate/entcsNASA跑道安全监控器拉杜岛西米尼恰努国家航空航天研究所,汉普顿,弗吉尼亚州23666詹弗兰科·恰尔多University of California,Riverside,CA 92521摘要由洛克希德·马丁公司设计的跑道安全监视器(RSM)是美国宇航局减少航空事故计划的一部分。我们开发了RSM协议的Petri网模型,并使用我们的工具SMART的模型检查功能来调查可以归类为RSM中的遗漏警报场景的行为。为了应用离散状态技术并减轻由此产生的状态空间爆炸现象的影响,我们的模型使用了高度离散化的系统视图,该视图通过将监控的跑道区域划分为较小体积的网格并考虑仅涉及两架飞机的场景来获得。该模型还假设没有通信故障,例如来自雷达的错误输入或缺乏传入数据,因此它依赖于所有参与者对现实的一致看法。尽管进行了这些简化,我们还是能够暴露RSM概念设计中的潜在问题。我们的调查结果已转交设计工程师,他们采取了纠正措施。结果强调了我们的工具SMART中实现的新的模型检测算法所达到的高水平的效率,并证明了它们对现实世界的系统的适用性。由于内存消耗过多,使用NuSMV和SPIN验证RSM的尝试失败。保留字: 模型检查,航空安全*部分由美国国家航空航天局(NAG-1-02095)和美国国家科学基金会(NAG-1-02095)资助的工作。0219745号02039711电子邮件地址:radu@nianet.org2 电子邮件地址:ciardo@cs.ucr.edu1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2005.04.011180 R.I. 西米尼恰努湾 Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179-1941介绍随着投入运行的系统的复杂性每年都在增长,现代飞机越来越多的功能转移到基于计算机的自动化设备上。然而,这种复杂性的快速发展并没有与所部署设备的认证程度的同等进步相匹配这是由于分析复杂系统需要大量的资源,包括形式化方法领域提供了一种替代传统测试方法的方法,传统测试方法只能探索有限数量的场景。形式验证使用严格的数学技术来彻底检查系统的模型是否满足一组期望的属性。模型检测自20世纪90年代初以来越来越受欢迎,它是一种完全自动化的技术,依赖于发现模型的可达状态集,并评估以时态逻辑表示的给定属性是否满足。模型通常用建模语言来指定,例如自动机,Petri网或伪代码。如果一个时间属性成立,模型检查将以100%的置信度证明它。当一个属性不成立时,模型检查工具提供了一个反例,以模型中的执行路径的形式,它可以说明错误的来源。在使用这些计算机化工具来验证现代协议时,主要的障碍通常是状态空间爆炸现象。随着模型的大小和复杂性的增加,状态空间的大小也会增加,有时会增加到指数级更大的状态集。然而,模型检测技术的进步,特别是在符号模型检测,已经有可能分析系统的状态空间非常大。模型检验在复杂的、大部分是同步的电路设计的验证中特别成功然而,直到最近,它通常被认为不足以验证大型异步协议和软件。在过去的几年里,我们的研究已经成功地针对类的全局异步本地同步系统,包括一些松散耦合的系统(同构或异构),发展有点彼此独立。最近,NASA和洛克希德·马丁公司已经开始开发一种用于检测跑道事件的协议,称为跑道安全监视器(RSM)[11],这是我们技术的一个很好的候选者。虽然其验证具有挑战性,并将我们的计算资源推向极限,但我们能够发现许多构成潜在危险的有趣场景。然而,同样重要的是,R.I. 西米尼恰努湾Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179181总的来说。相比之下,总数为6。7× 1042个可达状态,这有力地证明了响应空间模型是鲁棒的和安全的.本文其余部分的结构如下。第2节和第3节描述了RSM和我们用于本研究的工具SMART。第4节给出了我们开发的RSM模型的细节,第5节报告了我们的分析结果。最后,第6节总结了我们的工作,并讨论了未来扩展的想法。2跑道安全监控器跑道安全监视器(RSM)是NASA跑道侵入预防系统(RIPS)研究的一个组成部分RSM由洛克希德·马丁公司的工程师设计和实施,旨在纳入集成显示系统(IDS)[2],这是NASA自1993年以来一直在开发的一套驾驶舱系统。IDS还包括其他入侵检测和预防算法,如TCAS II [10]。IDS设计使RSM能够利用现有的数据通信设施、显示器、全球定位系统(GPS)、地面监视系统信息和数据链路。冲突避免协议已经存在并在运行。TCAS [10]自1994年以来一直在使用,现在美国联邦航空局要求所有美国商用飞机都使用TCAS。TCAS有一个完整的正式规范,但由于其复杂性,它只得到了部分验证[3,12]。SATS [1]也在NASA兰利开发中,旨在帮助确保通用航空器在无塔地区机场的安全着陆,并将正式验证。RSM的目的。跑道安全监视器的目标是检测跑道入侵,FAA将其定义为3由于大多数航空安全事故发生在跑道上或附近,跑道安全监视器在避免事故方面发挥着关键作用。RSM不是为了防止入侵,而是为了发现它们并提醒飞行员。 RIPS的其他组件以许多IDS功能的形式提供预防,例如平视显示器、电子移动地图、交通信息驾驶舱显示器洛克希德·马丁公司[11,16]进行的实验研究表明,入侵情况不太可能发生时,IDS技术在飞机上使用。RSM应该大大改善这种积极的效果。3参见http://www.faa.gov/runwaysafety/网站。182 R.I. 西米尼恰努湾 Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179-194返回IDS跑道安全监控器IDS流量监视器获取所有权和交通状态。计算流量数据入侵区侵入试验(each目的物区域高度)侵入区的测试所有权每次交通扫描不需要测试所有权不在区域无区域交通检测到侵入:设置警报标志/数据无侵入:清除警报标志/数据开始/停止/继续侵入测试侵入检测跟踪入侵区域区域内交通运行状态矩阵Fig. 1. RSM算法的顶层设计。响应面设计图1显示了RSM算法的高级架构。 RSM在驾驶舱内安装的设备上运行,并在机场起飞和降落程序之前激活。在每架飞机上运行一个独立的RSM副本,并将其作为本机运行的飞机和其他飞机,使用同一跑道的地面车辆,甚至物理障碍物(如设备)作为目标。RSM监控起飞或着陆跑道周围区域的交通情况。该区域是一个三维空间,从跑道的每个边缘横向延伸到220英尺,在跑道上方高达400英尺的高度,距离每个跑道端部1.1海里(400英尺的高度对应于起飞/着陆轨迹的3°下滑斜率该协议,实现为一个C语言程序,包括一个重复循环的三个主要阶段。在第一阶段,RSM从通过数据链路接收的雷达更新中收集交通信息。它识别监控区域内的每个目标,并存储其3D物理坐标。更新的频率可能不是恒定的,更新可能会丢失,甚至数据可能会出错。数据链接错误或遗漏的影响没有在这项研究中解决,但提出了一个具有挑战性的任务,为未来的研究。这些错误已经成为一些实验测量的主题[16],它们的分析需要一个在我们目前的模型中没有捕获的随机变量,而只关心逻辑错误。在第二阶段中,算法从预定的一组值中为每个目标分配状态,所述预定的一组值包括滑行、预起飞模式、起飞模式、爬升模式、着陆模式、滑跑模式和滑行通过模式。当我们描述我们的系统模型时,我们详细讨论了这些状态的含义。R.I. 西米尼恰努湾Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179183目标→所有权↓出租车 武雄爬升土地推出阿比特鲁出租车takeoclimboutlandrollout-afafafa cf-一 个fdede deadb/c一 个fdede deadb/c一 个fdede deadb/c一个地b/c-bcbc bcbc-a:距离接近b:在takeo/着陆路径c:距离小于最小间距d:在同一方向上起飞/着陆,距离小于最小间隔e:Takeo/在相反方向着陆,距离接近f:在跑道表1用于设置报警的操作状态矩阵。第三阶段负责检测入侵,并根据本船和目标的空间属性(位置,航向,加速度)以及一些逻辑条件对每个目标执行。表1显示了该阶段的运行状态矩阵。我们的分析重点是证明这个决策过程能够检测到所有可能的入侵场景,或者找到RSM未能发出警报的可能入侵场景3SMART工具为了对跑道安全监控器进行建模,我们使用了我们的工具SMART(可靠性和时序的随机和模型检查分析器)[4],该工具是我们为复杂系统的逻辑和随机分析而开发的给出一个系统的形式化描述作为一个(随机)Petri网,SMART可以执行状态空间的建设,验证时间逻辑属性,并提供有效的数值解的时间和随机分析。SMART与大多数其他模型检查器相比有几个优点:• 状态的紧凑(次线性)存储结构[13]。• 状态之间的过渡关系的非常紧凑的编码[7]。• 基于饱和度的高效符号状态空间探索算法[5],一种用于符号模型检验的最先进的迭代方法。• 快速生成反例[8]。SMART接受一个图灵等价版本的Petri网作为输入[14]。每个SMART输入文件定义一个或多个结构化(即,划分为子模型)基于状态的模型。模型可以参数化并定义一组度量,在我们的情况下,可以将其视为通过系统状态探索进行评估的逻辑查询。输入语法在SMART用户手册中有详细说明,可从http://cs.ucr.edu/~ciardo/SMART/。184 R.I. 西米尼恰努湾 Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179-1944RSM的SMART模型为了对响应面建模,我们首先确定代表系统状态的变量然后,我们将这些信息转换为Petri网,输入到SMART。我们将模型划分为3n + 3个子模型,其中n是在区域内移动的目标的数量。前三个子模型的变量描述了所有权的状态。其他n组3个子模型的变量描述每个目标的状态。对于每架飞机,相关属性为:位置:一个三维矢量(x,y,z),其中X轴横跨跑道的宽度,Y轴沿跑道的长度,Z轴垂直。速度和航向:第二个三维矢量(vx,vy,vz)。沿跑道的加速度:ay。状态:枚举类型变量。报警器标记:布尔变量。Phase:一个整数变量。所有其他变量都被认为与我们的研究无关,可以从模型中抽象出来,以减少其状态空间的大小。状态变量的域。由于SMART在离散型系统上操作,因此需要通过离散化进行抽象以处理RSM算法的连续型变量。为了得到变量域的良好表示,我们从可以从协议规范中提取的最粗略的可能离散化作为建模者,我们必须考虑在非常粗糙的离散化(通过将不同的状态折叠成单个代表,可能合并太多有意义的行为最后,我们选择了以下领域:• 坐标x,y,z可以简单地为x,y,z∈ {0, 1, 2},其中0表示在监控区域之外,1表示在附近,2表示在跑道上。然而,我们选择了一个更好的参数表示:x∈{0,.,maxx},y∈ {0,.,maxy},并且z∈ {0,.,maxz},其中0表示区域外,并且常数maxx、maxy和maxz可以根据建模者的偏好进行调整换句话说,location(0, 0, 0)表示区域外的所有位置。 一个目标离开了这个区域,或者还没有进入这个区域,就会被分配到这个位置。作为替代方案,我们可以使用围绕监控区域的R.I. 西米尼恰努湾Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179185211 2 3 4实际轨迹:(51.5,161.3),(128.5,93.6),(220.1,80.3),(318.5,111.2),(371.1,183.1),.离散轨迹:(1,2),(2,1),(3,1),(4,2),(4,2),.离散速度:(+1,-1),(+1,-1),(+1.0),(+1,+1),(+1,+1),.图二. 二维离散目标轨迹这将不必要地增加状态空间,其中形式为(0,y,z)、(x,0,z)、(x,y,0)、(maxx+1,y,z)、(x,maxy+1,z)、(x,y,maxz+1)的条目都表示相同的情况:目标没有被监视。• 速度值vx、vy、vz可以被分配域{0,±1,±2},其中0意味着不移动,±1意味着缓慢移动(低于45节的预定滑行速度阈值TS),并且±2意味着在沿着轴线的任一方向上快速移动(高于TS同样,更好的表示是vx,vy,vz∈{−最大速度,., 0,..., maxspeed},使用另一个参数maxspeed。• 加速度ay有两个相关的值:非负值或负值。• 状态为{out,taxi,pretakeo,takeo,climb,land,rollout,ythru}。• 该阶段处于{雷达更新,设置状态,检测}。目标的三维运动。我们的离散化划分成一个3-D网格中排列的数量的监测区。因此,飞机的可能位置由来自离散域{(0,0,0)}<${1,.,maxx}×{1,.,maxy}× {1,.,maxz}。类似地,连续轨迹由抽象的、离散化的轨迹表示。通过三维网格的细胞。当用离散状态方法对连续变量然后,我们执行以下建模约束:• 仅允许在相邻单元格之间移动。原则上,目标可以自由地保留在当前单元中或移动到相邻的26个单元中的任何一个,对应于坐标x、y和z的不确定性减小、不变或增加。但是,更改必须与标题一致。例如,当vx为正时,x不能减小。图2=4.0t=3.0t=2.5t=3.5不t=2.0186 R.I. 西米尼恰努湾 Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179-194显示了一个例子的离散化轨迹在2-D空间。• 当单元(0,0,0)中的飞行器进入监视区域时,其位置在边界上被非确定性地选择,即,x∈ {1,maxx},y∈{1,maxy},或z=maxz(不是z= 1,因为从下面无法进入地面)。同样,飞机只能从边界离开监测区。• 入口速度参数也是非确定性地选择的,但与入口方向一致。例如,一个目标不能从左边以负的vx进入。这些限制中的每一个都是通过禁止弧和转换警卫在Petri网模型中强制执行的。然而,该模型可能包含不切实际的轨迹。这在验证过程中是可以接受的,只要模型涵盖了所有现实行为。如果一个属性在抽象模型中全局成立,那么它也将在现实模型中成立。然而,如果一个属性不全局成立,我们必须检查SMART生成的相应反例,以确定它是否代表一个现实的场景。地位定义。在执行循环的第二阶段,使用其它状态信息确定性地更新每个飞行器的状态变量。为了对这个阶段进行建模,我们定义状态值如下:out:不在监控区域(x= 0)滑行:在地面上,低速或无跑道航向(1)A(|V x|产品介绍|v y| ≤TS) ∨(vx= 0))takeo take-roll:在地面上,跑道航向,加速(1)A(|v y|>T S)(v x= 0)(a y≥ 0)展开:在地面上,跑道航向,减速(1)A(|v y|>T S)(v x= 0)(a y<0)爬升:空中,有跑道航向,正垂直速度(z >1)地面:空中,有跑道航向,负垂直速度(z>1)空中:空中,而不是在攀登或陆地上 模式(vx/= 0)注意,上面使用的谓词z= 1和z >1也意味着x >0和y >0,因为非监测区由单个单元(0, 0, 0)表示,而不是由状态的边缘表示另外,加速度ay,需要区分R.I. 西米尼恰努湾Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179187最大x×最大y×最大z最大速度1靶2个目标3个目标4个目标模型中的状态数3×5×32 1.0×13104.1×14107.6×15103.4×19108.4×21106.6×23101.1×26101.7×29105.8×31103.5×32103.5×36105.0×39105×10×5210×10×1023×5×35 2.7×14108.3×15101.4×17104.4×21107.6×23105.0×25107.2×28106.9×31101.8×34101.2倍36106.3×39106.7×42105×10×5510×10×105状态空间生成时间(秒)3×5×322.012.933.934.915×10×525.528.2711.1913.9110×10×10213.6220.5827.5034.423×5×354.416.518.7710.985×10×5512.9119.0725.4232.0510×10×10528.4542.8457.2571.75状态空间生成存储器(MB)3×5×322.003.004.004.995×10×527.2110.8114.4118.0110×10×10220.8631.2941.7252.153×5×354.226.338.4410.555×10×5515.4823.2130.9538.6910×10×10539.7359.5979.4599.31表2参数状态空间生成的结果。不需要直接对takeoRoll和rollout状态进行建模,因为其值是基于变量Vy的旧值和新值在现场计算的。状态空间测量。刚才描述的模型可以用作这是进一步分析的基础,因为它捕获了目标在三维空间中的自由运动(RSM的第一阶段)和目标状态分配(RSM的第二阶段)。然后,我们可以直接对第三阶段进行建模,或者定义查询,使用状态和位置变量的组合来确定警报是否已被正确设置我们选择通过向Petri网模型中添加转换来直接对警报的设置进行为了评估核心模型的复杂性,我们收集了针对不同输入参数生成的状态空间的测量结果:目标数量(n),网格大小(maxx×maxy×maxz)和速度阈值(maxspeed)。的状态空间大小、运行时和内存消耗列于表2中。的结果表明,可以为多个目标生成可达性集合, 一个相当大的网格大小,以及在几分钟内的多个速度阈值,使用不到100 MB的内存。5模型检验响应面对于协议的逻辑分析,我们使用了SMART的模型检测模块。模型检测是检验离散状态系统的时序逻辑SMART实现了分支时间计算树逻辑(CTL)[9]。188 R.I. 西米尼恰努湾 Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179-194本舰位置目标位置最小间隔半径起飞(Takeoff)目标=滑行距离最小值分离报警=关闭起飞(Takeoff)目标=滑行距离最小值分离报警=ON出租车(Taxi)目标=滑行距离>最小值分离报警=关闭图三. 无记忆属性的场景(底层)。符号和正式定义。表中的操作状态矩阵 1列出了报警设置标准,如RSM算法文档[11]所示。我们的研究旨在彻底检查这个操作矩阵是否能够检测到所有的入侵场景。两架飞机在最小间隔内的情况,即,在我们的模型的相邻单元格中,没有设置警报变量的情况从现在起称为错过警报场景。以下谓词用于描述感兴趣的属性(下标o和t分别表示ownship和target完成阶段0=检测阶段t=检测(更新完成)Sep.(最小间隔无损失)报警报警o=真(报警已发出)轨道statuso/∈ {taxi,(at至少有一架飞机正在起飞或降落)一个“无记忆”的属性。“ 是 否 存 在 最 小 间 隔 丢 失 且 警 报 关 闭 的跟 踪 状 态 ?“• CTL语法:EF(完成跟踪分离报警)当“距离正在接近”的条件在当前状态中不满足时,会出现导致满足该查询的状态的场景。这是图3的第三个快照的情况。然而,这可能不对应于不想要的行为,因为警报可能已经被设置在先前的状态中,当最小间隔丢失时。报警变量的值还取决于报警是否然而,即使警报老化,这种情况仍然是潜在的问题,因为目标最终可以在比老化持续时间更长的时间内保持恒定距离(小于最小间隔)R.I. 西米尼恰努湾Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179189见图4。 场景2(空中)。导致在警报期满之后的回合中的请注意,查询的“无内存”性质会影响结果。我们在特定的时间快照中查看属性,而不考虑导致当前状态的事件顺序。为了更好地理解系统,我们接下来研究了两个飞机之间的最小间隔距离丢失后系统的状态。分析导致分离损失的过渡。“当 警 报 关 闭 时 , 是 否 存 在 通 过 转 换到 当 前 状 态 而 丢 失 最 小 间 隔 的 状 态 ?“• CTL:EF(done_track_sep_alarm[(<$done)U(done_track_sep_alarm)])注意,查询中的嵌套EU运算符(而不是EX)是due事实上,需要几个状态转换来完成坐标(3)、状态(1)的更新和再次设置警报(1)。 这个查询的见证者(见图4)有一个处于着陆或爬升状态的本机,目标在跑道上的速度比本机快,在间隔内移动与侧面成一定角度。设置报警的条件这种情况是第二个条件没有得到满足,因此没有发出警报。飞机实际上可能会相撞(轨迹相交,如图4所示),而没有一个参与者得到警告。上面的场景是唯一一个为这个查询生成“坏状态”的场景,这一事实证明了RSM的健壮性。这种情况可以通过添加小于最小间隔的距离作为这种状态组合的标准的一部分来纠正。请注意,我们在两个状态(之前和之后)中都包含了谓词跟踪本舰位置目标位置最小间隔半径着陆路径登陆(Landing)目标=飞越距离最小值,9月,不在着陆路径上!报警=关闭登陆(Landing)目标=飞越距离>最小值分离报警=关闭190 R.I. 西米尼恰努湾 Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179-194图五. 场景3(地面)。过渡),因为我们感兴趣的是仅涉及起飞和/或着陆轨迹的场景。然而,这个额外的约束可能会掩盖一些其他不期望的行为。因此,我们接下来要问一个更一般的问题。更强的安全性能。“是否有一个跟踪状态,其中最小间隔丢失,可达到没有以往任何时候都设置警报?“的• CTL:E[(<$alarm)U(done_track_<$sep_alarm)];几个示例场景满足此查询。例1. (见图5)演员进入舞台滑行快,不对准跑道,在近距离彼此。一旦在跑道上,其中一个(说拥有)改变方向,并调整自己的跑道。 此后,它被归类为takeo(或climbout,如果它成为空中)。另一架飞机保持在最小间隔内,但它不会靠近:它可以要么在本舰后面,要么更危险地在本舰前面。没有人发出警报,因为“距离正在接近”的标准再次不满足。如果进入时飞机之间的距离很小,可能没有足够的时间进行逃生机动,即使后来通过关闭设置警报图5显示了一个与安全属性相矛盾的抽象跟踪。所示轨迹是在地面监测区域的水平截面飞机的位置是在每次雷达扫描时给出的。第三个快照说明了系统的实施例2. 对于未被跟踪的机载状态(状态跟踪),也存在相同的情况。实施例3. 还有一些不满足安全属性的额外场景,其中事件在两架飞机进入月球后立即发展。本舰位置目标位置最小间隔半径起飞(Takeoff)目标=滑行距离最小值分离报警=关闭出租车(Taxi)目标=滑行距离最小值分离报警=关闭R.I. 西米尼恰努湾Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179191被包围的区域在这些情况下的不良行为是由于两个平面的先前位置是未知的(在我们的模型中坐标为(0,0,0)),因此它们的距离在当前状态下不能接近。如果飞机在彼此非常接近的位置(例如,两者都试图着陆),则不会升起飞行器。然而,由于我们选择的建模约定,这种不确定性仅由我们的理论模型表现出来,而不是由RSM设备的协议的实际实现表现出来为了总结上述场景的共同特征,我们观察到,关键因素是当失去最小间隔时,两架飞机都是滑行/滑行通过,因此情况没有被跟踪(潜在的不良事件被协议规范掩盖)。随后,谓词为了进一步扩展我们的讨论,我们来看看在达到坏状态之后场景的可能延续。如果在随后的更新之后,距离正在接近,则将发出警告,并且“错过警报”的情况将不复存在。图6是场景3的扩展,图6显示了使问题永久化的唯一方法。如果目标在本舰前方“之字形”移动,它可以在最小间隔半径内停留更长的时间,目标必须曲折前进以保持距离,因为沿着一条平行的路径前进会导致算法将其标记为“采取行动”。新的操作状态组合的报警标准是“在相同方向上进行操作并且距离小于最小间隔”。因此,一旦目标停止锯齿形移动,就会发出警报。当目标不是飞机而是车辆(如服务卡车)时,为目标的“恶意行为”增加了额外的自由度地面车辆总是被认为是滑行模式的协议,无论他们的速度,航向,和物理坐标。因此,如场景4所示,目标可能会在近距离内跟踪本机,甚至在本机排队等待起飞和加速后继续追逐本机出于与场景4相同的原因,将不会产生任何标记对于最新的RSM实施,设计师考虑了我们的发现,并取消了对地面车辆的特殊处理。这解决了场景5中的情况。情景4的情况不那么令人担忧,因为在实践中实现这一点非常困难,即使是破坏者故意实现的同时,暴露它也有一些好处:设计师意识到这种低概率192 R.I. 西米尼恰努湾 Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179-194出租车(Taxi)目标= 滑行距 离 =D 警本舰位置目标位置最小间隔半径起飞(Takeoff)目标 =滑行距 离 =D 警报=关闭出租车(Taxi)目标= 滑行距 离 =D 警本舰位置目标位置最小间隔半径起飞(Takeoff)目标= 滑行距 离 =D 警报=关闭见图6。 情景4(地面)。见图7。 情景5(飞机与车辆)。事件,并且由于这是系统中唯一剩余的不需要的行为,因此它用作RSM算法的阶段3的验证6结论和今后的工作从我们的分析中汲取了几个教训,首先,我们的不良核查方法具有不可否认的价值。在我们的研究结束时,其中大部分与建模决策有关,我们向RSM设计人员提供了一份重要发现的清单,这些发现在不同机场位置已经进行的涉及真实飞机的测试活动中没有暴露出来我们的技术的优点是,除了相当便宜,它是详尽无遗的。我们能够分析模型中所有可能的场景,并发现发生概率极低的潜在问题R.I. 西米尼恰努湾Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179193这些几乎不可能在测试过程中暴露出来,通常一天不超过12次测试,或者模拟会议。当与1013− 1042这表明需要进行详尽的分析。第二个结果我们的实验是,在识别出问题并建议对协议进行修改以消除这些问题之后,我们提高了设计中有关遗漏警报的保证级别。关于假警报的双重分析,这仍然在未来研究计划的清单上。从实际的角度来看,飞行员同样关心这两种情况。个别报告表明,频繁的假警报可能成为一种滋扰,或者更糟的是,在操作飞机时分散注意力。还有一种情况是,具有太多假警报的系统将倾向于被切换或忽略,从而使其实际上无用。因此,必须降低误报警的发生率,即使这些误报警不像误报警那样严重,误报警应该被完全消除。协议的设计者必须提出一个平衡的解决方案,将非常“宽松”的简单性这里没有讨论的另一个方面是容错。我们假设所有场景都是在没有通信故障的情况下发生的,这意味着雷达和数据链路为所有参与者提供准确和及时的更新。我们分析的一个自然扩展是包括错误行为,无论是良性的(错过或延迟更新)或恶意/拜占庭(参与者之间的数据不一致)。这类分析需要在模型中纳入概率方面,这将是进一步研究的主题。虽然我们的工作验证了RSM在无故障假设下的正确操作,但数据链路上的故障可能会严重影响算法的正确操作。设计一个考虑错误数据的模型并不容易,因为现实的错误可能很难建模。一方面,如果所有的数据都是错误的,入侵是完全不可避免的,无论如何好的RSM,否则。另一方面,如果没有数据出错,我们已经证明了算法的正确性。引用[1] V. Ceno,H. Gottlie b s en,R. Butt ler,andS. K alvala。SATS初步概念的模型和分析。NASA兰利技术Rep. 212999,2004年3月。[2] S. Beskenis,D. Green,P. Hyer,and E.约翰逊低能见度着陆和水面作战的综合显示系统。NASA兰利承包商报告208446,1998年7月194 R.I. 西米尼恰努湾 Ciardo/Electronic Notes in Theoretical Computer Science 128(2005)179-194[3] W.昌河Anderson,P. Beame,S. Burns,F.莫杜尼奥湾Notkin和J. Reese。 大型软件规范的模型检查。IEEE TSE,24(7):498[4] G.恰尔多河琼斯,A. Miner和R.西米尼恰努使用SMART进行逻辑和随机建模。计算机性能建模技术和工具。Eval. ,LNCS 2794,pp. 78[5] G. Ciardo,G. Luéttgen和R. 我是你的儿子。 S aturn at ion:用于符号状态空间生成的一种新的逻辑结构。在TACAS328[6] G.恰尔多河Marmorstein和R.西米尼恰努饱和度解除。在TACAS379[7] G. Ciardo和A.矿工。 GSPN的有效Kronecker解的数据结构PNPM 1999年9月22日[8] G. Ciardo和R.西米尼恰努 利用边值决策图符号化产生最短路径。FMCAD256[9] E.M. Clarke和E.A.爱默生使用分支时间时序逻辑设计与综合同步骨架。IBM Workshop on Logicsof Programs,LNCS 131,pp. 52[10] C. Livadas,J. Lygeros和N.A.林奇 TCAS的高级建模和分析。 1999年,1999年,RTSS[11] D.F. 小格林跑道入侵探测和警报的跑道安全监控算法NASA兰利承包商报告211416,2002年1月。[12] 海姆达尔议员TCAS II分析的经验和教训。ISSTA79-83,1996年。[13] A. Miner和G. Ciardo.利用决策图的高效可达集生成与存储。ICATPN1999年6月6日[14] T.村田Petri网:性质,分析和应用。Proc. IEEE 77(4):541-579,1989年4月。[15] D. 琼斯跑道侵入预防系统情况说明书。2000年10[16] J·蒂默曼跑道入侵预防系统,ADS-B和DGPS数据链分析,达拉斯-英尺。沃思国际机场。NASA承包商报告211242,NASA兰利,汉普顿,弗吉尼亚州,2001年11月。
下载后可阅读完整内容,剩余1页未读,立即下载
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- VMP技术解析:Handle块优化与壳模板初始化
- C++ Primer 第四版更新:现代编程风格与标准库
- 计算机系统基础实验:缓冲区溢出攻击(Lab3)
- 中国结算网上业务平台:证券登记操作详解与常见问题
- FPGA驱动的五子棋博弈系统:加速与创新娱乐体验
- 多旋翼飞行器定点位置控制器设计实验
- 基于流量预测与潮汐效应的动态载频优化策略
- SQL练习:查询分析与高级操作
- 海底数据中心散热优化:从MATLAB到动态模拟
- 移动应用作业:MyDiaryBook - Google Material Design 日记APP
- Linux提权技术详解:从内核漏洞到Sudo配置错误
- 93分钟快速入门 LaTeX:从入门到实践
- 5G测试新挑战与罗德与施瓦茨解决方案
- EAS系统性能优化与故障诊断指南
- Java并发编程:JUC核心概念解析与应用
- 数据结构实验报告:基于不同存储结构的线性表和树实现
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)