结合遗传编程和模型检验生成环境假设
Combining Genetic Programming and Model Checking to Generate Environment Assumptions
摘要：
当环境假设未被考虑时，软件验证可能产生虚假故障。环境假设是系统或组件对其操作环境的预期，通常根据该系统或组件的输入条件进行指定。在这篇文章中，我们提出了一种方法来自动推断网络物理系统（CPS）的环境假设。我们的方法以三种不同的方式改进了最先进的技术：首先，我们学习涉及信号和数值变量的复杂CPS模型的假设;第二，学习的假设包括定义在多个变量上的算术表达式;第三，我们确定了环境假设的可靠性和信息量之间的权衡，并证明了我们的方法在优先考虑这些标准时的灵活性。我们评估我们的方法使用公共领域基准的CPS模型从洛克希德·马丁公司和卫星控制系统的一个组成部分，卫星系统供应商LuxSpace。结果表明，我们的方法优于国家的最先进的技术学习假设的CPS模型，而且，当应用到我们的工业CPS模型，我们的方法是能够学习的假设是足够接近的假设人工开发的工程师是有实用价值的。
英文摘要：
Software verification may yield spurious failures when environment assumptions are not accounted for. Environment assumptions are the expectations that a system or a component makes about its operational environment and are often specified in terms of conditions over the inputs of that system or component. In this article, we propose an approach to automatically infer environment assumptions for Cyber-Physical Systems (CPS). Our approach improves the state-of-the-art in three different ways: First, we learn assumptions for complex CPS models involving signal and numeric variables; second, the learned assumptions include arithmetic expressions defined over multiple variables; third, we identify the trade-off between soundness and informativeness of environment assumptions and demonstrate the flexibility of our approach in prioritizing either of these criteria. We evaluate our approach using a public domain benchmark of CPS models from Lockheed Martin and a component of a satellite control system from LuxSpace, a satellite system provider. The results show that our approach outperforms state-of-the-art techniques on learning assumptions for CPS models, and further, when applied to our industrial CPS model, our approach is able to learn assumptions that are sufficiently close to the assumptions manually developed by engineers to be of practical value.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
