论文标题
使用CSP对安全要求的离线运行时验证
Offline Runtime Verification of Safety Requirements using CSP
论文作者
论文摘要
动态形式验证是提供持续信心的关键工具，即系统在使用中符合其要求，尤其是在使用系统之前与静态正式验证配对时。本文介绍了工作流程和运行时验证（RV）工具链，Varanus及其在工业案例研究中的应用。使用工作流程我们从自然语言安全要求文档中手动得出通信顺序过程（CSP）模型，Varanus用作监视器Oracle。模型的重复使用意味着监视器的Oracle不必单独开发，冒着静态验证的模型之间的矛盾危险。该方法由teleterated操纵系统的离线RV（称为Mascot）证明，该系统可在联合欧洲圆环（JET）融合反应堆内进行远程操作。我们描述了我们的吉祥物安全设计文档的模型（包括建模过程如何在设计中揭示了指定的指定）并评估Varanus工具链的实用程序。工作流和工具提供了安全文档的验证，从文档到系统的安全性能的可追溯性以及RV的经过验证的Oracle。
Dynamic formal verification is a key tool for providing ongoing confidence that a system is meeting its requirements while in use, especially when paired with static formal verification before the system is in use. This paper presents a workflow and Runtime Verification (RV) toolchain, Varanus, and their application to an industrial case study. Using the workflow we manually derive a Communicating Sequential Processes (CSP) model from natural-language safety requirements documents, which Varanus uses as the monitor oracle. This reuse of the model means that the monitor oracle does not have to be developed separately, risking inconsistencies between it and the model for static verification. The approach is demonstrated by the offline RV of a teleoperated manipulation system, called MASCOT, which enables remote operations inside the Joint European Torus (JET) fusion reactor. We describe our model of the MASCOT safety design documents (including how the modelling process revealed an underspecification in the design) and evaluate the Varanus toolchain's utility. The workflow and tool provide validation of the safety documents, traceability of the safety properties from the documentation to the system, and a verified oracle for RV.
