安德烈·普拉特(AndréPlatzer)on Verifying Cyber-Physical Systems

||对话

安德烈·普拉特(AndréPlatzer)肖像安德烈·普拉特(AndréPlatzer)是计算机科学助理教授Carnegie Mellon University。他开发了网络物理系统的逻辑基础,以表征其基本原理,并回答我们如何信任计算机控制物理过程的问题。金宝博官方他获得了硕士学位2004年,来自德国的卡尔斯鲁赫大学(TH)和博士学位。2008年,他从德国奥尔登堡大学获得计算机科学,之后他加入CMU担任助理教授。

Platzer博士因其关于动态系统,网络物理系统,编程语言和定理证明的逻辑的研究而获得了许多奖项金宝博娱乐,包括NSF职业奖和ACM博士学位论文荣誉奖。金宝博官方他还被《流行科学》杂志评为10名杰出的年轻科学家之一,也是IEEE智能Systems杂志观看的AI十个观看者之一。金宝博官方

Highlights来自以下采访的普拉策的想法:

  • Keymaera是用于网络物理系统的正式验证工具。金宝博官方它看到了许多现实世界的应用程序,例如在European Train Control System
  • Keymaera’s capability comes from Platzer’s “differential dynamic logic,” which builds on earlier work in (e.g.)动态逻辑
  • 普拉策(Contra Levitt),普拉特(Platzer)并不相信自动驾驶机器人将需要使用决策理论,尽管它们可能会使用。
  • Platzer与正式验证(“我建立正确的系统?金宝博官方在后者上取得进展的一种方法是开发Rushby所谓的“深层假设跟踪”。


Luke Muehlhauser: One of your projects isKeymaera, a tool for deductive formal verification of hybrid systems, including autonomous control systems for trains, planes, and robots. What counts as a “hybrid system,” in this context? What commercial or government applications do you see as being within KeYmaera’s plausible capabilities reach, but for which KeYmaera isn’t yet being used?


安德烈·普拉特(AndréPlatzer):Keymaera是验证混合系统的工具。金宝博官方混合系统(或更确切金宝博官方地说是混合动力学系统)是离散动力学和连续动态相互作用的系统。换句话说,系统的一部分表现出一种离散的行为,通常是由计算金宝博官方或通信引起的,并且系统的其他部分表现出连续的行为,例如空间中的身体运动或连续的化学反应。金宝博官方经典工程中的系统主要具有连续的动力学,而计算机科学则通常探索离散的动态,因为毕竟,计算机计算了一件事,因此固有地离散了。交流是一种类似的离散现象,其中在某个时间点交换了一次信息,然后再在其他时间点再次交换。例如,在无线通道上,通信并非始终不断发生,只有偶尔会发生。无辜的旁观者可能会出现多么快。

现在,混合系统金宝博官方从意识到令人兴奋的事情一旦您进行离散的动态和连续动态相互作用就会发生。突然之间,您的系统可以使用离散的计算机和高级金宝博官方软件算法的功能来控制和影响连续的物理过程并使它们更安全。

但是我们再也无法孤立地理解系统的离散和连续部分,因为它们相互作用。金宝博官方仅仅担心该软件是否会崩溃,还要担心它是否将正确的控制输入输入到实物系统中,以及这些输入对物理的影响。金宝博官方同样,仅仅理解连续动态也不足以使其效果取决于计算机程序生成的控制输入。

这是混合系统开始和Keymaera进入的地金宝博官方方。混合系统是网络物理系统(CPS)背后的通用核心数学模型,带来了令人兴奋的新能力,即我们如何更好地改变世界。但是,这些功能齐头并进,我们的责任是确保当我们非常需要时,系统不会让我们失望。金宝博官方

正如珍妮特·翼(Jeannette Wing)恰当地说的那样:“我们如何为人们提供可以押注生活的网络物理系统?”金宝博官方

Application areas include aviation, automotive, railway, robotics, medical devices, physical or chemical process control, factory automation, and many more areas than I could list. Hybrid systems are a very general mathematical model which makes them interesting for many possible application areas. KeYmaera has indeed been used with industrial partners from the automotive industry, on mobile robotics applications of an industrial partner, in a study of a surgical robotics system by a government lab, and we are currently working with the Federal Aviation Authority on how to use KeYmaera for the next generation Airborne Collision Avoidance System ACAS X. Having said that, all those application areas bring up interesting challenges. Since most software in the wild still contains bugs, there is more potential and there remain more challenges in all the other application areas as well.


Luke: What role does差分动态逻辑在Keymaera玩?您开发它的灵感是什么?


安德烈:差分动态逻辑是Keymaera背后的理论基础和机制。这是使Keymaera起作用的验证能力的原则。差异动态逻辑是您可以在其中指定和验证混合系统属性的逻辑。金宝博官方逻辑以单个语言集成了混合系统的所有相关特征:用于描述其连续动态的微分方程,差异方程式 /离散动态和条件切换的离散分金宝博官方配,非确定性选择以及重复。有了这些基本的动力学原理,所有其他相关的原理都可以表达。

当我开始博士学位时,我设计了不同的动态逻辑。我一直对混合系统的核心逻辑基础看起来非常好奇,只是迫不及待地想发现它们。金宝博官方尤其是因为它们精美地汇集了数学的离散和连续部分,这些部分在经典上是单独考虑的。

但是后来有人向我展示了一个模型European Train Control System(ETCS) with critical parameters (such as when to start braking) that were chosen more or less at random based on their performance in a few simulations. Suddenly I saw that there was also a real need in practice for the flexibility that differential dynamic logic provides. There simply had to be a better and more disciplined way of approaching the problem of how to design hybrid systems and safely choose their respective parameters. Any specific number for a crucial design parameter can obviously only be safe within a range of constraints on all the other parameters of the system. And, indeed, the chosen parameter value for the start braking point in the ETCS model turned out to cause a collision when just increasing the speed a little.

从这一点开始,我设计了不同的动态逻辑,双重关注其核心理论及其在应用中的实际使用。这种更广泛的重点无疑使它更加成功。尤其是当实际应用提出有趣的理论挑战时,并且相反,由于纯粹的理论原因而考虑的问题后来对毫无戒心的应用至关重要。

差分动态逻辑is what we later used as the basis for implementing the theorem prover KeYmaera and has served us well since. Much has been written about differential dynamic logic since my first draft in 2005, including a。But a good survey can be found in aLICS tutorial


Luke: What previous work in logic and differential equations did you build on to create differential dynamic logic?


安德烈:差异动态逻辑幸运的是,所有科学都可以继续前进。其发展和理论从逻辑,数学和计算机科学领域的所有领域详尽清单要比整个访谈更长。与控制和工程的连接的列表将同样长。实际上,这是混合系统如此令人兴奋的原因之一。金宝博娱乐金宝博官方当然,这是一种能够探索您最喜欢的数学领域的一种方式,同时仍然拥有其他人关心的重要应用程序。

幸运的是,Keymaera为您提供与科学和工程其他领域的所有强大联系,但它们隐藏在差异动态逻辑的非常优雅和直观的语言后面。这意味着用户不需要了解所有数学领域,并且可以使用差异动态逻辑及其证明规则的句法结构进行播放。差异动态逻辑为人们提供了一个安全的框架,在这种框架中,他们可以利用和利用所有这些领域而无需深入了解所有这些领域。然后,计算机可以检查推理是否以正确的方式合并。

我构建的最中心的工作是动态逻辑最初是由于普拉特(Pratt)和许多人的开创性,包括哈雷尔(Harel),迈耶(Meyer),帕里克(Parikh),科尔(Kozh)以及索斯·莱(Sophus Lie)的连续代数和连续群体的理论。这两种发明都来自我出生之前,但在设计差异动态逻辑方面有很大帮助。

动态逻辑是常规离散程序的逻辑,我通过使用微分方程增强它并将其推广到具有相互作用的离散和连续动态的混合系统来杂交。金宝博官方原始的动态逻辑也已实现并成功地用于供奉献者KeY我们的供奉献者Keymaera所基于的。这种遗产还解释了有趣的名字Keymaera,这是独立的,因为Keymaera是一个同谐的人Chimaera,来自古希腊神话中的混合动物。

回想起来,很明显,动态逻辑实际上已经渴望混合系统已经过去了三十年,而没有人注意到。金宝博官方动态逻辑最初是针对非确定系统制定的,在该系统中,程序可以产生不止一种可能的效果。金宝博官方这是一个基本特征,但实际上与常规程序的行为略微略有不同,这主要是确定性的,即每个程序语句都会完全有一个效果。在混合系统中,故事有所不同,因金宝博官方为CPS的实施永远不会像您认为会运行的那样确定性,并且因为环境总是需要考虑您需要考虑的未来行为。Dynamic logic and dynamical systems are simply made for each other

甚至more fundamental than dynamic logic itself are the general fundamental principles of logic. They led me to the realization that hybrid systems deserve a study of their logical characteristics. Hybrid systems used to be second class citizens because they were challenging and no one had created a logical foundation for them. Now that those proper logical foundations are in place, we see that hybrid systems and their programmatic expressions as hybrid programs are not just some peripheral artifact, but are actually a powerful construct in their own right. They possess the intrinsic characteristics of integrating interacting discrete and continuous behavior. The result of such an interaction may be a little bit like what happens when particles of fundamentally different origin collide in a high-energy physics collider experiment. Historically disjoint areas of mathematics & science suddenly being to interact. Really surprising interactions happen and正在建造科学桥梁,以团结离散和连续计算通过混合动力学的中介性质。

Another example illustrating the consequences of the impact of logic on hybrid systems is that proof theory led to a generalization of Lie’s seminal results in ways that relate to Gentzen’s seminal cut elimination in logic. Cuts are the logically fundamental mechanism behind lemmas in proofs and have been shown by Gentzen to be unnecessary. They are rather discrete, though, because cuts prove a (static) lemma and then use it. The counterpart for discrete cuts is called差距which prove a property of a differential equation and then modify the system behavior to comply with this property.差异是基本的而且,就我所知,Sophus Lie似乎并没有意识到这种逻辑机制对于微分方程的重要性。像这样的现象表明,当像Gerhard像Gerhard Extzen这样的逻辑学家与Sophus Lie这样的代数主义者互动时,就会发生惊人的科学。

然而,在一天结束时,出于所有这些思维方式的理论惊喜,肯定也令人放心地观察它们在验证和分析结果中对CPS应用程序的实践效果和相关性,而这是不可能的。每天都有有用的应用程序,将令人兴奋的理论具有令人兴奋的理论。


Luke:您认为动态逻辑的创建者或您构建的其他理论工作的创造者,以开发差异动态逻辑,以为他们的work could be useful for program safety or verification one day? Or is this an instance of you plucking up theoretical results from unrelated disciplines and using them for your own purposes in software verification?


安德烈:嗯,这些都是非常聪明的人。我发现很难想象动态逻辑的开拓者不会想到程序验证的可能用途。即使动态逻辑可能是从更多的理论 /逻辑研究开始的,我敢肯定,他们知道这一未来。而且我也不是第一个使用动态逻辑进行验证的人。但是,确实,与具有差异动态逻辑的情况不同,动态逻辑的理论,实践和应用的发展主要由不同的群体领导。也许这只是混合系统自然吸引力的一部分,我永远无法像我对他们的应用一样对他们的理论充满好奇。金宝博官方

话虽如此,一个很好的问题是,动态逻辑的发明者是否对混合系统有了想法。金宝博官方我当然不知道。动态逻辑早于混合系统的发明近二十年。金宝博官方但是混合系统几乎一直在金宝博官方我们身边。只是直到1990年代,没有人注意到它们本身就是一种迷人的数学现象。

关于灵感的另一个主要来源,Sophus谎言的开创性工作,他可能没有想到在验证混合系统中的可能用途,因为Sophus Lie的结果早于一个世纪的动态逻辑。金宝博官方他发明了现在所谓的Lie Groups 1867-1873,它早在计算机出现之前就发明了。但是,我不想留下印象,这是我开发差异动态逻辑及其理论和应用时唯一的灵感。KurtGödel,Gerhard Gentzen,Alfred Tarski,David Hilbert,Alonzo Church,Yiannis Moschovakis,HenriPoincaré,Joseph Doob,Joseph Doob,Eugene Dynkin,Eugene dynkin和许多其他许多其他人也具有重大影响。我肯定会归功于他们以前发现的结果。


Luke:莱维特(1999)认为,随着智能系统变得越来越自治,并在越来越多的不确定金宝博官方性,未知的环境中运作,就不可能用控制理论等工具完全对其环境和可能的行为进行建模:

如果机器人使用更普遍,他们will need to operate without human intervention, outdoors, on roads and in normal industrial and residential environments where unpredictable… events routinely occur. It will not be practical, or even safe, to halt robotic actions whenever the robot encounters an unexpected event or ambiguous [percept].

目前,商业机器人主要通过控制理论反馈来确定其行为。控制理论算法需要在软件程序中体现的世界可能发生的事情的可能性,这些模型可以使机器人对视觉事件的任何与任务相关的任何事件进行适当的操作响应。当在开放的,不受控制的环境中使用机器人时,将不可能向机器人提供先验models of all the objects and dynamical events that might occur.

In order to decide what actions to take in response to un-modeled, unexpected or ambiguously interpreted events in the world, robots will need to augment their processing beyond controlled feedback response, and engage in decision processes.

因此,他认为,自治计划最终将需要做出决策理论。

您如何看待这个预测?通常,您认为哪些工具和方法与对未来高度自主系统的高度安全保证最相关?金宝博官方


安德烈:莱维特肯定有一点性建议y of stronger safety arguments for robots, especially in light of their challenging and uncertain environments.

但是,我不建议完全驳斥控制理论。我什至没有看到决策理论如何与控制理论相矛盾。毫无疑问,控制理论是在包括机器人在内的网络物理系统上贡献有价值的技术和观点。金宝博官方网络物理系统的精神及其混合系统的数学模型是从中学习金宝博官方全部涉及的各种学科并将概念汇集在一起​​,而不是将它们隔离。

尽管我同情莱维特对可能使用决策理论方法的结论,但我不同意他的论点。我这样做的原因是对网络物理系统背后的重要原理的一个很好的例证。金宝博官方莱维特(Levitt)在您引用的文字和其他地方引用的其他地方说,控制理论无济于事,因为它需要模型。他进一步认为,解决方案是使用决策理论,但是,该理论仍然需要模型:

“For each step in a plan to accomplish a robot task, […] we can model the robot’s immediate possible action choices as decisions. Then we can develop先验机器人动作可能与任务相关的结果的值集。”

实际上,这需要更多的模型:先前的信念分布模型,模型感知如何更新信念,在州采取行动的成本模型。

认为使用模型的方法是使用更多的模型,即使此参数经常发生,也没有定论。同时,很难在不采用世界模型的情况下逃脱笛卡尔恶魔。只要我们承认我们的预测受到某种形式的模型的约束,无论使用模型,它们可能没有任何隐藏或数据驱动的模型。实际上,甚至有一个充分的理由考虑越来越灵活的模型。

无论如何,我同意Levitt的观点,即机器人生活在不确定的环境中,因此不确定性需要包括在模型中。简单的模型足以理解系统中的某些现象,而其他方面需要更复杂的模型。金宝博官方但是他们仍然是模特!正确的模型是确定性的,概率的,非确定性的还是对抗性的,取决于确切的目的。在某些情况下,对不确定性的非确定性理解要好得多,在其他情况下,在其他情况下,它们必须是概率的,而在其他情况下则必须是概率。

This is one of the central guiding principles behind多动力系统金宝博官方,我将其定义为结合多个动态方面的系统,例金宝博官方如离散,连续,随机,非确定性或对抗性动力学。多动力系统将混合系统推广,并提供金宝博官方了混合系统缺失的网络物理系统的动力学特征。差异动态逻辑非常优雅地概括多动力系统的动态逻辑金宝博官方

这种灵活性对于高保证安全系统的成功至关重要。金宝博官方如果所有模型,分析结果和技术都需要一旦发生动态方面就可以完全丢弃,那么这只是一个可惜的事情。相反,模型和分析技术与差异动态逻辑家族,那么与引入或删除非确定性或其他动态方面相关的成本没有压倒性的成本。

我的同事布鲁斯·克罗格(Bruce Krogh),戴维·加兰(David Garlan)和我们的学生也主张了这种模特的灵活性,在这种情况下,洞察力是考虑到通常更可行多个异质模型而不是一个全弹药。

Levitt表达的另一个常见但错误的论点是

“实际上,我们声称,如果机器人的看法可以肯定,我们几乎没有与机器人行为相关的不确定性。”

“如果我们能感觉到,我们可以采取行动”的论点是一个普遍的谬论。它的隔离是非常真实的:如果我们看不到,几乎不可能安全地控制任何东西。但是,即使传感器恰好工作得很好,控制器中仍然有许多微妙和公然的错误机会。而且,从莱维特很容易被驳斥的行动影响的不确定性带来了更多的错误。为了强调,我只专注于讨论独立于感应和驱动不确定性的控制器错误。

例如,我们的验证工具KeYmaera丫nni Kouskoulas, one of my collaborators at the John’s Hopkins University’s Applied Physics Lab (JHU APL), to find and fix two very subtle flaws in the controllers of a surgical robotics system for skull-base surgery. These controllers had been developed according to the best practice state of the art in safety-critical systems and had been scrutinized by their developers. Yet, the developers had second thoughts and approached the JHU APL, who ultimately approached us. The fact that the bugs have only been found by formal verification in the end demonstrates that it is just extraordinarily difficult to get cyber-physical systems correct without the right analytic tools. But I am not surprised that it took sound verification tools to find the bugs. One was a timing bug caused by the inertia of the system. The other one had to do with very subtle acting and counteracting control depending on the precise geometrical relationships.

这不是孤立的情况。我们已经观察到在DARPA HACMS项目中使用验证的类似好处。观察在将机器人的正式验证部分与未验证的部分进行比较时可能出现的差异是一次有趣的经历。这始终是一种令人大开眼界的体验,所有参与者都学到了有关应用领域的重要内容。

莱维特低估了重大挑战:

“总而言之,我们声称对世界状态的评估在两种感觉上都是可以在计算上进行的。首先是我们可以指定有关世界状态的价值观先验并使用它们在任务执行期间动态重视操作。第二个估值的数量是在相对较少的涉及机器人任务(例如道路,交通信号,人类和动物)的世界实体的抽象类别中的秩序线性。”

但是,决策的复杂性在实践中是一个问题。甚至看似简单的计划实例是NP-HARD, which Bellman identified as the curse of dimensionality in the 1950s. Correct decisions that come half an hour too late are not particularly useful for rescuing a robot’s safety mission. Real-time responses are critical. That’s one of the reasons why it is crucial to have pre-verified safe responses as opposed to settling on unbounded online deliberation.

与上面的报价指示的相反,几十年来,找出如何使模型正确,正确获取值并确保两者都转化为正确选择的操作,这是几十年来一直是一个开放的挑战。

考虑ACAS X,这是FAA的下一代空降碰撞系统,该系统负责我们在JHU APL的合作者,并使用我们的验证技术进行分析。金宝博官方它的设计以马尔可夫决策过程优化的形式建立在决策理论上。在某种程度上,确定“没有碰撞”是设计飞机避免碰撞系统的最高价值,这听起来很琐碎。金宝博官方但是,这如何准确地转化为数学?什么是正确的次要目标,可以防止不必要的避免演习?入侵飞机的合适型号是什么?为了飞行员的回答?经过多年的ACA X仔细设计和高技能的设计,我仍然看到了一个“最佳”临时版本,这不是任何人想要的。幸运的是,那不会飞。

总体而言,我认为验证最终将网络物理系统的正确性降低到我们是否正确的模型的问题。金宝博官方确定问题的正确模型是一个真正的挑战。但是一旦我们做到了,仍然有许多微妙的方法可以使答案错误。这些是验证消除的缺陷。话虽如此,验证也在验证我们是否首先获得正确的模型方面取得了进展。

根据记录,我也强烈不同意莱维特在该职位论文中提出的其他主张。尤其:

“我们声称,使机器人成为可能的道德行为的核心能力是通过对感觉数据的自动解释来理解机器人外部的世界。机器人的看法与关于世界的真理或虚假的陈述与句法规则或类似的陈述具有根本不同的关系。”

这一说法直接与阿隆佐教堂(Alonzo Church)的开创性证据相矛盾。我对网络物理系统的逻辑和证据的主要研究线,准确地表明了如何建立并成功利用这种关系进行验证。金宝博娱乐金宝博官方因此,我理解莱维特的主张是可能的建议,而不是结论性的论点。但是,这可能是逻辑学家的特征,以通过是否带有证据来区分定理与猜想。


Luke: You wrote that “verification is also making progress on validating whether we got the right model in the first place.” What did you have in mind, there? The thing that came to mind for me wasRushby (2013),但我对减少问题(他所说的)“认知怀疑”的具体进展并不了解。


安德烈: John Rushby makes a great case for distinguishing logic doubt (“did we get the arguments right?”) versus epistemic doubt (“did we get our knowledge of the world right?”). I agree with him that we can get logic doubt under control and make it a problem of the past. Yet, that is exactly what you need such strong sound reasoning frameworks for cyber-physical systems for, such as differential dynamic logic. The ultimate proof will simply have to take the dynamics of the system into account just as much as it takes its control into account.

Terminologically, I usually contrast formal verification (“did I build the system right?”) with formal validation (“did I build the right system?”). That is primarily because verification versus validation has a widespread (but not unambiguous) compatible connotation in the field. And also because I want to emphasize that we should not settle only for arguments that Rushby aptly phrases as:

“Because an expert says so.”

Yet, it doesn’t matter what name we use, it’s still our responsibility to make sure the system really works in the end.

我们的NSF Expedition项目CMAC(复杂系统的计算建模和分析),由我的同事Ed Clarke等人领导,我们还使用正式验证的元素使用,我们还通过对它们进行正式验证测试是否进行正式验证测试,以探测合理性的模型金宝博官方他们满足了预期属性。这些不仅是最终的安全性特性,而且是平凡的特性,其唯一目的是验证模型是否按预期行为。当然,这是一种在芯片设计中也成功的技术。

为了跟进Rushby的建议,我完全同意他对我所说的深层假设跟踪的恳求。也就是说,确保所有的假设和结论都经过精心跟踪。再次使用多个异质模型进行验证的重要主题。如果某人的假设是错误的,则是未成年人和大打ic的普遍原因。或者,如果没有人知道他们,那么其他人就得出了错误的结论。这也是为什么隐含的模型假设不足的原因往往会对系统的行为产生最可怕的后果。金宝博官方

例如,在我们关于自动驾驶机器人地面车辆的可靠障碍物避免障碍的工作中,我们的模型随后通过在有传感器和执行器和位置不确定的情况下,从静态到动态一直到动态障碍的障碍物的动态能力进行。由于我们在Keymaera中陪同每个模型都有正确的证明,因此我们不禁注意到在哪种情况下,系统是安全的,何时何时安全。金宝博官方例如,在我们的模型中,从“障碍被卡住”到“障碍可以在任何想要的地方移动,无确定性”是一个简单的变化。但是,由于证明是不起作用的,因此您立即意识到您首先需要了解障碍速度的一些束缚。与光速相比,动态障碍物更快,很难防御。

后来,在未经验证的不同控制器实现的干燥过程中,有趣的是看到动作的差异。未经验证的机器人控制器有时会与障碍物相撞,这正是它不应该做的。验证系统的相应(仿真)运行在碰撞发生之前很久就否决了不安全的控制动作。金宝博官方原因是原型的。谁设计了我们可以访问的未验证控制器的人做自然的事情:机器人首先考虑了所有障碍,并希望能够快速传感。好吧,这就是我们第一个经过验证的模型也假设的。但是我们的Keymaera证明立即进行了进一步的进一步研究,并调查了动态障碍的案例,这就是为什么我们建议考虑未验证控制器的动态障碍的原因。

未经验证的机器人仍然相撞。这次,原因更加微妙。简而言之,实施方式默默地假设墙壁不会在其他代理商的情况下移动。每天的经验听起来很合理。捕获是角落确实移动。好吧,他们不是真的。But as soon as your verification model says that obstacles either move or they don’t and that it’s their choice (nondeterministically!) where they move to, then you cannot help but notice in your proof that the system is only safe if your controller correctly addresses the case where an obstacle suddenly comes racing round a corner. And indeed, when we asked, we got the confirmation that troublemaker cases in practice were partially occluded obstacles.

现在,可能很容易责怪原始机器人控制器的开发人员,并说他们只是没有给予足够的关注。但这太容易了。实际上,这将完全错过这一点。关键是机器人技术和任何其他类型的网络物理系统设计都充满挑战。金宝博官方这些是非常困难的问题。编程非常困难。而且编程机器人只会使事情变得更加困难,因为我们突然必须面对周围的整个物理现实。与使他们正确正确的方法相比,还有更多的方法可以使他们弄错。我们迫切需要有助于我们正确设计设计的分析支持,以便我们可以将生活押在它们上。

后来与许多学术界和行业的许多人进行了交谈,他们中的大多数人都不明显,即使他们自己没有,也必须将环境空间的某些静态部分视为移动。这是一个错误,验证使我们无法做到。

但是猜猜我们是如何发现的。一个月前,我小组的PostDocs在一些例子上尝试了我们刚经过验证的控制器,并感到非常沮丧,因为它的口味太保守了。它回开狭窄的门口。我本人可能很困惑。但是后来我们意识到我们经过验证的控制器是正确的。如果障碍物可以移动到任何地方,它们也可能会从我们机器人无法看到的角落后面迅速移动。请注意,我们从未将这些知识纳入我们的模型,控制器或其他任何内容。我们只是从具有移动障碍物的飞机上的机器人运动的规范模型开始。然后,我们发现了我们的证明导致我们设计一个可验证的安全控制器的地方。他们带领我们进入了一个远离狭窄门口的控制器。 But that is what the robot simply has to do to stay provably collision-free.

We later discussed our verified controller with our collaborators in industry. They not only confirmed that our controller works within the intended operational range and wasn’t overly conservative at all. But they also simply loved the sudden new capability of playing with different instantiations of the parameters of our verified model to find out whether the design will work correctly efficiently within their intended operating regime. Without having to set up all those different scenarios and system configurations experimentally. And the verified controller automagically ends up doing the right thing. When cutting corners, it will slow down to avoid collisions. When moving with a bigger margin around a corner, it would happily speed up. We didn’t build that in. It just followed from the safety constraints of our proofs.

尽管如此,我们可能还是在世界运动原则的模型和对环境的假设中犯了错误。这会给我们一个真实,不可否认的证据,这只是不适用于现实,因为它的假设没有得到满足。或者我们可能已经误导了我们关心的安全性。这就是正式验证的出现。确保模型适合现实的相关部分以及配方符合意图的技术。我们刚刚取得了一些有希望的进展,我敢肯定,仍然会发现更多令人兴奋的事情。

Formal validation is just as exciting as formal verification. And that is why I am developing the Logical Foundations of Cyber-Physical Systems, because we simply need such strong analytic foundations when software reaches out into our physical world. Yet, with those foundations, there are suddenly amazing opportunities for how we can change the world for the better by designing cyber-physical systems that help us in our daily lives in more ways than we ever dreamed off. After all, true cyber-physical systems combine cyber capabilities with physical capabilities to solve problems that neither part could solve alone.


Luke:谢谢,安德烈!