Research On Temporal Logic To Assertion Graphs

With the successful application of Internet and Embed System in system such ascar/airplane and other safety systems,it seems that the dependence on computerdevice’s function will be more and more obvious.In fact,the pace of changing like thiswill be more and more fast.Because of rapid growth of technology,the reliable methodof developing verification system are becoming more and more important.the validmethods for verifying complexity system include simulation verification,testingverification and formal verification.Former two verification methods take a long timeand are difficult to use,what’s more,their unablity to handle all possible inputs andpotential bugs is fatal.Formal verification verify whether a system satisfies design bymathematic methodology which makes sure the absolute covery of test case. Modelchecking is a formal verification technology used to verify finite state concurrentsystem.In model checking,models are built firstly,and are used to check if they satisfythe specification.Temporal logic such as CTL and LTL is commonly used asspecification language,model checking based on temporal logic has already usedwidely in industry.GSTE is a efficiently automatic model checking algorithm,whichuses assertion graphs as its specification language.Assertion graphs is easily to usedcomparing with temporal logic,and model and properties of GSTE are both executedconcurrently.In conclusion,It’s practical converting temporal logic to assertion graphs.The paper starts with basic concepts of formal methods,comparing temporal logicwith assertion graphs and extending assertion graphs.Extending verification algorithmis proposed on extent of the paper,aiming at the capacity of verifying extendingassertion graphs.In this paper, formal methods and model checking are firstly introduced, and thenresearch significance is given. Secondly after an adequate introduction to verificationof GSTE, assertion graphs, its specification language, are introduced.Thirdly,weintroduce LTL, CTL and model checking algorithm based on them and compare CTLwith LTL and GSTE with model checking algorithm based on CTL,convert temporallogic to assertion graphs,illustrate limitation of assertion graphs between convention.We define terminate based on concepts in GSTE and terminate assertiongraphs based on assertion graphs and extend algorithm in GSTE and proposeterminately satisfy model checking algorithm aiming at the capacity of handlingextending assertion graphs,and prove the correction of algorithm.At last,computingprocess are shown by verifying if a model satisfyies properties.