More Scalable LTL Model Checking via Discovering Design-Space Dependencies (Artifact)

This record contains a single artifact in compressed .tar.gz format, holding software and models to run the Discover Design-Space Dependencies (D3) algorithm for scalable Linear Temporal Logic (LTL) model checking on two benchmarks derived from real-world case studies. The artifact relates to the TACAS 2018 paper:Dureja, R., Rozier, K.Y.: More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D3). In: TACAS (2018)The artifact includes the benchmarks evaluated, source code, and scripts to efficiently reproduce the results reported in the paper. Please refer to the README contained within the artifact for more detailed information.The D3_Artifacts subdirectory contains tools, scripts, results, plots and models for experiments to demonstrate the industrial scalability of D3 on NASA’s NextGen airtraffic control system (modelled by a set of 1,620 real-life, publicly-available SMV-language benchmark models with LTL specifications) and to evaluate the property-dependence analysis on real-life models of Boeing AIR Wheel Braking System.D3 is implemented as a preprocessing script in ~2,000 lines of Python code (.py files). Other file types include SMV-language (.smv), related metadata files (.xml) and mapping (.map) files, command scripts (.cmd), plots in .jpg image format and documents in .html and graphical .svg formats.The artifact has been thoroughly tested on the Ubuntu Virtual Machine (VM) available at:Hartmanns, Arnd; Wendler, Philipp (2018). figshare. https://doi.org/10.6084/m9.figshare.5896615BackgroundModern system design often requires comparing several models over a large design space. Different models arise out of a need to weigh different design choices, to check core capabilities of versions with varying features, or to analyze a future version against previous ones. Model checking can compare different models; however, applying model checking off-the-shelf may not scale due to the large size of the design space for today’s complex systems. We exploit relationships between different models of the same (or related) systems to optimize the modelchecking search. Our algorithm, D3, preprocesses the design space and checks fewer model-checking instances, e.g., using nuXmv. It automatically prunes the search space by reducing both the number of models to check, and the number of LTL properties that need to be checked for each model in order to provide the complete model-checking verdict for every individual model-property pair. We formalize heuristics that improve the performance of D3. We demonstrate the scalability of D3 by extensive experimental evaluation, e.g., by checking 1,620 real-life models for NASA’s NextGen air traffic control system.

本记录包含一个单一的压缩文件（.tar.gz格式），其中包含运行Discover Design-Space Dependencies（D3）算法的软件和模型，该算法适用于可扩展的线性时序逻辑（LTL）模型检查，并针对源自现实世界案例研究的两个基准进行优化。该文件与TACAS 2018论文《通过发现设计空间依赖性（D3）实现更可扩展的LTL模型检查》（Dureja, R., Rozier, K.Y.: More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D3). In: TACAS (2018)）相关。该文件包括评估的基准、源代码和脚本，以便高效地重现论文中报告的结果。请参阅文件内的README以获取更详细的信息。D3_Artifacts子目录包含用于展示D3在NASA NextGen空中交通管制系统（由一组1,620个真实可用的SMV语言基准模型和LTL规范建模）上的工业可扩展性的工具、脚本、结果、图表和模型，以及评估对波音AIR轮式制动系统真实模型上的属性依赖性分析。D3作为约2,000行Python代码（.py文件）的前处理脚本实现。其他文件类型包括SMV语言（.smv）、相关元数据文件（.xml）和映射文件（.map）、命令脚本（.cmd）、.jpg图像格式的图表以及.html和图形.svg格式的文档。该文件已在Ubuntu虚拟机（VM）上进行了彻底测试，相关信息可参考Hartmanns, Arnd; Wendler, Philipp (2018). figshare. https://doi.org/10.6084/m9.figshare.5896615。现代系统设计通常需要在大规模设计空间内比较多个模型。不同的模型源于权衡不同的设计选择、检查具有不同特性的版本的核心能力或分析未来版本与之前版本之间的差异。模型检查可以比较不同的模型；然而，由于现代复杂系统设计空间的大规模，现成的模型检查可能无法扩展。我们利用同一（或相关）系统不同模型之间的关系来优化模型检查搜索。我们的算法D3预处理设计空间，并检查较少的模型检查实例，例如使用nuXmv。它通过减少需要检查的模型数量和每个模型需要检查的LTL属性数量来自动剪枝搜索空间，以便为每个单独的模型-属性对提供完整的模型检查结论。我们形式化了提高D3性能的启发式方法。我们通过广泛的实验评估证明了D3的可扩展性，例如，通过检查NASA NextGen空中交通管制系统的1,620个真实模型。