Title :
Design and verification of the sequential systems automata using temporal logic specifications
Author :
Ursu, A. ; Gruita, G. ; Zaporojan, S.
Author_Institution :
Dept. of Inf. Technol., Tech. Univ. of Moldova, Romania
Abstract :
A design and verification method of sequential systems automata using temporal logic specifications is proposed. The method is based on well-known Z. Manna and P. Wolper temporal logic satisfiability analysis procedure. A new satisfiability analysis algorithm for temporal logic specifications which includes past time as well as future time temporal logic operators is proposed. A case study is carried out which deals with two design examples
Keywords :
finite automata; formal specification; formal verification; logic design; sequential circuits; temporal logic; design; satisfiability analysis algorithm; sequential systems automata; temporal logic specifications; verification; Algorithm design and analysis; Automata; Design methodology; Information technology; Logic design; Process design; System testing; Tellurium; Timing;
Conference_Titel :
European Design and Test Conference, 1997. ED&TC 97. Proceedings
Conference_Location :
Paris
Print_ISBN :
0-8186-7786-4
DOI :
10.1109/EDTC.1997.582436
