Letychevskyy O. Verification and Testing of Interactive Systems Specified by Basic Protocols

The thesis is devoted to the methods for processing of requirements. Five parts of technology are considered – formalization of requirements as basic protocols, searching of inconsistencies and incompleteness, test generation from the set of basic protocols, synthesis and analysis of dynamic properties of model. Methods of algebraic and insertion programming are used in development. It is defined the special class of basic protocols, that present the requirements as the set of formal specifications. This class is suitable for the resolving technology tasks without exponential explosion. Correspondingly to developed formalism the algorithms of verification are created in thesis with usage of proving machine. The synthesis of model correspondingly to the set of basic protocols is considered in thesis. The different criteria of test generation are considered by means of symbolic modeling methods. These criteria are used for test generation from specifications created as modern engineer languages – MSC,SDL, UML.