Verification of autonomous systems for space applications
Verification of autonomous systems for space applications
复制标题
空间应用自主系统的验证
DOI：
10.1109/aero.2006.1656029
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
A. Jonsson
中科院分区：
文献类型：
--
作者：
G. Brat;E. Denney;D. Giannakopoulou;J. Frank;A. Jonsson
自主软件，尤其是基于模型的自主软件，能够在未来的太空应用中发挥重要作用。例如，它可以帮助简化地面操作，或者协助进行自主交会对接操作，甚至有助于从问题中恢复（例如，可以使用规划器来探索电力子系统恢复行动的空间，并在无需（或极少需要）人工干预的情况下实施解决方案）。一般来说，基于模型的系统的探索能力使其具有极大的灵活性。不幸的是，这也使得它们在执行和验证方面对我们人类来说是不可预测的。传统的验证技术对这些系统是不够的，因为它们主要基于测试，这意味着对其行为空间的探索非常有限。在我们的工作中，我们探索如何使用先进的验证与确认（V&V）技术，如静态分析、模型检查和组合验证，来获得对基于模型的系统的信任。我们还描述了如何在系统重构以及验证的背景下使用综合方法。
Autonomous software, especially if it is based on model, can play an important role in future space applications. For example, it can help streamline ground operations, or, assist in autonomous rendezvous and docking operations, or even, help recover from problems (e.g., planners can be used to explore the space of recovery actions for a power subsystem and implement a solution without (or with minimal) human intervention). In general, the exploration capabilities of model-based systems give them great flexibility. Unfortunately, it also makes them unpredictable to our human eyes, both in terms of their execution and their verification. The traditional verification techniques are inadequate for these systems since they are mostly based on testing, which implies a very limited exploration of their behavioral space. In our work, we explore how advanced V&V techniques, such as static analysis, model checking, and compositional verification, can be used to gain trust in model-based systems. We also describe how synthesis can be used in the context of system reconfiguration and in the context of verification