约翰·舒曼博士是一个成员健壮软件工程组RSE在NASA艾姆斯．他于2000年获得了哈佛大学的康复学位TechnischeUniversitätMünchen自动化定理证明在软件工程中的应用。他的博士论文(1991)是关于高性能并行定理的证明。Schumann博士从事软件和系统健康管理的研究，先进金宝博娱乐的空中交通管制算法和自适应系统的验证和验金宝博官方证，空中交通管制系统和无人机事件数据的统计数据分析，数据分析和状态估计的可靠代码生成。Schumann博士的一般研究兴趣集中在正式和金宝博娱乐统计方法的应用，以改进先进的安全和安全关键软件的设计和可靠性。
他受雇于SGT公司。作为首席科学家的计算科学。
路加福音Muehlhauser： 在Denney等人(2006)，你和你的共同作者有助于解释：
软件认证旨在表明，有问题的软件实现了一定的质量，安全或安全性。其结果是证书，即，独立认为所申请物业的证据。认证方法很广泛......但是通过基于正式方法的方法实现了最高程度的信心，并使用证明证书的逻辑和定理来实现。
我们已经开发了一种认证方法……[证明]航空航天软件的安全性，该软件是由高级规格自动生成的。我们的核心思想是扩展代码生成器，使其能够同时生成代码和详细的注释……从而实现完全自动化的安全证明。验证条件生成器(VCG)处理注释代码并产生一组安全义务，当且仅当代码是安全的时，这些义务是可证明的。然后，一个自动定理证明程序(ATP)履行了这些义务，证明程序可以由一个独立的证明检查程序来验证，作为证书。
(我们的)建筑区别于受信任的和不信任组件...可信组件必须是正确的，因为它们的结果中的任何错误都可能会损害系统给出的保证;金宝博官方不受信任的组件不会影响声音，因为它们的结果可以通过可信组件检查。
你还可以使用这个有用的例子:
在您的认证系统架构中，为什么问题规范和综合系统不受信任?金宝博官方
约翰·舒曼：理想情况下，此数字中的整个架构只能包含可信组件。然后，可以确保在验证过程中发生任何不好的情况。遗憾的是，像程序合成系统或整个自动定理先词一样的金宝博官方软件系统不能用当前技术正式验证。他们的代码是成千上万的代码行。因此，我们使用诀窍复杂性不对称：例如，找到大量的大量因素的软件是复杂的;它的验证是复杂和耗时的。另一方面，检查每个效果是微不足道的：一个只要乘以因素。这样的检查器易于实现并验证。因此，如果我们现在使用未经验证的Prime-Finder，并且对于每个结果，我们可以确定我们的Prime系列Finder是否正常工作。重要的是：有人需要为每个结果运行检查器，但由于检查程序快速，它无关紧要。 Similar situation here: synthesis system and prover are大和复杂的，但证明检查器不是。VCG具有中等复杂度和可验证性。整个系统的实际瓶颈是你必须相信你的安全策略和领域理论。金宝博官方两者都可以是更大的逻辑公式集。根据我的经验:如果一个公式超过5行，那么它很可能包含一个错误。不幸的是，没有简单的方法来解决这个问题。
卢基:凭直觉，您认为通过正式方法开发的系统(如您自己的过程)与通过普通工程方法和广泛测试开发的系统金宝博官方相比，“安全”程度有多高?据你所知，对这种假设有任何实证检验吗?
约翰：直观地，我认为使用正式方法（FM）软件开发和V＆V可以大大提高安全性。但是，有许多问题/考虑因素：
- 使用FMs来验证某些被充分理解的安全属性不会被违反(例如，没有缓冲区溢出、没有被零除、没有未初始化的变量)是非常有益的(参见最近的安全问题——其中很多问题都与此类安全属性有关)。一些用于这项任务的技术(例如，静态分析)已经在这方面取得了很大的成就。
- 即使假设有这些工具，人们也会问:我能详细说明吗全部必要的安全属性？是软件的规范，我对此进行了基于FMS的验证，正确和一致吗？正确的，一致和完整的规范非常难以写入 - 因此对于任何合理复杂性的软件，我将假设在代码中有规范中至少存在许多错误。
- 在我看来，FMS应与传统方法（包括测试）一起使用，以及动态监控。作为示例，No缓冲溢出的正式证明应该能够减少（但不消除）广泛的测试。由于测试只能是有限的，动态监控（AKA运行时验证（RV）或软件健康管理（SWHM））应该用于对未见的软件行为（例如，由意外环境中的休眠错误或操作引起的）作出反应。RV和SWHM本身主要是基于正式的方法。
我不知道任何这样的经验测试 - 他们很难以无偏见的方式进行。致力于成本和可靠性建模（例如，B. Boehm）可能会提供一些洞察力，但我需要看看。
卢基：您认为正式验证方法最终能够处理更复杂的安全性能，例如对火车，飞机和汽车以及Asimovian属性的碰撞（洛杉矶焊接& Etzioni）对于与人类金宝博官方互动的系统？
约翰已经有几个例子，其中形式化方法已经成功地用于规范和/或复杂系统的开发。金宝博官方例如,B方法(一种与Z方法相关的工具支持方法)已被用于巴黎地铁(14号线)的列车自动控制。空客正在使用抽象解释(Cousot)等形式化方法来开发关键安全性的飞机软件。
TCAS系统（交通金宝博官方碰撞避免系统）是商用飞机的国际系统，警告飞行员从迫在眉睫的中间碰撞（距离距离不到一分钟）。已经详细研究了这种复杂的系金宝博官方统（飞机需要使用精心通信协议来解决冲突），并存在正式的规格/分析（例如，Leveson，Heimdahl和其他）。
在我看来，正式方法足以用于指定/验证复杂系统。金宝博官方然而，Ueberlingen事故表明，该系统并非防止安全。金宝博官方这里的“系统金宝博官方”是指：实际硬件/软件，飞行员（从TCAS系统和ATC获得冲突的消息），航空公司（据说有人告诉飞行员忽略警告并飞行最有利可图的路线）和瑞士空气交通管制，没有完全员工。
在我看来，在混合控制系统中(人类操作员拥有全部或部分控制)，对人类行为的准确建模和预测仍然是一个未解决的大问题。金宝博官方
全自动系统（例如，UAS）可能会安全金宝博官方地处理这种情况，但总的来说有几个主要问题：
- 验收问题(我们会登上无人机吗，我们会放弃车轮吗?)据推测，当BART第一次引入无人驾驶列车时，他们不被通勤者接受，他们不得不让司机回到火车上。
- 如何安全地在“混合模式”环境中进行操作？例如，有些汽车是自动的，一些汽车手动驱动，或者商人飞机与一般航空和UAS系统。金宝博官方人类运营商可能会以意想不到的方式制作（愚蠢）错误或反应。自动化系统可能意外地反应，例金宝博官方如，由于软件错误。
- 如何处理系统安全?金宝博官方许多提高安金宝博官方全性的系统目前很容易受到恶意攻击:例如ADS-B系统，它应该使用一种未加密的协议取代部分老化的ATC系统;无人机可以被欺骗(见中情局无人机被伊朗捕获);现代汽车很容易被黑进去。
虽然在复杂系统的严格的追踪和规范中发生了很多事情，但在我们甚至接近谈论机器人规律时需要解决许多问题。金宝博官方
操作员错误后如何安全地恢复复杂系统？金宝博官方假设具有驾驶辅助系统的汽车中的驾驶员（例如，自适应巡航控制，检测不安全车道变化）。金宝博官方自动系统如何对即将发生的问题作出反应，而不会导金宝博官方致驾驶员吓坏并犯更多的错误？
当系统硬件或软件出现问题时，如何安全地金宝博官方恢复系统?当澳航A380的引擎爆炸时，飞行员收到了大约400条诊断和错误信息，他们必须处理这些信息(幸运的是他们有时间)。其中一些信息相互矛盾，或者执行起来是危险的。
这表明以复杂系统的简洁和正确的状态信息呈现操作员仍然是一个大问题。金宝博官方
飞行员降落A380后，他们无法打开引擎。机器智能的第一个迹象是"别杀我" ?
卢克：谢谢，约翰！
你喜欢这篇文章吗？你可以享受我们的其他对话帖子，包括：
