Аннотация
В работе приводится сравнительный анализ двух методов абстрактной интерпретации: один из них был предложен P. Cousot, второй разработан на кафедре автоматики НГТУ независимо от первого. Оба метода основываются на общей идее преобразования исходного кода программы в модель и последующего ее анализа. Оба метода предполагают исследование на всех возможных путях исполнения программы. В работе приведены примеры анализа одной и той же программы исследуемыми методами, выделены различия в исследуемых методах. В частности, метод абстрактной интерпретации предполагается использовать для автоматической проверки одного класса ошибок, для которого используется специальный домен для записи данных. Второй исследуемый метод позволяет разработчику выполнять произвольные проверки, а те ошибки, которые определялись доменом, могут быть выявлены в момент интерпретации программы. Другим отличием является то, что метод абстрактной интерпретации позволяет анализировать исходный код программ даже при их неполном представлении, несмотря на то что это негативно сказывается на точности анализа. Для второго исследуемого метода необходимо иметь полное представление исходного кода.
Ключевые слова: программное обеспечение, тестирование, входные интервалы, формальная верификация, динамическая верификация, верификация, проверка моделей, модели программного обеспечения, графы, тотальная корректность программ
Список литературы
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. –
P. 238–252.
2. Воевода А.А., Романников Д.О., Зимаев И.В. Применение UML диаг-рамм и сетей Петри при разработке встраиваемого программного обеспече-ния // Научный вестник НГТУ. – 2009. – № 4 (37). – C. 169–174.
3. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model checking. – М.: МЦНМО, 2002. – 416 с.
4. Bush W.R., Pincus J.D., Sielaff D.J. A static analyzer for finding dynamic programming errors // Software: practice and experience. – 2000. – Vol. 30, iss. 7. – P. 775–802. – doi: 10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H.
5. Глухих М.И., Ицыксон В.М., Цесько В.А. Использование зависимостей для повышения точности статического анализа программ // Моделирование и анализ информационных систем. – 2011. – Т. 18, № 4. – C. 68–79.
6. Романников Д.О. О поиске входных интервалов // Сборник научных трудов НГТУ. – 2014. – № 1 (75). – С. 140–145.
7. Coherent clusters in source code / S. Islam, J. Krinke, D. Binkley, M. Harman // Journal of systems and software. – 2014. – Vol. 88. – Р. 1–24.
8. Марков А.В., Романников Д.О. Алгоритм трансляции диаграммы активности в сеть Петри // Доклады Академии наук высшей школы Российской Федерации. – 2014. – № 1 (22). – С. 104–112.
9. Романников Д.О. Нахождение ошибок обращения к несуществующим элементам массива на основании результатов анализа сети Петри // Сборник научных трудов НГТУ. – 2012. – № 1 (67). – С. 115–120.
10. Воевода А.А., Марков А.В., Романников Д.О. Разработка программного обеспечения: проектирование с использованием UML диаграмм и сетей Петри на примере АСУ ТП водонапорной станции // Труды СПИИРАН. – 2014. – Вып. 3 (34). – С. 218–231.
Воевода Александр Александрович – доктор технических наук, профессор кафедры автоматики НГТУ. Основное направление научных исследований – управление многоканальными объектами. Имеет более 200 публикаций.
E-mail: ucit@ucit.ru
Романников Дмитрий Олегович – кандидат технических наук, старший преподаватель кафедры автоматики НГТУ. Основное направление научных исследований – формальная верификация, проверка моделей. Имеет 31 публикацию. E-mail: rom2006@gmail.com
