Towards Proving Runtime Properties of Data-Driven Systems Using Safety Envelopes
Towards Proving Runtime Properties of Data-Driven Systems Using Safety Envelopes
复制标题
使用安全信封证明数据驱动系统的运行时属性
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Carlos A. Varela
中科院分区：
文献类型：
--
作者：
S. Breese;F. Kopsaftopoulos;Carlos A. Varela
动态数据驱动的应用程序系统[1，2]（DDDAS）允许在广泛的领域中实现前所未有的自我修复和自我诊断行为。这些系统的有用性与其固有的复杂性相抵消，因此容易受到规范或实现错误的影响。此外，DDDAS技术通常应用于正确性至关重要的安全关键领域。形式化方法促进了软件系统正确性证明的发展，它提供了比非穷举单元测试更强的行为保证。虽然单元测试可以验证系统在某些有限数量的配置中正确运行，但形式化方法使我们能够在配置空间的无限子集中证明正确性，这在涉及连续力学的网络物理系统中经常需要。虽然正式的方法的功效传统上是抵消显着更大的开发成本，我们提出了新的开发技术，可以减轻这种担忧。在本文中，我们探索新的技术，以确保基于认证编程和软件验证的数据驱动系统的正确性。特别是，我们专注于使用交互式定理证明系统来证明数据驱动系统的基本属性，可能依赖于基于物理的假设和模型。我们介绍了正式的安全包线的概念，类似于飞机的性能包线的概念，它组织系统属性的方式，使它清楚地表明哪些属性在哪些假设下。除了在证明开发中保持模块化之外，该技术还使得运行时监视器的派生能够检测潜在的不安全系统状态更改，从而允许用户精确地知道哪些属性已经被验证为适用于当前系统状态。使用这种方法，我们演示了部分验证的原型数据驱动系统的航空电子设备，其中机翼传感器数据被用来确定是否有可能是一架飞机在失速状态。
Dynamic data-driven application systems [1, 2] (DDDAS) allow for unprecedented self-healing and self-diagnostic behavior across a broad swathe of domains. The usefulness of these systems is offset against their inherent complexity, and therefore fragility to specification or implementation error. Further, DDDAS techniques are often applied in safety-critical domains, where correctness is paramount. Formal methods facilitate the development of correctness proofs about software systems, which provide stronger behavioral guarantees than non-exhaustive unit tests. While unit testing can validate that a system behaves correctly in some finite number of configurations, formal methods enable us to prove correctness in an infinite subset of the configuration space, which is often needed in cyber-physical systems involving continuous mechanics. Although the efficacy of formal methods is traditionally offset by significantly greater development cost, we propose new development techniques that can mitigate this concern. In this paper, we explore novel techniques for assuring the correctness of data-driven systems based on certified programming and software verification. In particular, we focus on the use of interactive theorem-proving systems to prove foundational properties about data-driven systems, possibly reliant upon physics-based assumptions and models. We introduce the concept of the formal safety envelope, analogous to the concept of an aircraft’s performance envelope, which organizes system properties in a way that makes it clear which properties hold under which assumptions. Beyond maintaining modularity in proof development, this technique furthermore enables the derivation of runtime monitors to detect potentially unsafe system state changes, allowing the user to know precisely which properties have been verified to hold for the current system state. Using this method, we demonstrate the partial verification of an archetypal data-driven system from avionics, where wing sensor data is used to determine whether or not an airplane is likely to be in a stall state.
使用 SMT 求解器扩展 Sledgehammer
DOI：
10.1007/s10817-013-9278-5
发表时间：
2013
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Lawrence C. Paulson
通讯作者：
Lawrence C. Paulson