论文部分内容阅读
以带有多个可接受条件的广义Büchi自动机为研究对象,提出基于启发式NDFS的模型检测新算法.该算法结合on-the-fly算法与启发式NDFS算法,能较快地判断出广义Büchi自动机非空性,通过理论证明和实验验证了算法的正确性和可行性.与已有算法相比,在广义Büchi自动机非空的情况下,该算法减少了系统状态空间的搜索,提高了检测效率,且能形成相应反例,为缓解形式化验证中的状态空间爆炸问题提供了有效的解决途径,为安全苛求系统的安全性保障提供了有力支撑,丰富了基于模型的软件形式化开发方法.
Taking a generalized Büchi automaton with multiple acceptable conditions as the research object, a new model detection algorithm based on heuristic NDFS is proposed, which combines the on-the-fly algorithm and the heuristic NDFS algorithm to quickly determine the generalized Büchi automaton is non-norm, and the correctness and feasibility of the algorithm are verified by theoretical proofs and experiments.Compared with existing algorithms, this algorithm reduces the search of system state space when the generalized Büchi automaton is not empty, Improve the detection efficiency, and can form the corresponding counterexample, which provides an effective solution to alleviate the state space explosion problem in formal verification, provides a strong support for the safety protection of the safety-critical system, and enriches the formalization of model-based software Development method.