Methods of Software Verification

• Main Authors: R. E. Gurin, I. V. Rudakov, A. V. Rebrikov
• Format: Article
• Language: Russian
• Published: MGTU im. N.È. Baumana 2015-01-01
• Series: Nauka i Obrazovanie
• Subjects: analysis; static; dynamic; interpretation; symbolic execution; model checking
• Online Access: http://technomag.edu.ru/jour/article/view/158

<p>This article is devoted to the problem of software verification (SW). Methods of software verification designed to check the software for compliance with the stated requirements such as correctness, system security and system adaptability to small changes in the environment, portability and compatibility, etc. These are various methods both by the operation process and by the way of achieving result. The article describes the static and dynamic methods of software verification and paid attention to the method of symbolic execution. In its review of static analysis are discussed and described the deductive method, and methods for testing the model. A relevant issue of the pros and cons of a particular method is emphasized. The article considers classification of test techniques for each method. In this paper we present and analyze the characteristics and mechanisms of the static analysis of dependencies, as well as their views, which can reduce the number of false positives in situations where the current state of the program combines two or more states obtained both in different paths of execution and in working with multiple object values. Dependences connect various types of software objects: single variables, the elements of composite variables (structure fields, array elements), the size of the heap areas, the length of lines, the number of initialized array elements in the verification code using static methods. The article pays attention to the identification of dependencies within the framework of the abstract interpretation, as well as gives an overview and analysis of the inference tools.</p><p>Methods of dynamic analysis such as testing, monitoring and profiling are presented and analyzed. Also some kinds of tools are considered which can be applied to the software when using the methods of dynamic analysis. Based on the work a conclusion is drawn, which describes the most relevant problems of analysis techniques, methods of their solutions and at what stages of development it is advisable to use one or another method.</p>