Abstract
Comparative analysis of two methods of abstract interpretation is given in the paper. The first method was proposed by P. Cousot, the second one was developed on automation department in NSTU independent from the first one. Both methods base on common idea of source code representation to a model and following analysis of it. Both methods assume investigation on all possible paths of program execution. Examples of analysis of same program were presented in the paper. In addition, differences of considered methods were carried out in the paper. Specifically the abstract interpretation method assumes to use for automatically checking of one class errors with specifically used data domain. The second studied method allows to developer to execute arbitrary checks and errors that might be find with use of domain could be find in moment of program interpretation. Another different is that abstract interpretation mothed allows analyzing program’s source code even without full information about system, despite the fact that precision will be lower. Full system representation required for the second method.
Keywords: software, testing, input intervals, formal verification, dynamic verification, verification, model checking, software models, graphs, total correctness of programs
References
1. Cousot P., Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Conference record of the fourth ACM symposium on principles of programming languages, Los Angeles, California, Jan. 17–19, 1977. New York, ACM Press, 1977, pp. 238–252.
2. Voevoda A.A., Romannikov D.O., Zimaev I.V. Primenenie UML diagramm i setei Petri pri razrabotke vstraivaemogo programmnogo obespecheniya [An approach to the using UML and Petri nets for embedded software designing]. Nauchnyi vestnik NGTU – Science bulletin of Novosibirsk state technical university, 2009, no. 4 (37), pp. 169–174.
3. Clarke E.M., Grumberg O., Peled D. Model checking. Cambridge, London, MIT Press, 2001. (Russ. ed.: Klark E., Gramberg O., Peled D. Verifikatsiya modelei programm: Model checking. Moscow, MTsNMO Publ., 2002. 416 p.).
4. Bush W., Pincus J., Sielaff D. A static analyzer for finding dynamic progam-ming errors. Software: practice and experience, 2000, vol. 30, iss. 7, pp. 775–802. doi: 10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H
5. Glukhikh M.I., Itsykson V.M., Tses'ko V.A. Ispol'zovanie zavisimostei dlya povysheniya tochnosti staticheskogo analiza programm [The use of dependencies for Improving the precision of program static analysis]. Modelirovanie i analiz informatsionnykh sistem – Modeling and analisys of information systems, 2011,
vol. 18, no. 4, pp. 68–79.
6. Romannikov D.O. O poiske vkhodnykh intervalov [On the search for input intervals]. Sbornik nauchnyh trudov NGTU – Transaction of scientific papers of Novosibirsk state technical university, 2014, no. 1 (75), pp. 140–145.
7. Islam S., Krinke J., Binkley D., Harman M. Coherent clusters in source code. Journal of systems and software, 2014, vol. 88, рр. 1–24.
8. Markov A.V., Romannikov D.O. Algoritm translyatsii diagrammy aktivnosti v set' Petri [Algorithm of automatic conversion of the activity diagram into Petri-net structure formats]. Doklady Akademii nauk vysshei shkoly Rossiiskoi Federatsii – Proceedings of the Russian higher school Academy of sciences, 2014, no. 1 (22), pp. 104–112.
9. Romannikov D.O. Nakhozhdenie oshibok obrashcheniia k nesushchestvuiushchim elementam massiva na osnovanii rezul'tatov analiza seti Petri [Finding errors or nonexistent array’s elements based on the results of the analysis Petri nets]. Sbornik nauchnyh trudov NGTU – Transaction of scientific papers of Novosibirsk state technical university, 2012, no. 1 (67), pp. 115–120.
10. Voevoda A.A., Markov A.V. Romannikov D.O. Razrabotka programmnogo obespecheniia: proektirovanie s ispol'zova-niem UML diagramm i setei Petri na primere ASU TP vodonapornoi stantsii [Software development: software design using UML diagrams and PETRI nets for example automated process control system of pumping station]. Trudy SPIIRAN – SPIIRAS proceedings, 2014, iss. 3 (34), pp. 218–231.