Kolchin A. Development a toolkit for checking of asynchronous models

A method for on-the-fly exact state abstraction construction for temporal properties checking obtained first. The main distinction with existing methods is that the obtained method does not need additional experiments runs because the abstract state consists of values of attributes subset, which is sufficient for the model properties checking. So the abstract states do not distinguish a variation of insignificant attributes values, this fact gives an opportunity to significantly decrease number of states needed for the properties checking. A new method for guided search developed. At first a special regular expressions over alphabet of model transitions names are used as guides, and thus, the test goals specification improved. The method provides capability for automation of test scenario creation on a basis of formal model and thus gives an opportunity for decreasing of efforts needed for testing and model analysis.