论文标题
在过渡系统（扩展版本）的均匀采样轨迹上
On Uniformly Sampling Traces of a Transition System (Extended Version)
论文作者
论文摘要
约束随机验证（CRV）的一个关键问题是产生输入刺激，从而在其行为空间的有针对性角落良好覆盖了系统的运行。然而，现有的CRV解决方案对系统运行的分配没有正式的保证。在本文中，我们朝着解决这个问题迈出的第一步。我们提出了一种基于代数决策图的算法，用于采样有界轨迹（即状态序列），具有可证明的均匀性（或偏差）保证的顺序电路，同时满足给定限制。我们已经在称为tracesampler的工具中实现了算法。广泛的实验表明，TraceSampler优于提供类似均匀性保证的替代方法。
A key problem in constrained random verification (CRV) concerns generation of input stimuli that result in good coverage of the system's runs in targeted corners of its behavior space. Existing CRV solutions however provide no formal guarantees on the distribution of the system's runs. In this paper, we take a first step towards solving this problem. We present an algorithm based on Algebraic Decision Diagrams for sampling bounded traces (i.e. sequences of states) of a sequential circuit with provable uniformity (or bias) guarantees, while satisfying given constraints. We have implemented our algorithm in a tool called TraceSampler. Extensive experiments show that TraceSampler outperforms alternative approaches that provide similar uniformity guarantees.
