跳到主要内容

PRISM 文件结构

引言​

PRISM（Probabilistic Symbolic Model Checker）是用于分析概率系统的形式化验证工具。理解其文件结构是构建有效模型的第一步。本章将详细介绍PRISM的两种核心文件类型：模型文件（.prism）和属性文件（.props），并通过实际案例展示它们的组成与关联。

PRISM 模型文件（.prism）​

模型文件定义了系统的状态、转换规则和概率行为，其结构包含以下关键部分：

1. 模块（Module）​

模块是PRISM的基本构建块，代表系统中的并发组件。每个模块包含变量和命令。

prism
module M1
    x : [0..5] init 0; // 变量定义（范围0-5，初始值0）
    
    [action] x < 5 -> 0.8:(x'=x+1) + 0.2:(x'=0); // 命令（动作标签+概率转移）
endmodule

2. 变量（Variables）​

变量描述系统状态，支持布尔、整数和时钟类型：

  • b : bool init false;
  • count : [0..10];
提示

使用init指定初始值，否则PRISM自动选择范围最小值。

3. 命令（Commands）​

命令定义状态转换，格式为：
[动作标签] 守卫条件 -> 概率1:更新1 + 概率2:更新2;

prism
[retry] fail=true -> 0.9:(fail'=false) + 0.1:(fail'=true);

4. 常量与公式​

常量用于参数化模型，公式可定义中间计算：

prism
const int MAX = 100;  
formula ready = (queue_size <= MAX/2);

5. 系统定义​

通过system关键字指定模块组合方式（如并行）：

prism
system "M1 || M2" endsystem

PRISM 属性文件（.props）​

属性文件（.props）包含待验证的规约，使用PCTL（概率计算树逻辑）或CSL（连续随机逻辑）语法：

1. 概率属性​

验证某路径的概率是否满足阈值：

prism
P>=0.95 [ F success ]  // "最终成功"的概率≥95%

2. 期望值属性​

计算长期平均或累积值：

prism
R{"energy"}<=10 [ C<=100 ] // 100步内累计能耗不超过10

3. 时间相关属性​

适用于实时系统：

prism
P<0.1 [ F<=3600 error ] // 1小时内发生错误的概率<10%

实际案例：简单通信协议​

模型文件 (protocol.prism)​

prism
// 定义常量
const double p_loss = 0.1;  

module Sender
    sent : bool init false;  
    [send] !sent -> (sent'=true);  
endmodule

module Receiver
    received : bool init false;  
    [recv] sent & !received -> 
        1-p_loss:(received'=true) + p_loss:(received'=false);  
endmodule

system "Sender || Receiver" endsystem

属性文件 (protocol.props)​

prism
// 消息最终被接收的概率
P>=0.99 [ F received ]  

// 平均重传次数
R{"retransmissions"}=? [ C<=100 ]

总结​

文件类型核心元素用途
.prism模块、变量、命令、系统定义描述系统行为与概率逻辑
.propsPCTL/CSL表达式指定待验证的系统属性
练习
  1. 扩展上述通信协议模型，增加超时重传机制。
  2. 编写属性验证“在3次重传内成功接收的概率”。

扩展阅读：