| Model checking is an important approach to improve the reliability of hardware and software systems. Basically, in model checking, a temporal logic formula is used to describe the desired property of the system, and a Buchi automaton is utilized to describe the model of the system. Next, negation of the temporal logic formula is transformed into a Buchi automaton. Finally, product of the two automata is constructed, and emptiness of the eventually product automaton is checked. If it is empty, the system satisfies the specification; otherwise, the system does not satisfies the specification, and counterexamples are provided.Linear temporal logic LTL is one of the most popular languages useful in describing the properties of systems in model checking. Thereby, transformation from LTL formulas to Buchi automata is a key step in LTL model checking. Performance of transformation algorithm directly affects the efficiency of LTL model checkers. Currently, typical transformation algorithms are the on-the-fly transformation algorithm proposed by Gerth et al., and the one based on VWAA proposed by Gastin and Oddoux. These algorithms have been applied in some model checker. However, when dealing with large and complex LTL formulas, these algorithms fails in providing the resulting automata..In order to overcome the above problem, a new transformation algorithm based on the CF normal form is proposed in this thesis. Meanwhile, according to the advantages of alternating formulas, the transforming algorithm is further improved. In addition, by taking advantages of strongly connected component in directed graph, the resulting Buchi automata are further simplified. Based on the new algorithm, we develop a tool called LTLNFBA for transforming LTL formulas to Buchi automata. We compare LTLNFBA with the best two tools available for transforming LTL formulas to Buchi automata, experimental results show that LTLNFBA works well in practice. |
PDF Full Text Request