Symbolic model checking for discrete real-time systems  

作　　者：Xiangyu LUO Lijun WU Qingliang CHEN Haibo LI Lixiao ZHENG Zuxi CHEN 

机构地区：[1]College of Computer Science & Technology, Huaqiao University [2]Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology [3]School of Computer Science and Engineering, University of Electronic Science and Technology of China [4]Department of Computer Science, Jinan University

出　　处：《Science China(Information Sciences)》2018年第5期199-221,共23页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China (Grant Nos. 61170028, 61572234, 61370072, 71571056);Young Scientists Fund of the National Natural Science Foundation of China (Grant No. 61502184);Program for New Century Excellent Talents in Fujian Province Universities (Grant No. 2013FJ-NCET-ZR03);Natural Foundation Key Program for Young Scholars in the Universities of Fujian Province (Grant No. JZ160409);Natural Science Foundation of Fujian Province (Grant No. 2015J01255);Promotion Program for Young and Middle-aged Teacher in Science and Technology Research of Huaqiao University (Grant No. ZQN-YX109);Guangxi Key Laboratory of Trusted Software (Grant No. kx201323)

摘　　要：A considerably large class of critical applications run in distributed and real-time environments,and most of the correctness requirements of such applications must be expressed by time-critical properties.To enable the specification and verification of these properties in both qualitative and quantitative manners,we propose a new real-time temporal logic RTCTL＊, by incorporating both the quantitative（bounded）future and past temporal operators from the qualitative temporal logic CTL＊. First, we propose a symbolic method for constructing the temporal tester for arbitrary principally temporal formulas. A temporal tester is constructed as a non-deterministic transducer with a fresh boolean output variable, such that at any position the output variable is set to be true if and only if the corresponding formula holds starting from that position.Then we propose a symbolic model checking method for RTCTL＊ over finite-state transition systems with weak fairness constraints based on the compositionality of testers. The soundness and completeness of the model checking method, the expressiveness of RTCTL＊, and the complexity of the tester construction are described and proven. We have already implemented an efficient model checking prototype for the real-time linear temporal logic RTLTL, which is a quantifier-free version of RTCTL＊, by building upon the Nu SMV model checker. The theoretical and the experimental results from the prototype both confirm that for checking bounded temporal formulae of the form f U[0,b]g or f S[0,b]g, our method performs exponentially better than the translation-based method in Nu SMV.A considerably large class of critical applications run in distributed and real-time environments,and most of the correctness requirements of such applications must be expressed by time-critical properties.To enable the specification and verification of these properties in both qualitative and quantitative manners,we propose a new real-time temporal logic RTCTL＊, by incorporating both the quantitative（bounded）future and past temporal operators from the qualitative temporal logic CTL＊. First, we propose a symbolic method for constructing the temporal tester for arbitrary principally temporal formulas. A temporal tester is constructed as a non-deterministic transducer with a fresh boolean output variable, such that at any position the output variable is set to be true if and only if the corresponding formula holds starting from that position.Then we propose a symbolic model checking method for RTCTL＊ over finite-state transition systems with weak fairness constraints based on the compositionality of testers. The soundness and completeness of the model checking method, the expressiveness of RTCTL＊, and the complexity of the tester construction are described and proven. We have already implemented an efficient model checking prototype for the real-time linear temporal logic RTLTL, which is a quantifier-free version of RTCTL＊, by building upon the Nu SMV model checker. The theoretical and the experimental results from the prototype both confirm that for checking bounded temporal formulae of the form f U[0,b]g or f S[0,b]g, our method performs exponentially better than the translation-based method in Nu SMV.

关 键 词：symbolic model checking temporal tester real-time temporal logic just discrete system OB-DDs 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]