Verifying Real-Time Software Is Not Reasonable (Today) - Abstract of Invited Talk
Verifying Real-Time Software Is Not Reasonable (Today) - Abstract of Invited Talk
复制标题
验证实时软件不合理（今天） - 特邀演讲摘要
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Edward A. Lee
中科院分区：
文献类型：
--
作者：
Edward A. Lee
验证是为了证明正式系统具有某些属性。验证安全关键型实时控制软件（例如飞机或汽车控制系统）尤为重要。不幸的是，此类系统需要验证的许多属性实际上并不是软件定义的正式系统的一部分。因此验证软件是没有意义的。那么应该验证什么？说“系统”必须经过验证是油腔滑调的，因为“系统”不是正式的系统。它是一束硅和电线。只能验证系统的模型。什么型号？
如果软件的语义扩展到包括时间属性，那么验证实时软件就成为可能。在本次演讲中，我将认为此类扩展是实用且有效的，但它们需要在相当基本的层面上重新思考软件抽象。此外，它们还需要对计算机架构师、编译器设计者和操作系统设计者制定的许多性能优化进行重新设计。我将展示其中一些，这种重新设计产生的设计具有竞争性的性能和可验证的时序。
Verification is about demonstrating that a formal system holds certain properties. It is particularly important to verify safety-critical real-time control software, such as aircraft or automotive control systems. Unfortunately, many of the properties that need to be verified for such systems are not actually part of the formal system defined by the software. It therefore makes no sense to verify the software. So what should be verified? It is glib to say that "the system" must be verified, because "the system" is not a formal system. It is a bundle of silicon and wires. Only a model of the system can be verified. What model?
If the semantics of software is extended to include temporal properties, then verifying real-time software becomes possible. In this talk, I will argue that such extensions are practical and effective, but that they require rethinking software abstractions at a rather fundamental level. Moreover, they require reengineering of many performance optimizations that computer architects, compiler designers, and operating system designers have instituted. I will show for some of these that such reengineering yields designs that have competitive performance and verifiable timing.