整合了人为因素的自动化设计模型和机械化方法

整合了人为因素的自动化设计模型和机械化方法

Judith Crow

Computer Science Laboratory，SRI International，Menlo Park CA 94025，USA，crow@csl.sri.com

Denis Javaux

University of Liège，Work Psychology Dept，FAPSE-ULG.Bat.B-32，4000Sart-Tilman，Belgium，d.javaux@ulg.ac.be

John Rushby

Computer Science Laboratory，SRI International，Menlo Park CA 94025，USA，rushby@csl.sri.com

摘　　要

近来，人为因素和形式化方法研究群体逐渐汇合，为计算、预测、分析复杂航空系统及其操作者表现的协同工作指明了新方向。此前已表明完全自动化、有限状态验证技术可用来确定现有系统模式混淆的可能来源；本文将这些技术用于新系统设计。我们用一个简单的例子来说明如何使用自动化有限状态技术探索自动驾驶仪设计选择，然后给出这一技术的其他应用，比如验证源自经验的、自动驾驶行为的最小智力模型。

关键词：人为因素，形式化方法，有限状态机，自动化，设计。

1　模型、方法和机械化

航空心理学以及人为因素（Human Factors，HF）方面的研究为评估现代航空器的人-计算机界面和系统提供了有价值的视角和有效方法。然而，这些方法一般都是经验主义的，而且是后验的：它们依赖调查问卷（例如，［17，19］），仿真试验（例如，［17，18，19］）或报告系统（例如，［22］），因此仅适用于航空器、原型机或者原型模拟机可利用的情况。这些方法是进行描述而不是分析，因此，在系统设计过程中应用人为因素知识大部分是非正规的，往往基于Billins提出的“以人为中心”的设计［1］这样一些准则。

按照DO-178B/ED-12B（机载软件认证建议）的用语，这类非正规的过程构成了“评论”，区别于“分析”：“分析过程为正确性提供可重复的证据，评论过程则定性评估正确性”［14第6.3节］。我们感兴趣的是能不能开发一些分析方法用以增强当前和以后设计中关于人为因素的评述结论。

人为因素领域的一些研究人员在这个方向上已经开辟了一条途径。利用系统和认知建模等领域的技术，他们开发了自动化的模型、驾驶员模型以及界面模型。由于模型具有预测属性，在自动化设计的最初阶段可以运用这些模型为几种形式的分析提供支持。这方面最新趋势的例子包括［3，8，13，20，23］。

描述自动化行为是这些建模方法的前提条件。因此，有关人为因素研究人员提出了他们自己的自动驾驶行为描述：Degani的OFM形式化方法［3］，Sherry等人的操作程序表（Operational Procedure Tables，OPT）［20］，Vakil和Hansman的结合控制方块图与模式转换矩阵的“混合”模型［23］，以及Javaux［6］的模式转换条件图。这些描述都与计算机科学家使用的形式化方法非常相似，依赖于将自动化系统建模为有限状态机的概念。

“形式化方法”（Formal Method，MF）是计算机科学的一个分支，使用数学逻辑结构对自动化系统的行为进行建模，可以用机械化定理证明器和模型检查器进行非常强有力的分析。有限状态机是FM中用到的一种形式化方法，最近研究人员在驾驶舱自动化中开始运用这种方法。例如，Butler等人［2］研究了自动驾驶的一致性表现，Leveson等人［11］探索那些特别容易出错的结构，Rushby［15］将自动驾驶与似真智能模型比较。Leveson和Palmer［10］，以及Rushby、Crow和Palmer［16］具体说明如何使用他们的方法预测MD-88自动驾驶仪中的已知的自动化意外［12］。

HF和FM领域的建模方法逐渐汇合，意味着开发新方法时这两个领域都应该受到关注：人为因素领域让我们认识到什么需要建模以及怎样建模，FM领域提供对模型进行细节研究的符号表示和工具。本文的目的是探索这种合成的方法是如何支持设计时使用的机械化分析，使之达到比非正规的评论更好的完整性、可重复性和客观性。

1.1　支持设计过程

如上所述，困难之处是，建立的模型、方法和工具能够干预自动化设计的前期过程并且适用于指定的自动化高运转状态。模型可以用来预测特定情况下的自动化行为，反映作为智能模型基础的心理过程以及这些过程影响使用者对自动化系统的行为方式，并获取人-机界面的相互作用信息（包括安全性和性能）。

解决这些问题，是HF和FM领域的主要挑战。提供答案和解决方案，开发新的设计技术设计人员可以在设计的前期就能测试替代方案，进而充实传统的自动化原型技术。为了说明这些技术在自动化设计中的应用，我们举两个例子——检测和避免意外情况，调查自动驾驶行为的不完备智能模型。

1.1.1　检测和避免意外情况

第一个例子基于A320自动速度保护。这种保护用来避免超速和触发自动模式转换。

A320的自动速度保护

V/S FPA是一种垂直模式，允许飞行员以一个特定的垂直速度（V/S子模式）或航迹倾角（FPA子模式）控制垂直轨迹。目标垂直速度由飞行员通过飞行控制单元（Flight Control Unit，FCU）给出，范围是-6000ft/min到＋6000ft/min（-9.9°到＋9.9°）。当V/S FPA接通时，如果自动油门被激活的话，它将自动接通SPEED（或者马赫数）控制模式。SPEED模式控制发动机的推力以维持空速达到FCU选定的第二个目标值。

V/S FPA和SPEED一起工作实现各自的控制目标（垂直速度和空速），但V/S FPA处于优先地位。例如，需要下降时，V/S FPA控制俯仰姿态获得目标垂直速度。SPEED减小发动机推力，甚至可能降至慢车状态，避免增加空速（飞机正在下降），远离目标空速。但是，如果控制的下降率太大（例如，6000ft/min），即使采用慢车推力也不够，这样空速会开始增加并且超过FCU上选定的空速值。由于垂直速度优先于空速，V/S FPA将保持相同的俯仰姿态。

为了避免空速达到危险值（比如，抖振速度），A320自动驾驶仪内置自动速度保护，当空速达到当前的气动构型允许的最大速度（VMAX或者Vfe）时，用OPEN模式替代V/S FPA模式。OPEN模式是爬升或下降模式，没有特定的垂直速度目标而且空速处于优先地位。

使用FCU选定目标高度在决定OPEN模式取代V/S FPA的过程中十分重要，如果FCU选择的目标高度低于当前高度OP DES（开始下降）接通，否则OP CLB（开始爬升）接通（即FCU选定的目标高度高于当前高度）。下降时启用自动速度保护意味着OP DES会取代V/S FPA，俯仰姿态立刻减少，空速减少到FCU给定的目标值。

保护方案在这种情况下非常有效，解决了V/S FPA接通并有大下降率引发的各种问题。尽管自动化速度保护实现了保护空速的目标，但是它还会使得飞机的飞行状态与飞行员的意图出现巨大偏差。

1.1.2　自动化意外

当飞机接通V/S　FPA开始进近下降时，会发生不可预料突然的相互作用。例如，如果空中交通管制（ATC）要求推迟降落，在最终进近时改平。当ATC允许飞行员重新下降时，飞机位于下滑道上不得不急剧下降以获取正常的下降航迹。在这种情况下空中客车公司建议使用V/S FPA，将FCU选取的高度设定为复飞高度（在复飞的情况下）。当飞机已经低于复飞高度时采取该行动，这样FCU选取的高度变成了高于飞机的目标值——在正常运行时非常少见。

如果飞行员关注空速不够，过早放襟翼，就会出现自动速度保护问题，襟翼展开时，最大允许速度会自动降为Vfe，也就是设定襟翼展开对应的标牌速度。如果襟翼在空速降到低于Vfe之前展开，飞机就会超速。

这种情况下会返回到OPEN模式，但是由于FCU目标高度已设定为高于飞机的复飞高度，自动驾驶仪将不会进入到OP DES模式，而是进入OP CLB模式（如图1）。飞行员面临着两个自动化意外问题：原本想下降，模式复原同时飞机开始爬升。

图1　V/SFPA复原为OP CLB

这种事件在航线运行中发生过好几次。因此，空中客车公司决定为客户提供一套不能复原为OPEN模式的全面超速保护。代之以V/S FPA模式依然执行，自动驾驶同时调整目标垂直速度维持空速低于最大可接受速度。A330和A340尚未采用类似的设计。

从人为因素的角度解释此类事件的发生。自动化意外与自动化行为的不完整的智力模型有关［11］。自动速度保护很少见，即使飞行员曾经经历过，由于频率效应可能就不会那么重视了［7］。此外，预料模式复原是一个复杂的认知操作［6］：飞行员需要回忆一系列步骤（即类似思维模式的转换），联系起来预测到襟翼展开时会导致超速，同时查看以下情况，接通V/S FPA，将FCU选定高度设定在飞机高度之上（与平常不同）。这远不像放下襟翼这么简单。

设计自动化时我们希望能够预测这种潜在的异常现象，探索不同的设计方案以减少这类现象。一种方法是进行设计模拟，但这会引发如何选择运行场景以及如何检查表现等问题。有一种形式化方法技术叫做模型检查，可以检测所有可能的场景，核查与预想的不变量或智能模型的不同之处。

1.2　设计的机械化分析

这里介绍的机械化分析是在斯坦福大学Murphi状态探测系统中进行的［4］，所用验证技术的详细描述见［15］。因篇幅有限，我们概括性地介绍该方法，略去详细的分析过程。

其基本思想是构建一个A320自动化相关的状态机模型，然后探索模型的所有可能场景。通过评价每一步中的不变量，检查一致性行为的简单期望。对于更复杂的期望而言，可以对比检查自动化状态和智能模型状态，这也可以描述成状态机。由于模型提炼后只需要考虑有限的几个状态，因此进行状态开发，多次检查模型可以涉及所有可能的场景。在这个例子中，进行建模我们既不需要飞机的准确速度，也不需要保护限制的值，需要的只是飞机是高于还是低于有关限制，仅仅使用几个值能否反映出这些关系。

在Murphi中进行系统建模时要给定系统的状态参数，和描述系统执行行动的一系列规则以及系统执行行动的环境。一些或全部状态下具有的特性分别设定为断言或者不变量。然后，Murphi对系统进行全面模拟，研究所有可能的行为，验证指定性能确实满足所有可达状态。如果特性未保持，Murphi进行错误跟踪，描述出现违反的场景。

提取我们的分析结果时，自动驾驶仪的表现可以用6个状态变量来表示，分别代表垂直模式，FCU选定高度，最大速度限制，航空器速度，飞行阶段（如下降）和襟翼构型。襟翼构型进一步抽象成Boolean变量显示襟翼是否展开，除了襟翼构型以外，这些变量都在一组未解释的常量集合之上变动。例如，反映当前飞机最大允许速度的变量可以是两个值中的一个，VMAX或V_fe，分别代表V/S FPA和“襟翼展开”模式下的最大允许速度。对这个简单的例子进行编码大约使用了10个Murphi规则，包括“开始状态”规则，用来指定系统的初始状态。在我们的模型中，初始状态对应于正常降落时飞机的构型：垂直模式为V/S FPA，FCU高度低于飞机高度，最大速度为VMAX，飞机速度低于VMAX，飞行阶段是下降和襟翼收上。其他Murphi规则对应于接通V/S FPA模式，采用OPEN模式，设定襟翼，在FCU输入复飞高度，增加、减少或维持飞机的速度，等等。

显然只有这个简单的部分反映自动驾驶逻辑模式的Murphi模型，我们能够探索超速保护机制的设计选项。假设我们正在设计一种机制并要分析自动驾驶从V/S FPA模式转换为OPEN模式（获取独立于FMGS输入的高度限制的FCU选定高度）的超速保护行为。如果航空器速度超过当前最大允许速度，我们的模型选择或者VMAX或者V_fe。为了探讨这种设计方案，我们只需要添加一个Murphi规则约束超速情况，以及一个反映自动驾驶表现基本预期的不变量。例如，如果我们指定飞机正在下降，自动驾驶仪将永远不会转到OP CLB模式。如果现在我们允许Murphi进行状态探索（在所有可能的情况下激活指定的规则），我们会发现在超速保护机制和OPEN模式的模式逻辑之间存在不可预料的和可能很危险的耦合，如果飞机放下襟翼下降同时其高度低于FCU选定高度，那么会选择OP CLB而不是OP DES。

这种行为（相当于上面所描述的自动化意外）不合要求，所以我们考虑另外一种超速保护机制。如果飞机的速度超过了V/S FPA中的最大允许速度，我们不转换到OPEN模式，我们仍然选择V/S FPA模式，但减慢飞行员指令的目标垂直速度。如果我们修改Murphi的超速条件规则，重复进行状态探索，就不会发现问题。正是由于这些优点我们才强烈赞成这第两种设计。

当然，这个例子是以往A320设计已知事件的事后重构，但是它说明了如何使用有限状态验证技术探索设计选择并在开发的早期阶段给出设计选项。

到目前为止所描述的垂直模式逻辑的Murphi模型仅给出了系统模型和表达为不变量的简单预期。如果我们加上明确描述驾驶员模式逻辑的智力模型（再一次使用［15］中的技术），我们可以深入探索与驾驶员互动相关的自动驾驶设计。例如，按照［6，7］，我们假设驾驶员积累的经验和培训引出略去了很少遇到的转换情况的简易智力模型，然后我们拿新的或改进的设计与简易驾驶员智力模型的设计进行对比，看看能否以潜在不安全的方法区别出彼此。

回到我们的例子，在进近的下降过程中从V/S FPA自动转换为OP CLB模式相当少见，这样的话也可以提出不含这种转换的一般智力模型。不出所料，当我们针对第一个超速保护机制将Murphi系统模型与简易的智力模型进行验证对比时，Murphi报告差错迹象，相当于事故征候中反映的自动化意外。一般驾驶员模型预测出的V/S FPA模式与垂直模式逻辑计算出来的OP CLB模式不同。

1.3　不完备的智力模型

智力或者概念模型的想法是很多最近发表的关于飞行员自动化交互作用文章的核心内容［7，15，20，21，23］。智力模式影响使用者的行为，因而对安全产生影响。因为它们通常是系统行为的简单和不完整的反映（参见文献［7，15］），一个重要的问题是在何种程度上可以简化这些模型同时不影响运行安全和效率。我们把最简化的模型称为最小安全智力模型。

1.3.1　最小安全智力模型

目前，Javaux正在为空中客车公司做一项研究，确定安全熟练地操作A340-200/300自动驾驶仪要求的最小智力模型［8］。

使用逆向设计描述自动驾驶行为，编写问卷调查这个问题。问卷已提交给7名空中客车教员和试飞员。针对A340-200/300上268种可能的模式转换场景，要求专家们给出每种条件的重要性等级。（亦即，“如果驾驶员没有认识到开始转换时必须满足这种条件，驾驶员-自动化系统的安全性怎么样？”）图2给出了典型的结果。它描述了两个自动驾驶仪接通的情形（使用Javaux图表，见［6］）。条件下的数字对应专家给出的平均评分（1表示“一点都不重要”，4表示“非常重要”）。

图2　使用双自动驾驶仪的评分图表

定义阈值为2.5（1和4之间的中间值），出现了下面的使用双自动驾驶仪的最小安全模型（图3）。

图3　使用双自动驾驶仪的最小安全智力模型

通过这种主观评估方法获取的结果可靠性怎么样呢？当被问及他们对各种条件进行评分的方法时，专家们解释说他们寻找忽略威胁安全条件的情况或场景。他们利用自己的经验和事故征候及事故记忆发现典型疑难案例。但是探索式的方法缺乏系统性和全面性，很可能错过一些相关情况，就好像它在OP CLB自动化意外情景中显现的那样。空中客车公司以往的研究结果表明：在一些模式转换中专家的评分是一致的，但是在其他模式转换中却差异显著。这些结果说明主观评价技术的局限性。

1.3.2　最小智力模型的安全分析

FM技术和工具提供了一种途径来评估和量化源自主观评估的变化性。使用前面已经采用的有限状态验证技术，我们可以验证一个给定的模型对自动驾驶来说是否既是最小又是安全的。采用有限状态验证技术解决设计时最小智力模型的辨识问题，有几种方法可用。假定想要高效地研究一系列精神现象的模型，我们建议将Javaux规则评分方案编码直接运用于驾驶员行为的Murphi模型，因此允许我们使用参数表示对一给定验证运行模型的选取，重复对不同的复杂程度（增加了还是减少了）和规则条件评分（低了还是高了）测试模型。

比较等级增强型模型和实际系统或者经过有限状态验证技术改进的模型，使我们可以确定驾驶员行为的最小模型是否符合实际的系统设计，从而肯定（或拒绝）源于经验的最小模型，预测在飞行员和系统模型有分歧那些方面的自动化意外。有了这些信息以后，系统分析师和设计师有机会做出明智的决策，即为了保持驾驶员和系统模式逻辑模型不分歧，同时预测给出附加的驾驶员提示或培训的有效位置，应该在哪里采用“以人为中心”的设计原则。

最小安全模型的概念肯定是对给定航空器模型而言。然而，一旦验证了某个特定的最小智力模型的安全性，我们也可以在下一代航空器设计上运用该模型，用以预测设计决策和飞行员训练的收敛和发散区域。

2　讨论

以往形式化方法的研究一直缺乏智力模型，而人为因素的研究却缺乏自动化可重复的方法和工具。这里介绍的方法考虑这两个缺陷。本文表明在设计领域的自动化开发阶段采用心理学上的智力模型很重要，同时，反过来，在航空系统的设计阶段采用完全自动化可重复的方法分析这些模型并使用这些方法计算和预测可能的自动化意外也很重要。

致力于理解和减少自动化系统中操作人员差错来源的交叉学科，人-计算机交互（Human-Computer　Interaction，HCI）做了很多有意义的工作。文中给出的组合方法，扩充了人为因素和形式化方法的研究，旨在补充和提高，但不是取代人-机交互领域正在进行的工作。我们的思路是使用已有的有限状态验证方法和工具，核查源于经验的驾驶员行为的智力模型，同时计算这些模型用于驾驶员-自动驾驶仪交互设计的结果。该思路的新颖之处在于我们结合了人的因素和形式化方法领域的方法和工具，并利用这些技术来自动分析系统设计的性能，而大多数以前的工作主要是基于这些学科中的一个或另外一个，使用手工方法分析系统部署的人工特征（包括自动化意外）。我们认为自动化可作为一种有价值的辅助手段，但肯定不能取代人对设计规范的详细审查。全面搜索设计空间和由有限状态验证技术提供的差错踪迹，是很有价值的，可以方便地引入现有的人工审查程序。

在将来，我们计划将这种结合方法运用于更大的例子，采用更加逼真的设计评价其效能，可能还包括Javaux的A340-200/300模型。我们还打算利用该技术进一步探索使用不完整或不合适智力模式的后果，包括：正常行为的智力模型和带一个或多个反常模式的系统模型之间的交互效应；研究多重智力模型之间的交互效应（比如，为每个机组成员建立的模型）；预先准备和评估用于训练材料和检查单的指南。

3　致谢

Denis Javaux的工作得到了空中客车公司的大力支持。Judith Crow和John Rushby的工作受到SRI国际和DARPA美国空军罗马试验室F30602-96-C-0204合同的支持。

参考文献

［1］Charles Billings.Aviation Automation.The Search for a Human-Centered Approach.Lawrence Erlbaum Associates，Mahwah，NJ，1997.

［2］Ricky Butler，Steven Miller，James Potts，Victor Carre1o.A formal methods approach to the analysis of mode confusion.In 17^th AIAA/IEEE Digital Avionics Systems Conference，Bellevue，WA，October 1998.

［3］Asaf Degani.Modeling Human-Machine Systems：On Modes，Error，and Patterns of Interaction.Ph.D.thesis，Georgia Institute of Technology，1996.

［4］David Dill.The Murphi verification system.In Rajeev Alur and Thomas Henzinger，editors，Computer-Aided Verification，CAV'96，volume 1102of Lecture Notes in Computer Science，pages 390-393，New Brunswick，NJ，July/August 1996.

［5］Denis Javaux Véronique De Keyser，editors.Proceedings of the 3^rd Workshop on Human Error，Safety，and System Development（HESSD'99），University of Liege，Belgium，June 1999.

［6］Denis Javaux.The cognitive complexity of pilot mode interaction：A possible explanation of Sarter ＆Woods classical results.In Proceedings of the International Conference on Human-Computer Interaction in Aeronautics（HCI-Aero'98），Montréal，Canada，May 1

［7］Denis Javaux.A method for predicting errors when interacting with finite state machines.In Javaux and De Keyser［5］.

［8］Denis Javaux，Estelle Olivier.Assessing and understanding pilots'knowledge of mode transitions on the A340-200/300.In Proceedings of the International Conference on Human-Computer Interaction in Aeronautics（HCI-Aero'00），Toulouse，France，September 2000.

［9］Richard Jensen，Lori Rakovan，editors.Proceedings of the Eighth International Symposium on Aviation Psychology，Columbus，OH，April 1995.

［10］Nancy Leveson and Everett Palmer.Designing automation to reduce operator errors.In Proceedings of the IEEE Systems，Man，and Cybernetics Conference，October 1997.

［11］Nancy Leveson，L.Denise Pinnel，Sean David Sandys，Shuichi Koga，Jon Damon Rees.Analyzing software specifications for mode confusion potential.In C.W.Johnson，editor，Proceedings of a Workshop on Human Error and System Development，pages 132-146，Glasgow，Scotland，March 1997.

［12］Everett Palmer.“Oops，it didn't arm.”-A case study of two automation surprises.In Jensen and Rakovan［9］，pages 227-232.

［13］Peter Polson，Sharon Irving，J.E.Irving.Applications of formal models of human computer interaction to training and use of the control and display unit.Final report，System Technology Division，ARD 200，Federal Aviation Administration，Dept.of Transportation，1994.

［14］Requirements and Technical Concepts for Aviation，Washington，D.C.DO-178B：Software Considerations in Airborne Systems and Equipment Certification，December 1992.This document is known as EUROCAE ED-12Bin Europe.

［15］John Rushby.Using model checking to help discover mode confusions and other automation surprises.In Javaux and De Keyser［5］.

［16］John Rushby，Judith Crow，Everett Palmer.An automated method to detect potential mode confusions.In Proceedings of 18^th AIAA/IEEE Digital Avionics Systems Conference，St Louis，MO，October 1999.

［17］Nadine Sarter，David Woods.Pilot interaction with cockpit automation I：Operational experiences with the flight management system.International Journal of Aviation Psychology，2（4）：303-321，1992.

［18］Nadine Sarter，David Woods.Pilot interaction with cockpit automation II：An experimental study of pilots'mental model and awareness of the flight management and guidance system.International Journal of Aviation Psychology，4（1）：1-28，1994.

［19］Nadine Sarter，David Woods.“Strong，Silent，and‘Out-of-the-loop'”：Properties of advanced（cockpit）automation and their impact on human-automation interaction.Technical Report CSEL 95-TR-01，Cognitive Systems Laboratory，The Ohio State University，Columbus，OH，February 1995.

［20］Lance Sherry，Peter Polson，Michael Feary，Everett Palmer.Analysis of the behavior of a modern autopilot.Technical Report C69-5370-009，Honeywell Incorporated，Minneapolis，MN，1997.

［21］Lance Sherry，Peter Polson.Shared models of flight management systems vertical guidance.International Journal of Aviation Psychology，9（2）：139-153，1999.

［22］Sanjay Vakil，R.John Hansman，Alan Midkiff，Thomas Vanek.Feedback mechanisms to improve mode awareness in advanced autoflight systems.In Jensen and Rakovan［9］，pages 243-248.

［23］Sanjay Vakil，R.John Hansman.Approaches to mitigating complexity-driven issues in commercial autoflight systems.In Javaux and De Keyser［5］.