关键词: 模型检验, 空属性探测, 可计算时态逻辑公式, 验证综合系统系统

Abstract: In model checking a new method is proposed on checking whether a system property represented by a computation temperal logic(CTL) formula is vacuity. From the polarity of atomic proposition, a series of CTL formulae is derived by substituting the atomic proposition with TRUE or FALSE, before they are verified by model checking tools. If one of the CTL formulae has passed the verification, then it is concluded that the system property is a vacuity. In this solution, to check the vacuity of the CTL formula, it is not necessary to substitute all of its sub-formulae by TRUE or FALSE, but instead, it is enough to substitute its atomic proposition, and thus the number of times for checking is linear with the number of atomic propositions. With a VIS system, effectiveness of this solution is further verified by checking the vacuity of specification on the cross-road traffic controller.

Key words: model checking, vacuity detection, CTL formula, VIS system