The Study Of Acceleration Technology And Efficiency Of Control Structure-based Model Checking

Real-time system is a very important kind of computer system, whose validitydepends not only on the correctness of the system results, but also on the time whenthe results generate. For such systems it is essential to ensure its validity and safety,so rigorous analysis and verification are required during the design process. Timedautomata are very suitable to model and verify real-time systems, it is an importanttheory for real-time systems modeling and proving. In such systems, the controlprogram and the external environment often use different time scales, when suchsystems are modeled as timed automata, and then verified with the symbolic modelchecking techniques, serious fragments problem will be caused, and verification ratewill be decreased, and the space and time of model checking will be increased.Exact acceleration technology can solve the fragments problem caused bydifferent time scales during model checking process, its key technology is toconstruct acceleration model by adding an appended cycle to the timed automata, andthen accelerate the forward symbolic reachability analysis without changing thereachability property of timed automata. Since exact acceleration technology caneffectively solve the fragments problem, it has been widely used in reachabilityanalysis process. Despite the constantly development of the acceleration technology,there are still some problems with it, such as the construction of appended cycledepends on the size of acceleration window, which limits the application in practiceof the technology.The principle of exact acceleration technology is analyzed in this paper, and anexact acceleration method based on structure analysis is presented. By staticanglicizing of control structure of timed automata, the covering states can becalculated, of which the control locations are taken as candidates to add appendedcycle. Only the covering states should be saved during reachability analysis process.This approach not only achieves acceleration but also effectively reduce the statespace. The correctness and validity of this method formally proved in this paper.In addition, in some cases, the appended cycle couldn’t bring evident acceleration effect, and even worse it will decrease the speed of verification. In orderto achieve effective acceleration, exact acceleration techniques are analyzed, and theeffect of acceleration under different conditions is studied. By analyzing the mainparameters in acceleration process, a condition to determine whether the exactacceleration is effective is deduced, which makes the exact acceleration techniquemore effective. Experimental results show that, in most cases, this condition canaccurately determine whether a model needs to be accelerated.