DocumentCode :
3175435
Title :
Towards Test Case Generation for Synthesizable VHDL Programs Using Model Checker
Author :
Ayav, Tolga ; Tuglular, Tugkan ; Belli, Fevzi
Author_Institution :
Dept. of Comput. Eng., Izmir Inst. of Technol., Izmir, Turkey
fYear :
2010
fDate :
9-11 June 2010
Firstpage :
46
Lastpage :
53
Abstract :
VHDL programs are often tested by means of simulations, relying on test benches written intuitively. In this paper, we propose a formal approach to construct test benches from system specification. To consider the real-time properties of VHDL programs, we first transform them to timed automata and then perform model checking against the properties designated from the specification. Counterexamples returned from the model checker serve as a basis of test cases, i.e. they are used to form a test bench. The approach is demonstrated and complemented by a simple case study.
Keywords :
formal specification; hardware description languages; program testing; program verification; formal system specification; model checker; synthesizable VHDL programs; test case generation; timed automata; Automata; Automatic testing; Circuit synthesis; Computational modeling; Field programmable gate arrays; Mathematical model; Reliability engineering; Safety; Software testing; System testing; Test case generation; model checking; program transformation; synthesizable VHDL; timed automata;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Secure Software Integration and Reliability Improvement Companion (SSIRI-C), 2010 Fourth International Conference on
Conference_Location :
Singapore
Print_ISBN :
978-1-4244-7644-2
Type :
conf
DOI :
10.1109/SSIRI-C.2010.22
Filename :
5521560
Link To Document :
بازگشت