Verifying Invariants Using theorem Proving
Verifying Invariants Using theorem Proving
复制标题
使用定理证明验证不变量
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Hassen Saïdi
中科院分区：
文献类型：
--
作者：
S. Graf;Hassen Saïdi
我们的目标是使用一个定理证明器，以一种类似于模型检查的方式来验证分布式系统的不变性。S系统由一组连续的成分来描述，每个成分由一个转移关系和一个定义初始状态集合的谓词INIT给出。为了证明P是S的一个不变量，我们用类似模型检验的方法，计算出一个比P强、比归纳不变量Init弱的最弱谓词P‘，即当P’在某一状态为真时，则P‘在执行任何可能的转换后仍为真。P是一个不变量的事实可以用程序变量集合上的一组谓词(没有比P多的量词)来表示，每个可能的系统转换对应一个谓词。为了证明这些谓词，我们根据它们的性质使用自动或辅助的定理证明。
Our goal is to use a theorem prover in order to verify invariance properties of distributed systems in a “model checking like” manner. A system S is described by a set of sequential components, each one given by a transition relation and a predicate Init defining the set of initial states. In order to verify that P is an invariant of S, we try to compute, in a model checking like manner, the weakest predicate P′ stronger than P and weaker than Init which is an inductive invariant, that is, whenever P′ is true in some state, then P′ remains true after the execution of any possible transition. The fact that P is an invariant can be expressed by a set of predicates (having no more quantifiers than P) on the set of program variables, one for every possible transition of the system. In order to prove these predicates, we use either automatic or assisted theorem proving depending on their nature.