Automatic Test Case Generation for a Model Checker on a Diagram Describing Constraints of Execution Order of Functions

Yusuke AOYAMA  Takeru KUROIWA  Noriyuki KUSHIRO  

D - Abstracts of IEICE TRANSACTIONS on Information and Systems (Japanese Edition)   Vol.J101-D   No.3   pp.502-511
Publication Date: 2018/03/01
Online ISSN: 1881-0225
Type of Manuscript: Special Section PAPER (Special Section on Student Research)
model checking,  SPIN,  emulator,  accumulating of test cases,  

Full Text(in Japanese): PDF(1.3MB)
>>Buy this Article

Testing concurrency of systems is important, but all execution orders practically cannot be tested; hence, designers must prioritize test cases which should be conducted. Specifications, however, often omit dependency relations among functions, and the prioritization is, therefore, generally difficult. This paper proposes a diagram representation and a method to generate test cases for a model checker from the diagram representation. The diagram representation visualizes relations among functions running concurrently and helps designers to determine combinations of functions that should be tested. The combinations of functions are tested using automatically generated test cases.