From Model Checking to Runtime Verification and Back
From Model Checking to Runtime Verification and Back
复制标题
从模型检查到运行时验证并返回
DOI：
10.1007/978-3-319-67531-2_14
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
J. Barnat
中科院分区：
文献类型：
--
作者：
Katarína Kejstová;Petr Ročkai;J. Barnat
我们描述了一种新颖的方法，用于调整现有的软件模型检查器来执行精确的运行时验证。允许被测软件与更广泛的环境（包括文件系统和网络）进行通信。对模型检查器的修改很小且独立，这使得这是在新上下文中重用现有模型检查工具的可行策略。此外，根据运行时验证模式下单次执行期间收集的数据，我们自动重新构建执行环境的描述，然后可以在标准的、成熟的模型检查器中使用该描述。这个额外的验证步骤可以进一步提高覆盖率，特别是在并行程序的情况下，而不会在运行时验证过程中引入大量开销。
We describe a novel approach for adapting an existing software model checker to perform precise runtime verification. The software under test is allowed to communicate with the wider environment (including the file system and network). The modifications to the model checker are small and self-contained, making this a viable strategy for re-using existing model checking tools in a new context.Additionally, from the data that is gathered during a single execution in the runtime verification mode, we automatically re-construct a description of the execution environment which can then be used in the standard, full-blown model checker. This additional verification step can further improve coverage, especially in the case of parallel programs, without introducing substantial overhead into the process of runtime verification.