Generating optimal distinguishing sequences with a model checker.

This paper presents an approach for the automatic generation of shortest Distinguishing Sequences (DS) with the Uppaal model checker. The presented method is applicable to a large number of extended finite state machines and it will find an optimal result, if a DS sequence exists for the considered...

Mô tả đầy đủ

Chi tiết về thư mục
Xuất bản năm:	Software engineering notes. 30, 5 (2005).
Tác giả chính:	Robinson-Mallett, Christopher
Định dạng:	Bài viết
Ngôn ngữ:	English
Những chủ đề:	Theory of computation. Computation by abstract devices. Models of computation. Software. Software engineering. Software / Program Verification. Testing and debugging. Analysis of algorithms and problem complexity. Nonnumerical algorithms and problems. Algorithms. Verification. Distinguishing sequence. Extended finite state machines. Model checking. State identification. Test generation.