基于开发工件的保守混合自动机
Conservative Hybrid Automata from Development Artifacts
摘要：
验证在安全关键环境中运行的网络物理系统需要正式的系统模型。验证的有效性取决于模型的精度：模型中未捕获的可能行为可能导致正式验证，但不安全的系统。然而，手动构造是微妙的，容易出错，而自动构造不能扩展到大型复杂的系统。作为一种补救措施，本文设计了一种自动构建算法，利用包含在文物的开发过程中的信息：运行时监控规范和记录的测试痕迹。这些工件不会产生额外的成本，并提供足够的信息，以便构建过程可以很好地扩展到大型系统。该算法使用自上而下和自下而上的结构之间的混合方法，该方法允许证明结果保守，同时限制过度近似的水平。
英文摘要：
The verification of cyber-physical systems operating in a safety-critical environment requires formal system models. The validity of the verification hinges on the precision of the model: possible behavior not captured in the model can result in formally verified, but unsafe systems. Yet, manual construction is delicate and error-prone while automatic construction does not scale for large and complex systems. As a remedy, this paper devises an automatic construction algorithm that utilizes information contained in artifacts of the development process: a runtime monitoring specification and recorded test traces. These artifacts incur no additional cost and provide sufficient information so that the construction process scales well for large systems. The algorithm uses a hybrid approach between a top-down and a bottom-up construction which allows for proving the result conservative, while limiting the level of over-approximation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
