面向基于仿真的形式化验证的约束场景的任意时长均匀随机采样与枚举

基于模型的网络物理系统（CPS）非终止验证方法通常依赖于对受验证系统（SUV）模型在可能不同时长的输入场景下进行数值仿真，这些场景选自满足给定约束者。此类约束通常源于对 SUV 输入及其运行环境的需求（或假设），以及为（例如）优先处理（通常极长的）验证活动而施加的附加条件，如聚焦于显式演练选定需求的场景，或避免其满足中的空真。在此背景下，能够在满足给定约束的场景中高效随机采样（具已知分布，如均匀分布）或高效枚举（可能以均匀随机顺序）是验证过程可行性的关键促成因素，例如通过基于仿真的统计模型检验。不幸的是，在非平凡约束组合下，如输入序列空间中的马尔可夫随机游走等迭代方法一般无法按给定分布提取场景，且生成感兴趣合法场景的效率极低。我们展示了如何给定由有限记忆监视器简洁定义的输入场景约束集，综合出一种数据结构（场景生成器），从中可通过（可能均匀的）随机采样或（随机化）枚举高效提取满足输入约束的任意时长场景。我们的方法可无缝支持几乎所有基于仿真的 CPS 验证方法，从简单随机测试到统计模型检验与形式化（即穷举）验证。