Correctness properties are critical to conducting verification and validation on software systems, especially those cyberphysical systems whose functionality changes frequently due to software updates, changes in the operating environment, or newly learned behaviors. We detail a novel method to automatically construct expressive, executable correctness properties in the form of machine-learned correctness properties which can be used to ensure that a system's behavior is correct with respect to its design and operating requirements. We propose a method to bootstrap the creation of these correctness properties using a novel simulation-based generation of training and testing data using multiple extensions to the Cross Entropy algorithm for search-based optimization. Then, we apply this method to a software-in-the-loop evaluation of an autonomous vehicle to demonstrate that such models can assert about important properties of multi-agent cyberphysical systems. We demonstrate that this process brings the task of developing robust correctness properties from the realm of formal methods experts into the domain of system developers and engineers, and that machine-learned correctness properties are expressive enough to capture the correct behavior of cyberphysical systems in their complex environments. This advancement can provide evidence of dependability to system designers and users, enhancing trust in the deployment of autonomous vehicles and other intelligent transportation systems.

翻译：正确性属性对于软件系统的验证与确认至关重要，尤其是那些因软件更新、运行环境变化或新学习行为而频繁改变功能的网络物理系统。我们详细阐述了一种新颖方法，通过机器学习正确性属性自动构建具有表达力且可执行的正确性属性，从而确保系统行为符合其设计与运行要求。我们提出了一种引导创建这些正确性属性的方法，该方法基于新颖的仿真数据生成训练与测试数据，并采用交叉熵算法的多种扩展进行搜索优化。随后，我们将该方法应用于自动驾驶车辆的软件在环评估，以证明此类模型能够断言多智能体网络物理系统的重要属性。我们证明，这一过程将开发鲁棒正确性属性的任务从形式化方法专家的领域转移至系统开发者和工程师的范畴，且机器学习得到的正确性属性具有足够的表现力，能够捕捉网络物理系统在其复杂环境中的正确行为。这一进展可为系统设计者与用户提供可靠性证据，增强对自动驾驶车辆及其他智能交通系统部署的信任。