没有合适的资源?快使用搜索试试~ 我知道了~
形式化方法分析自动化飞机接口问题
理论计算机科学电子笔记43(2001)网址:http://www.elsevier.nl/locate/entcs/volume43.html14页用形式化方法约翰·拉什比1计算机科学实验室美国加利福尼亚州门洛帕克,邮编:94025摘要现代客机是高度自动化的,自动化和飞行员之间的接口问题与几起事故有关。我用一个简单的例子,从自动驾驶仪的广泛使用的飞机类型来展示如何正式的方法可以用来分析这些接口的某些方面,并暴露潜在的问题。这个例子用来说明更广泛的论点,即形式方法可以在传统上与之相关的领域之外找到应用,只要感兴趣的现象可以在离散数学中有效地建模。1引言发明微积分是为了解决运动物体的问题。自从牛顿和莱布尼茨创造了微积分的基本符号和技巧以来的几百年里,微积分的方法已经被应用于从流体的运动到生物系统的行为的各种各样令人困惑的问题。这种多产性的原因是众所周知的:微积分的基本概念是非常普遍的,可以用来模拟许多现象(事实上,现在学生通常被介绍给它作为计算方法已被调整,以利用现代计算机的能力(实际上,使这些计算自动化的愿望是数字计算机发展的推动力之一形式方法在这些方面类似于微积分:基本概念非常普遍(即,数理逻辑,它本身的发展是为了支撑整个逻辑学,它最早起源于古典逻辑,1这项研究部分由NASA兰利研究中心通过合同NAS 1 -20334和NAS 1 -00079支持。2001年由Els evierScience B. V. 操作访问和C CB Y-NC-N D链接。1拉什比2试图将理性思维的过程编成法典),并可用于模拟许多现象,它们承认(正在开始)有效的计算过程(如模型检查和定理证明),可用于计算实际问题的这些计算方法很好地利用了现代计算机的能力。我将用一个例子来说明这些观点,这个例子将正式的方法应用于传统上,航空心理学家、认知心理学家和人为因素专家使用实验和描述性方法对该主题进行了研究[1])而且似乎不是正式方法的可能目标。然而,事实证明,认知心理学家已经确立了当人类与任何类型的复杂系统交互时“心智模型”所扮演的核心角色如果人类认知的某些方面可以用状态机来描述,那么我们就可以使用形式化的方法来指定和建模这些方面,从而为计算它们的属性提供有效的手段下一节将描述一个简单的示例来演示这一点。2分析自动化惊喜当自动化系统的行为与其操作员的预期不同时,自动化意外就会发生如果实际的系统行为和操作员的心理模型都被描述为有限状态转换系统,那么基于模型检查的机械化技术可以自动用于发现导致两种这些方案确定了潜在的意外情况,并指出了应考虑设计变更或修订培训材料或程序的领域。心理模型可以由人为因素专家建议,或者可以从培训材料中导出,或者可以表达对“一致”行为的简单要求我和我的同事们之前已经通过将Murφ状态探索系统应用于MD88 [16,17]和A320 [4]自动驾驶仪中的说明性惊喜来证明了这种方法。在本文中,我提供了另一个基于Degani及其同事[5,6]发表的描述的例子。这个例子涉及所有商用飞机类型中部署最广泛的一种的自动驾驶仪,与前面的例子不同之处在于,需要对飞机的动力学进行更多的建模。图1显示了制导控制面板(GCP)的主要元件,该飞机的飞行员使用它来选择和控制自动驾驶仪的垂直飞行模式。有三种主要模式,每种模式都可以通过按下相应的按钮来启用。拉什比3ALT VS垂直速度举行海拔变化水平0052+00011Fig. 1.导航控制面板保持高度:使飞机保持当前高度。改变高度:使飞机飞到GCP顶部中心通过转动GCP中心的ALT转盘来设置该值当达到所需高度时,飞机变为保持高度模式。垂直速度:使飞机以GCP右上角垂直速度窗口中指示的速率爬升或下降(正值表示爬升,负值表示下降)。可通过转动GCP中心右侧的VS指轮来如果在高度窗口中设置的值如果垂直速度窗口指示爬升,则高于当前高度,或者如果垂直速度窗口指示下降,则低于当前高度),则设置限制,并且飞机将在指示高度处平飞并进入保持高度模式;否则,它将以设置的垂直速度无限期地继续爬升或下降。刚才描述的行为似乎相当简单。他们变得更加复杂,如果ALT拨号或VS拇指轮移动时,一种模式已经活跃。例如,如果在改变高度模式下转动高度盘,新的高度将成为目标,而如果转动VS指轮,飞机将转换到垂直速度模式。这里感兴趣的行为是在垂直速度模式下发生的那些行为:如果在该模式下改变VS指轮或ALT拨盘,则飞机将以垂直速度窗口中指示的爬升或下降速率飞行,如果高度窗口中的值“超前”于当前位置,则对爬升进行限制这种行为看起来相当简单,但它受到以下因素的影响:拉什比4存在一种特殊的捕获模式,当飞机接近目标高度时,当设定限制时,该模式自动激活。捕获模式使飞机在设定的高度从爬升或下降到水平飞行进行温和的过渡。在描述这种模式实际上是如何工作的之前,我先描述它可以展示的一些场景在每种情况下,场景开始时,飞行员选择垂直速度模式,上升速率为2,000 fpm,限制为27,000英尺;飞机将按照指示爬升,自动驾驶仪将在通过25,000英尺时自动切换到捕获现在假设在飞行26,000英尺时,飞行员将ALT刻度盘更改为新值。让我们考虑高度窗口中设置的不同值的行为。(i) 如果新值为27,500英尺,飞机将继续上升,并在此高度水平。这似乎是合理的,因为新的值是(ii) 如果新值为26,500英尺,飞机将继续上升,并在此高度水平这似乎也是合理的,因为尽管新的(iii) 如果新值为25,500英尺,飞机将改变方向并下降到该高度并保持水平。前两种情况与垂直速度模式的行为一致,而这一种情况则不同:新的设定高度“落后飞行员如何理解新的行为?一个合理的假设是,捕获模式的行为有些-什么样的变化水平模式,并始终针对设定的高度,无论在垂直速度窗口的设置。产生这些行为的实际机制与上面假设的心理模型大不相同。自动驾驶仪记录自动转换到捕获模式时的高度,并将捕获高度窗口中设置的任何新高度我们的目标是确定心理模型所建议的行为是否会偏离实际机制。我们将通过使用名为Murφ的状态探索工具(一种模型检查器)对其进行建模来探索这些行为 [7]。我在早期的论文[16]中提供了在这个领域使用Murφ的教程介绍,因此在没有对所使用的Murφ结构进行需要记住的一点是,Murφ规范由许多保护规则组成:在每一步中,选择一些在当前状态下保护评估为真的所选规则的主体被执行,这将导致某些状态变量的值发生更改(从而产生新的状态)。Murφ回溯以探索规则可能触发的不同序列,从而检查所有可能的行为和所有可达状态。在每个可达状态中,它检查指定的不变量是否拉什比5Constlo:20;hi:30;类型flightlevels:lo..hi;vertical_modes:枚举{none,hold_alt,vert_speed,change_level,capture};方向:枚举{up,down};是真的,并且停止并打印事件的跟踪(即,规则触发),每当检测到违规时,这些触发都会导致当前状态。在该域中,规则指定飞行员的动作(例如,按下按钮或改变由刻度盘设置的值),那些对应于飞行器的动态特性飞行器当前高度的变化),以及由自动驾驶仪响应于某些事件而执行的那些(例如,当飞机接近目标高度时,转换为捕获模式)。与基于MD-88自动驾驶仪[16]的练习不同,在那里只需要对自动驾驶仪的离散内部状态进行建模,在这里我们还需要对飞机的一些动力学进行建模-因为它的自动驾驶仪行为是由不同事件发生的高度之间的关系决定的。然而,一个非常粗糙的模型就足够了:我们将高度抽象为11个离散的飞行高度层(更少的可能也足够),并允许飞机在模型的每一步在相邻的飞行高度层之间移动。我们还需要记录飞机是上升还是下降,以及其自动驾驶仪的当前垂直模式。这些概念在Murφ中规定如下。为了对自动驾驶仪建模,我们需要状态变量来记录它的电流飞行模式,以及是否对其爬升或下降设置了限制。我们还需要记录飞机当前的飞行高度,它的高度盘的设置,以及它进入捕获模式的飞行高度(这是可变的上限开始)。vspd轮子的设置可以抽象为它是指示向上还是向下,我们还需要记录飞机当前的方向这些状态变量中的大多数的值在被称为飞行模式信号器(FMA)的显示器上呈现给飞行员,并且因此可以被假设为也存在于(并且正确地表示)飞行员的心理模型中然而,FMA中明显缺少上限启动(飞行员不知道其存在)和限制设置。我们所描述的心理模型的任务是从所呈现的其他信息中推断极限集我们在状态变量心理捕获中记录这个推断的值。这些状态变量在Murφ中指定和初始化如下。拉什比结6规则“自动飞行”(flight_mode!没有飞行模式!= hold_alt)current!=alt_dial ==>开始如果方向=向上电流hi,则电流:=电流+1;elsif direction = down current>lothen current:= current-1;结束;规则d:方向规则“手动飞行”flight_mode = none ==> begin如果d =上升电流Hi,则电流:=电流+1; elsif d =下降电流>Lo,则电流:=电流-1; endif;end;end;Varflight_mode:垂直模式;cap_start,current,alt_dial:flightlevels;direction,vspd_wheel:directions;limit_set:boolean;mental_capture:boolean;startstate开始flight_mode:= none;current:=(lo+hi)/2; clearmental_capture;clear cap_start;clear alt_dial;clear direction;clear结束;当自动驾驶仪脱离时(即,飞行模式为无),我们假设飞机否则,飞机处于“自动飞行”状态,拉什比7规则“启动垂直速度”飞行模式!= vert_speed ==> beginflight_mode:= vert_speed;direction:= VSPD_wheel;limit_set:=(direction = up alt_dial >= current)| (direction = down& alt_dial< = current);mental_capture:= limit_set结束;规则“Engage change level”飞行模式!= change_level ==> beginflight_mode:= change_level;如果alt_dial > currentthen方向:=向上; else方向:=向下; endif;limit_set:= true;mental_capture:= limit_set;结束;规则“Engage hold alt”飞行模式!= hold_alt ==> beginflight_mode:= hold_alt;limit_set:= false;mental_capture:= limit_set;结束;下面的规则指定当飞行员按下垂直速度按钮时会发生什么。方向由vspd轮设定(如何设定将在下文中描述),限制设定由alt转盘(也将在下文中描述)设定的值是否在当前飞行高度层的“前方”确定在这种情况下,心理模型与实际的自动化是相同的,因此心理捕获将与限制设置相同。当飞行员按下“改变高度”或“保持高度”按钮时,指定行为的规则是类似的。当飞机“接近”设定高度并且设定了限制时,自动从改变高度或垂直速度转换到捕获模式我们不需要精确地建模“接近”意味着什么,只要基本约束得到满足,就可以简单地拉什比结8规则“到达”flight_mode = capture current = alt_dial ==>beginflight_mode:= hold_alt;limit_set:= false;mental_capture:= false;结束;规则“附近”(飞行模式=改变高度)|flight_mode = vert_speed)&limit_set==>开始flight_mode:= capture;cap_start:= current;结束;请注意,当发生这种转换时,当前飞行高度层将记录在cap start状态变量自动驾驶仪自动从捕获模式转换到保持高度当它到达设定的高度时。接下来,我们指定当飞行员将高度盘调到飞行高度h时会发生什么.如果当前模式是垂直速度,则限制设置是否设置取决于alt表盘的新值是否在然而,如果自动驾驶仪处于捕获模式,则根据高度盘是否在上限起始飞行高度层的“前面”来重新评估限制设置规则:飞行高度规则“更改ALT拨号”h!= alt_dial ==> beginalt_dial:= h;如果飞行模式=垂直速度,则limit_set:=(direction = up alt_dial >= current)| (direction = down& alt_dial< = current);mental_capture:= limit_set;elsif flight_mode = capture thenlimit_set:=(direction = up alt_dial >= cap_start)|(direction = down &alt_dial <=cap_start); flight_mode:= vert_speed;elsif flight_mode = change_levelthen if h > currentthen方向:=向上; else方向:=向下; endif;endif;end;拉什比9规则d:方向rule“change VS thumbwheel”d!=方向==>开始direction:= d;如果飞行模式= hold_alt alt_dial!= current thenflight_mode:= vert_speed;limit_set:=(direction = up alt_dial >= current)| (direction = down& alt_dial< = current);mental_capture:= limit_set;elsif flight_mode = vert_speed则limit_set:=(direction = up alt_dial >= current)| (direction = down& alt_dial< = current);mental_capture:= limit_set;endif;end;end;不变“一致”飞行模式!= none -> mental_capture = limit_set;最后,我们说明了当飞行员改变垂直速度指轮时会发生什么。如果当前飞行模式是垂直速度,或者如果它是保持高度并且高度设置已经从当前飞行高度改变,则飞行模式变为垂直速度,并且限制设置是否取决于高度盘的值是否在我们的目标是检查心理捕捉是否总是与极限集,所以我们指定以下不变量。如果我们现在在这个规范上调用Murφ,它将在几分之一秒内探索几百个状态,并报告不变量一致性可以被证伪,并且它将展示如图2所示的迹线,表明这种行为。2该轨迹与第4页所述的情况类似,只是ALT刻度盘中设置的新值“落后于”自动转换到捕获模式时的值-虽然飞机在以前的情况下捕获了新的高度,但在这里它可以无限制地爬升。Murφ迹线提供的洞察力使我们能够对第4页的场景进行以下补充。(iv) 如果新值是24,500英尺,飞机将无限制爬升观察输入中的微小变化,即高度窗口中设置的新值,如何导致广泛不同的行为,如下表所示。[2]实际上,Murφ找到了一个比这短得多的反例跟踪;为了简化与其他场景的比较,我禁用了Engage change level和change VS thumb- wheel规则,并在consistent中的先行词中添加了表达式current>cap start alt dial>(lo+hi)/2,从而使Murφ找到了这个特定的跟踪。拉什比10启动状态启动状态0已启动。飞行模式:无cap_start:20current:24alt_dial:20direction:upvspd_wheel:uplimit_set:falsemental_capture:false规则更改_GCP_alt,h:27被解雇。alt_dial:27规则启动垂直速度发射。flight_mode:vert_speedlimit_set:truemental_capture:true规则自动飞行发射。当前:26规则自动飞行发射。当前:27差点被开除。flight_mode:capturecap_start:27规则更改_GCP_alt,h:26次击发。跟踪的最后状态(完整)是:flight_mode:vert_speedcap_start:27current:28alt_dial:26direction:upvspd_wheel:uplimit_set:falsemental_capture:true图二、由Murφ发现的反例迹拉什比11高度窗口中的值行为26,500爬升捕获25,500下降和捕获24,500无限制我们对Murφ的分析揭示了一种情况,在这种情况下,虚拟的心理模型与实际自动化的行为不同,从而突出了一个潜在的自动化惊喜。1989年,一个船员经历了这种惊喜。Degani和Heymann [5]提供了以下事件报告,从[2]中转述。“在爬升到27,000英尺并离开26,500英尺时,孟菲斯中心给了我们一个下降到24,000英尺的许可。当副驾驶在GCP高度设置上选择24,000英尺时,飞机进入了“捕获”模式。飞机继续以每分钟约300英尺速度爬升。没有高度警告,这个在28,500英尺的高度,孟菲斯中心询问我们的高度,我回答28,500,并立即开始下降到24,000英尺。“高度骤降”是飞行员的行话,指的是飞机偏离指定高度的情况--可能侵入指定给另一架飞机的我们假设了导致这种惊讶的心理模型,注意到在大多数情况下,飞机确实会捕捉到新的高度。Javaux和Polson [12]指出,飞行员的心理模型关注的是常见的情况,所以这个模型在心理学上是合理的。然而,飞行员应该按照制造商及其公司的既定程序操作飞机我无法获得这些程序的描述,但Degani等人[6]提供了相关自动驾驶仪培训手册中的信息。培训手册的部分目的是诱导适当的心理模型,因此值得研究这一描述。培训手册指出,在捕获模式下改变ALT拨盘会导致返回到垂直速度模式;隐含地,进入该模式的通常规则将确定爬升或下降是否有限制(即,如果新值在当前高度的“前面”,则将设置限制)它只需要修改Murφ规范中的几行代码,就可以实现对心理捕获操作的更改。然后,穆尔φ产生了一个与第4页情景(iii)类似的反例轨迹,表明这种心理模型也允许意外。很容易确定的是,由训练手册诱导的模型只会导致这样的意外,即当心理模型期望无约束的爬升或下降时,飞机进行捕获飞行,而原始的有没有可能某种拉什比12不幸的是,这是不可能的。自动驾驶仪的某些行为由高度窗口中设置的新值与进入捕获模式的高度之间的关系决定。后一信息(即,CAP起始高度)简单地不呈现给飞行员3,因此不可能构建其状态基于飞行员可利用的信息的心理模型,该心理模型精确地跟踪真实自动驾驶仪的行为。我的观点(与其他考虑过这个例子的人分享[5,6])是,这个自动驾驶仪的行为是不可接受的,它应该被认为是一个有缺陷的设计。自动化系统可能具有复杂的内部逻辑,并且该逻辑可能依赖于不在其用户界面上显示的状态变量,但是其操作应该使得相对简单的心智模型可以准确地预测其用户的动作的后果。第11页报道的自动化意外的受害者正确地将其归因于设计缺陷,并建议进行纠正(从[2]中转述)。“如果联邦航空局要求制造商将逻辑输入计算机,以便在达到巡航高度之前选择较低的高度时,不允许飞机爬升到最后指定的高度以上,那么这个问题在认证期间可以得到缓解。这是一个设计缺陷,应该得到纠正。”建议的修正可以避免海拔高度的暴跌,但在我看来,这并不支持一个简单而准确的心理模型。将支持这种模型的校正包括高度窗口的灯,如果捕获将发生则该灯被照亮(即,如果限制设置为真),或者是一个更激进的重新设计,其中在捕获模式下转动ALT转盘会导致返回到水平变化(而不是垂直速度)模式。3讨论这里提出的分析方法的一个局限性是,我们只对人机交互中涉及的认知过程的一小部分进行建模该方法是沉默的,例如,在问题上,可能是由于操作员的困难,在回忆正确的心理模型,或对操作员的注意力过度的要求。Bowman和Faconti [3]以及Duke和Duce [8]的工作非常有趣,他们将形式化方法应用于更深层次的认知模型,这使他们能够检测出与这里描述的自动化意外不同的问题。我认为所有这些方法都是相互补充的,并且代表了一个非常有前途的总体方向:通过使用机械化的形式化方法将系统的设计与人类认知的某些方面的模型进行明确比较来检测潜在的人为因素问题认知的不同方面的模型可能揭示不同类型的问题,3飞行员可以监视FMA转换到捕获模式,然后注意高度计阅读,但这似乎只在理论上可行,并不符合飞行器的实际责任,也不符合驾驶舱自动化的意图。拉什比13lems。这里描述的方法使用简单的心理模型来发现导致自动化意外的设计缺陷,并且似乎非常有效。开发Mur φ是为了支持异步通信协议的建模和分析,其主要应用是处理器 缓 存 一 致 性 协 议 ( 参 见 www.example.com 上 的 Mur φ 主 页http://verify.stanford)。edu/dill/murphi.html)。然而,我发现对自动驾驶仪及其心理模型进行建模非常方便。在我看来,形式化方法在“其他地方”成功使用的关键,而不是在硬件和协议设计的传统应用中,是使用有效的工具,而不是过度致力于特定的表达模式或计算模型。Mur φ,以其简单的保护规则和方便的符号编程他们的身体,已被证明是有效的领域相当远离其原来的应用程序(例如,我的同事和我也用它来获得不同Al-出租的容错性的定量估计许多传统科学的研究,如物理学、化学、生物学,甚至心理学,最近都开始基于数学模型的模拟和计算。我相信,形式化方法,通过为有限模型的枚举和无限模型的符号化探索提供有效的方法,将成为这些科学中的关键技术,并在远离其起源的许多引用[1] Kathy Abbott,Jean-Jacques Speyer,and Guy Boy,editors. 国际会议人机交互在航空:HCI-Aero 2000,图卢兹,法国,2000年9月。 C e'padu e`s-E'ditions.[2] ASRS报告113722。NASA航空安全报告系统(ASRS),1989年6月。ASRS数据库搜索可在http://nasdac.faa.gov/asp/asy_asrs.asp上找到。[3] 霍华德·鲍曼和乔治·法康蒂。使用LOTOS和Mexitl分析认知行为Formal Aspectsof Computing,11(2):132[4] 朱迪思·克劳丹尼斯·贾沃和约翰·拉什比将人为因素整合到自动化设计中的模型 和 机 械 化 方 法 。 在 Abbott 等 人 [1] , 第 163-168 页 中 。http://www.csl.sri.com/reports/html/hci-aero00.html网站。[5] Asaf Degani和Michael Heymann。飞行员-自动驾驶仪交互:一个正式的观点。在Abbott等人[1],第157[6] Asaf Degani,Michael Heymann,George Meyer,and Michael Shafto.人机交互的一些形式方面。技术报告NASA/TM[7] David L.迪尔Murφ验证系统。在Rajeev Zurr和Thomas A. Henzinger编辑,计算机辅助验证,CAV史普林格出版社拉什比14[8] 大卫·杜克和大卫·杜斯 认知体系结构的形式化,它的应用推理人机交互。Formal Aspects of Computing,11(6):665[9] 机组人员和现代驾驶舱系统之间的接口。FAA人为因素小组报告,联邦航空管理局,1995年。可在http://www.faa.gov/avr/afs/interfac.pdf网站。[10] 李工帕特里克·林肯和约翰·拉什比。拜占庭协议与认证:在容忍混合和链路故障的观察和应用。在Ravishankar K.放大图片作者:Michele Morganti,W. KentFuchs和Virgil Gligor,编辑,Dependency Computing for Critical Applications-5,Dependency Computing and Fault Tolerant Systems的第10卷,第139-157页,Champaign,IL,1995年9月。IEEE计算机协会。[11] DenisJ av aux和Ve'roniqueDeKeyse r,编辑。第三届人因失误、安全和系统开发研讨会(HESD'99)主席,比利时列日大学,1999年6月[12] 作者声明:John W.波尔森一种在与有限状态机交互时预测错误的方法。在Javaux和Keyser [11]中。也出现在可靠性工程和系统安全。[13] 菲利普·N约翰逊·莱尔德心理模型,认知科学系列第6卷。哈佛大学出版社,马萨诸塞州剑桥,1983年。[14] 菲利普·N约翰逊·莱尔德计算机与心智:认知科学导论。北京:北京大学出版社.[15] 史蒂文·平克。头脑是如何工作的W. W. 诺顿,纽约州纽约市,1997年。[16] 约翰·拉什比使用模型检查来帮助发现模式混淆和其他自动化意外。在Javaux和 Keyser [11] 中 。 修 订 版 出 现 在 可 靠 性 工 程 和 系 统 安 全 ; 预 印 本 可 在www.example.com上http://www.csl。sri.com/papers/hessd99/.[17] 约翰·拉什比朱迪思·克劳和埃弗雷特·帕尔默 一种检测潜在模式混淆的自动化方法。第18届AIAA/IEEE数字航空电子系统会议,密苏里州圣路易斯,1999年10月。http://www.csl.sri.com/papers/dasc99/.
下载后可阅读完整内容,剩余1页未读,立即下载
![doc](https://img-home.csdnimg.cn/images/20210720083327.png)
![rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.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)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)