Research And Development Of The Symbolic Model Checker For Real-Time Temporal Logic RTCTL* Based On Full Testers

Since the beginning of the 21st century,information technology has gradually be-come a powerful driving force for economic development and production efficiency improvement.With the increasing popularity of software technology,the software in-dustry shows a trend of rapid development.The complexity of system design is soaring with the increasing of scale and problem domain.It means that the possibility of error is greater and its security cannot be ignored.How to guarantee the security of the program and improve the reliability of it has been one of the core issues of software development.The model checking based on exhaustive state is widely concerned and applied because of its high degree of automation and providing counterexample when not satisfied.The existing formal specification languages of model checkers such as Computation Tree Logic(CTL)and Linear Temporal Logic(LTL),etc.,they all can't^verify the Real-Time Temporal Logic(RTCTL*),that is,their description ability is still insufficient.Therefore,this paper optimizes the RTCTL*algorithm based on full temporal testers and proves the soundness and completeness of main testers,then designs a RTCTL*symbolic model checker(RTSMC).Based on the symbolic model checking framework JTLV which is constructed by a highly modular approach,RTSMC implements the sym-bolic model checking algorithm of RTCTL*.Finally,new operators of RTSMC are checked entirely by the coverage testing and verification.Experimental results show that RTSMC extends the verification ability of JTLV,thereby,the time sensitive,con-currency and periodic real-time properties can be specified and verified.The combination of theory and practice makes the best use of both.The primary purpose of this paper is to implement the RTCTL*model checker.We also want to build an easy tool for researchers to learn.Therefore the development strictly follow the principle of low coupling,high modular implementation and the high readability.It can not only effectively relieve the state space explosion problem of explicitly state model checkers like the SPIN and CHESS but also provide a better way to study and implement model checking algorithms.