Subsequence Invariants
Subsequence Invariants
复制标题
子序列不变量
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
B. Finkbeiner
中科院分区：
文献类型：
--
作者：
Klaus Dräger;B. Finkbeiner
我们引入子序列不变量，它根据同步事件的发生来表征并发系统的行为。与引用系统状态变量的状态不变量不同，子序列不变量是在辅助计数器变量上定义的，这些辅助计数器变量反映给定集合中的事件序列到目前为止发生的频率。子序列不变量是对可能的计数器值的线性约束。我们允许子序列的每次出现与其他事件任意交错。因此，当给定过程与其他过程组成时，保留子序列不变量。因此，可以为每个过程单独计算子序列不变量，然后用于对整个系统进行推理。提出了一种有效的子序列不变量综合算法。我们的构造可以增量地应用于给定事件序列增长集的不变量增长集。
We introduce subsequence invariants, which characterize the behavior of a concurrent system in terms of the occurrences of synchronization events. Unlike state invariants, which refer to the state variables of the system, subsequence invariants are defined over auxiliary counter variables that reflect how often the event sequences from a given set have occurred so far. A subsequence invariant is a linear constraint over the possible counter values. We allow every occurrence of a subsequence to be interleaved arbitrarily with other events. As a result, subsequence invariants are preserved when a given process is composed with additional processes. Subsequence invariants can therefore be computed individually for each process and then be used to reason about the full system. We present an efficient algorithm for the synthesis of subsequence invariants. Our construction can be applied incrementally to obtain a growing set of invariants given a growing set of event sequences.