名称: 模型检查器描述: ‘实现有限状态系统的有界模型检查。使用场景: (1) 验证并发程序, (2) 硬件验证, (3) 协议验证.’ 版本: 1.0.0 标签:

验证
模型检查
时态逻辑
状态空间难度: 高级语言:
python
ocaml 依赖: []

模型检查器

使用SAT/SMT求解器实现有界模型检查。

使用场景

并发程序验证
协议验证
硬件验证
错误检测

技能功能

编码转换 - 转换为SAT/SMT
展开循环 - 有界探索
检查属性 - 安全性、活性
生成反例 - 针对违规

实现

from dataclasses import dataclass, field
from typing import Dict, List, Set, Optional
import z3

@dataclass
class State:
    """程序状态"""
    pc: int  # 程序计数器
    vars: Dict[str, int]  # 变量

@dataclass
class Transition:
    """状态转换"""
    from_state: State
    to_state: State
    condition: Optional[z3.BoolRef] = None

@dataclass
class Model:
    """转换系统"""
    states: Set[State]
    initial: Set[State]
    transitions: List[Transition]
    variables: List[str]

@dataclass
class Property:
    """时态属性"""
    pass

@dataclass
class Invariant(Property):
    """不变式: 始终P"""
    predicate: z3.BoolRef

@dataclass
class Reachability(Property):
    """最终可达: ◇P"""
    predicate: z3.BoolRef

class BoundedModelChecker:
    """有界模型检查器"""
    
    def __init__(self):
        self.solver = z3.Solver()
        self.model: Optional[Model] = None
        self.bound: int = 0
    
    def check(self, model: Model, property: Property, 
              bound: int = 10) -> 'CheckResult':
        """
        有界模型检查
        
        返回: (可满足/不可满足, 如果可满足则返回反例)
        """
        
        self.model = model
        self.bound = bound
        
        match property:
            case Invariant(pred):
                return self.check_invariant(pred, bound)
            
            case Reachability(pred):
                return self.check_reachability(pred, bound)
        
        raise ValueError(f"未知属性: {property}")
    
    def check_invariant(self, invariant: z3.BoolRef, 
                       bound: int) -> 'CheckResult':
        """
        检查不变式: ⊡P (始终P)
        
        编码: ∧_{i=0}^{k} (状态_i → P)
        """
        
        self.solver = z3.Solver()
        
        # 创建状态变量
        state_vars = self.create_state_variables(bound)
        
        # 编码初始状态
        self.encode_initial(state_vars[0])
        
        # 编码转换
        for i in range(bound):
            self.encode_transition(state_vars[i], state_vars[i+1])
        
        # 编码不变式违规
        for i in range(bound + 1):
            violation = z3.Not(self.encode_state_predicate(state_vars[i], invariant))
            self.solver.add(violation)
        
        # 检查
        if self.solver.check() == z3.sat:
            model = self.solver.model()
            return CheckResult(
                sat=True,
                counterexample=self.extract_trace(state_vars, model),
                message="不变式被违反"
            )
        
        return CheckResult(
            sat=False,
            counterexample=None,
            message="在边界内不变式成立"
        )
    
    def check_reachability(self, target: z3.BoolRef,
                          bound: int) -> 'CheckResult':
        """
        检查可达性: ◇P
        
        编码: ∃i. 状态_i → P
        """
        
        self.solver = z3.Solver()
        
        state_vars = self.create_state_variables(bound)
        self.encode_initial(state_vars[0])
        
        for i in range(bound):
            self.encode_transition(state_vars[i], state_vars[i+1])
        
        # 目标可达
        target_reached = z3.Bool('target_reached')
        for i in range(bound + 1):
            self.solver.add(
                target_reached == self.encode_state_predicate(state_vars[i], target)
            )
        
        self.solver.add(target_reached)
        
        if self.solver.check() == z3.sat:
            model = self.solver.model()
            return CheckResult(
                sat=True,
                counterexample=self.extract_trace(state_vars, model),
                message="目标可达"
            )
        
        return CheckResult(
            sat=False,
            counterexample=None,
            message="在边界内目标不可达"
        )
    
    def create_state_variables(self, bound: int) -> List[Dict[str, z3.Expr]]:
        """创建符号状态变量"""
        
        states = []
        
        for i in range(bound + 1):
            state = {}
            for var in self.model.variables:
                state[var] = z3.Int(f"s{i}_{var}")
            states.append(state)
        
        return states
    
    def encode_initial(self, state: Dict[str, z3.Expr]):
        """编码初始状态约束"""
        
        for init in self.model.initial:
            for var, val in init.vars.items():
                self.solver.add(state[var] == val)
    
    def encode_transition(self, from_state: Dict[str, z3.Expr],
                        to_state: Dict[str, z3.Expr]):
        """编码转换关系"""
        
        for trans in self.model.transitions:
            # 匹配: from_state 匹配 trans.from_state
            # 结果: to_state 匹配 trans.to_state
            
            conditions = []
            
            for var in self.model.variables:
                # 简单: 如果不改变则复制
                conditions.append(to_state[var] == from_state[var])
            
            # 添加特定转换的约束
            for var, val in trans.to_state.vars.items():
                if var in from_state and from_state[var] != val:
                    conditions.append(to_state[var] == val)
            
            if trans.condition:
                conditions.append(trans.condition)
            
            self.solver.add(z3.Or(conditions))
    
    def encode_state_predicate(self, state: Dict[str, z3.Expr],
                              pred: z3.BoolRef) -> z3.BoolRef:
        """为状态编码谓词"""
        
        # 将状态变量替换到谓词中
        subst = {z3.Int(var): val for var, val in state.items()}
        
        return z3.substitute(pred, subst)
    
    def extract_trace(self, states: List[Dict[str, z3.Expr]], 
                     model: z3.Model) -> List[Dict[str, int]]:
        """提取反例轨迹"""
        
        trace = []
        
        for state in states:
            concrete = {}
            for var, expr in state.items():
                val = model.eval(expr)
                concrete[var] = val.as_long()
            trace.append(concrete)
        
        return trace

@dataclass
class CheckResult:
    """模型检查结果"""
    sat: bool
    counterexample: Optional[List[Dict[str, int]]]
    message: str

并发程序验证

class ConcurrentModelChecker:
    """并发程序的模型检查器"""
    
    def __init__(self):
        self.checker = BoundedModelChecker()
    
    def verify_two_thread(self, program: 'Program', 
                        property: Property) -> CheckResult:
        """
        验证两个线程的程序
        
        交错语义:
        - 所有可能的线程调度
        - 共享内存一致性
        """
        
        # 建模为转换系统
        model = self.create_model(program)
        
        # 使用递增边界检查
        for bound in range(1, 20):
            result = self.checker.check(model, property, bound)
            
            if result.sat:
                return result
        
        return CheckResult(
            sat=False,
            counterexample=None,
            message="属性成立(或边界太小)"
        )
    
    def create_model(self, program: 'Program') -> Model:
        """创建转换系统模型"""
        
        # 提取状态和转换
        states = set()
        initial = set()
        transitions = []
        
        # 初始状态
        init_state = State(pc=0, vars=program.init_vars)
        initial.add(init_state)
        states.add(init_state)
        
        # 从CFG构建转换
        for stmt in program.statements:
            from_state = State(stmt.from_pc, stmt.from_vars)
            to_state = State(stmt.to_pc, stmt.to_vars)
            
            trans = Transition(from_state, to_state, stmt.condition)
            transitions.append(trans)
            
            states.add(from_state)
            states.add(to_state)
        
        return Model(
            states=states,
            initial=initial,
            transitions=transitions,
            variables=list(program.variables)
        )

活性检查

class LivenessChecker:
    """检查活性属性"""
    
    def check_liveness(self, model: Model, property: Reachability) -> CheckResult:
        """
        检查: ◇P (最终P)
        
        使用公平性约束
        """
        
        # 检查: 我们能无限次达到P吗？
        # 添加公平性: 每个线程无限执行
        
        # 目前, 简单的有界版本
        checker = BoundedModelChecker()
        
        # 尝试逐渐增大的边界
        for bound in range(1, 50):
            result = checker.check(model, property, bound)
            
            if result.sat:
                return result
        
        return CheckResult(sat=False, message="属性可能不成立")

关键概念

概念	描述
有界模型检查	展开到有界深度
SAT/SMT编码	编码为布尔公式
反例	违反的轨迹
公平性	调度器的假设

属性

属性	符号	描述
不变式	⊡P	始终P
可达性	◇P	最终P
活性	□◇P	无限次P
安全性	□(P → Q)	如果P则Q

技巧

从小边界开始
使用谓词抽象
谨慎处理无限状态
考虑公平性

权威参考文献

参考文献	重要性
Clarke, Grumberg, Kroening, Peled, Veith, “Model Checking” (MIT Press, 2018)	模型检查的权威教科书
Biere, Cimatti, Clarke, Zhu, “Symbolic Model Checking without BDDs” (TACAS 1999)	BMC论文
Ball & Rajamani, “The SLAM Project: Debugging System Software via Static Analysis” (POPL 2002)	软件模型检查
Kurshan, “Computer-Aided Verification of Coordinating Processes” (1994)	硬件模型检查起源
Holzmann, “The Model Checker SPIN” (IEEE TSE 1997)	SPIN模型检查器

权衡与限制

模型检查方法权衡

方法	优点	缺点
显式状态	简单, 完整	状态爆炸
符号(BDD)	处理大状态	可能爆炸
有界(SMT)	适合错误检测	不能证明活性
谓词抽象	扩展到软件	精度损失

何时不使用模型检查

对于大型系统: 状态爆炸; 使用抽象
对于参数化系统: 无界验证困难
对于概率系统: 使用概率模型检查
对于实时系统: 使用时序自动机模型检查

复杂性考虑

显式状态: O(n)状态, 变量指数级
符号: 最坏情况指数级, 通常实用
BMC: 线性于边界×状态大小
SMT求解: NP难, 但Z3在实践中快速

限制

状态爆炸: 主要瓶颈; 组件指数级
无限状态: 需要抽象或有界检查
可扩展性: 不能处理大型软件系统
活性: 难以验证; 需要公平性假设
反例: 可能太长难以理解
参数化: N进程系统困难

研究工具与成果

模型检查工具:

工具	应用	学习内容
SPIN	Promela	模型检查
CBMC	C有界	有界验证
BLAST	C	谓词抽象
SLAM	Windows驱动	软件模型检查
Java PathFinder	Java	显式状态
Alloy	关系型	轻量级建模

关键论文

Clarke et al. - 模型检查论文
Biere et al. - BMC论文

研究前沿

1. 软件模型检查

目标: 扩展到大型代码库
方法: 谓词抽象, 抽象精炼
工具: CBMC, ESBMC

实现陷阱

陷阱	实际后果	解决方案
状态爆炸	无法探索所有状态	抽象
无限状态	不终止	有界检查

模型检查器Skill model-checker

模型检查器

使用场景

技能功能

实现

并发程序验证

活性检查

关键概念

属性

技巧

相关技能

权威参考文献

权衡与限制

模型检查方法权衡

何时不使用模型检查

复杂性考虑

限制

研究工具与成果

关键论文

研究前沿

1. 软件模型检查

实现陷阱