A Statistical Model Checker for Nondeterminism and Rare Events (Artifact)

The Modest Toolset for quantitative modelling and verification includes the 'modes' statistical model checker. We present 'modes' in our TACAS 2018 tool paper titled "A Statistical Model Checker for Nondeterminism and Rare Events", with a particular focus on its capabilities in automated rare event simulation and in approximating optimal schedulers on nondeterministic models. In the paper, we present an experimental evaluation of the capabilities (in terms of the kinds of supported models and analyses), performance, and scalability (across multi-core and distributed setups). This artifact contains (1) the version of 'modes' and (2) the model files used for our experiments, (3) the raw experimental results, (4) summarising tabular views of those results (from which we derived the tables of results included in the paper), and (5) a Linux shell script to replicate a subset of the experiments. Since our complete experiments take several hours to complete and require powerful hardware and computer clusters, we have selected a subset for the replication script. It runs to completion within less than one hour on typical workstation hardware of today while still substantiating the main conclusions drawn in the paper.

面向定量建模与验证的Modest工具集（Modest Toolset）内置了统计模型检查器'modes'。我们在TACAS 2018的工具论文《面向非确定性与稀有事件的统计模型检查器》中对'modes'进行了详细介绍，重点阐述了其在自动化稀有事件模拟以及非确定性模型上近似最优调度器方面的核心能力。该论文中，我们针对该工具的功能（涵盖支持的模型类型与分析任务类型）、性能以及可扩展性（支持多核与分布式部署场景）开展了系统性实验评估。本附属工件包含：(1) 'modes'工具的可执行版本；(2) 实验所用的模型文件；(3) 原始实验结果数据；(4) 上述结果的汇总表格视图（我们据此整理得到论文中刊载的结果表格）；(5) 用于复现部分实验的Linux Shell脚本。由于完整实验耗时数小时，且需要高性能硬件与计算机集群支持，我们仅在复现代码中选取了部分实验子集。该复现代码可在当前主流工作站硬件上于一小时内完成运行，同时仍能验证论文中得出的核心结论。