Storm Docker镜像文档

1. 镜像概述与主要用途

Storm是一款现代概率模型检查器，专注于对概率系统进行形式化验证和分析。该Docker镜像封装了Storm的核心功能，提供便捷的部署和运行环境，用户无需手动配置依赖即可快速开展概率系统的建模与验证工作。主要用途包括验证概率系统的正确性、分析系统性能指标（如可靠性、安全性）及评估系统在不确定环境下的行为。

2. 核心功能与特性

• 多模型支持：兼容离散时间马尔可夫链（DTMC）、连续时间马尔可夫链（CTMC）、马尔可夫决策过程（MDP）等多种概率模型。
• 高效算法：集成先进的模型检查算法，支持可达性分析、期望奖励计算、长期平均奖励分析等核心任务。
• 接口友好：提供命令行接口（CLI），支持通过简单命令指定模型文件和验证属性，便于自动化集成。
• 工具兼容性：可与PRISM、JANI等概率建模工具兼容，支持多种输入格式（如.prism、.jani），满足多样化分析需求。

3. 使用场景与适用范围

Storm适用于以下领域：

• 计算机科学与软件工程：验证分布式系统、通信协议中的概率行为（如容错机制、随机调度策略的可靠性）。
• 人工智能与强化学***：分析马尔可夫决策过程（MDP）模型的策略优化、奖励收敛性及探索-利用权衡。
• 控制系统与嵌入式系统：评估安全关键系统（如自动驾驶、***设备）在随机故障下的失效概率。
• 学术研究：作为概率模型检查领域的基准工具，支持新算法的验证与性能对比。

4. 使用方法与配置说明

4.1 基本使用（docker run）

通过挂载本地模型文件，执行Storm分析：

docker run -v /本地模型路径:/data stormchecker/storm:latest storm /data/模型文件 --property "属性表达式"

参数说明：

• -v /本地模型路径:/data：将本地目录挂载至容器/data，使容器访问本地模型文件。
• stormchecker/storm:latest：Storm镜像名称（默认最新版，具体标签见Docker Hub）。
• storm /data/模型文件：执行Storm命令，指定容器内模型文件路径（支持.prism、.jani等格式）。
• --property "属性表达式"：待验证的概率属性（语法见4.2节）。

4.2 常用属性表达式示例

Storm支持以下属性类型（完整语法见***文档）：

• 可达性概率：Pmin=? [F "error"]（到达"error"状态的最小概率）。
• 有界可达性：Pmax=? [F<=10 "success"]（10步内到达"success"状态的最大概率）。
• 期望奖励：R{"cost"}min=? [F "done"]（到达"done"状态的最小期望成本）。
• 长期平均奖励：R{"throughput"}avg=? [S]（稳态下的平均吞吐量）。

4.3 高级配置（算法参数）

通过命令行选项调整分析精度或资源限制：

docker run -v /本地模型路径:/data stormchecker/storm:latest storm /data/model.jani \
  --property "P=? [F \"target\"]" \
  --precision 1e-6 \          # 数值计算精度（默认1e-3）
  --max-states ***        # 状态空间上限（避免内存溢出）

4.4 查看帮助与版本

获取命令行选项详情：

docker run stormchecker/storm:latest storm --help

查看镜像版本：

docker run stormchecker/storm:latest storm --version

5. 注意事项

• 模型文件需符合输入格式规范，建议使用JANI格式（支持复杂结构）或PRISM格式（广泛用于学术场景）。
• 大规模模型分析需配置足够内存，可通过docker run --memory=8g限制容器内存（根据模型复杂度调整）。
• 更多示例与教程见Storm***文档。