Аннотация
Данная работа посвящена разбору метода анализа программного обеспечения, основанного на принципе выявления всех возможных значений переменных и нахождения при помощи этого ошибок путем проверки верифицируемых формул на всех возможных значениях переменных. В работе рассмотрены примеры, на которых показаны основные принципы предлагаемого метода анализа ПО, а именно: пример программы с циклом, который показывает, каким образом можно выполнить сворачивание полного графа к «линейным» участкам программы, а затем выполнить их анализ. Вторым принципом рассматриваемого метода является анализ ПО «линейно», т. е. постепенный анализ каждой ветки программы. При этом отдельный анализ можно выполнять с места ветвления без необходимости выполнения полного анализа сначала. В работе приведены многочисленные примеры того, как необходимо выполнить разбиение основной программы на ветки. Главной особенностью такого разбиения является сохранение малого количества ветвлений. Приведена формальная семантика описания программы, предложенная П. Коусотом и используемая для формализованного описания алгоритмов анализа ПО. Исходная семантика была упрощена в части описания узлов графа – убраны лишние узлы, так как они не актуальны после преобразования графа, и расширена функция поиска возможных значений переменных после исполнения оператора. Также показано, каким обзором можно определить функцию поиска возможных вариантов переменных для бинарных и унарных операций путем ее определения для операций умножения и логического отрицания. Для остальных операций данная функция может быть легко построена по аналогии.
Ключевые слова: программное обеспечение, тестирование, входные интервалы, формальная верификация, динамическая верификация, верификация, проверка моделей, модели программного обеспечения, графы, тотальная корректность программ
Список литературы
1. Воевода А.А., Романников Д.О. Способы представления программ и их анализ // Сборник научных трудов НГТУ. – 2014. – № 3 (76). – С. 81–98.
2. Романников Д.О. О поиске входных интервалов // Сборник научных трудов НГТУ. – 2014. – № 1 (75). – С. 140–145.
3. Abramsky S., Hankin C. An introduction to abstract interpretation. – URL: https://www.cs.virginia.edu/~weimer/2007-615/reading/AbramskiAI.pdf (accessed 20.12.2014).
4. Cousot P., Cousot R. A gentle introduction to formal verification of computer systems by abstract interpretation // Logics and Languages for Reliability and Security. NATO Science Series III: Computer and Systems Sciences. – Amsterdam: IOS Press, 2010. – P. 1–29.
5. Глухих М.И., Ицыксон В.М., Цесько В.А. Использование зависимостей для повышения точности статического анализа программ // Моделирование и анализ информационных систем. – 2011. – Т. 18, № 4. – С. 68–79.
6. Bush W., Pincus J., Sielaff D. A static analyzer for finding dynamic programming errors // Software: Practice and Experience. – 2000. – Vol. 30,
iss. 7. – P. 775–802.
7. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. – М.: МЦНМО, 2002. – 416 с.
8. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. – СПб.: БХВ-Петербург, 2010. – 560 с.
9. Horwitz S., Reps T., Binkley D. Interprocedural slicing using dependence graphs // ACM Transactions on Programming Languages and Systems. – 1990. – Vol. 1, iss. 12. – P. 26–60.
10. Ferrante J., Ottenstein K.J., Warren J.D. The program dependence graph and its use in optimization // ACM Transactions on Programming Languages and Systems. – 1987. – Vol. 9, iss. 3. – P. 319–349.
11. Воевода А.А., Марков А.В., Романников Д.О. Разработка программного обеспечения: проектирование с использованием UML диаграмм и сетей Петри на примере АСУ ТП водонапорной станции // Труды СПИИРАН. – 2014. – Вып. 3 (34). – С. 218–232.
12. Романников Д.О. Нахождение ошибок обращения к несуществующим элементам массива на основании результатов анализа сети Петри // Сборник научных трудов НГТУ. – 2012. – № 1 (67). – C. 115–120.
13. Марков А.В., Романников Д.О. Алгоритм трансляции диаграммы активности в сеть Петри // Доклады Академии наук высшей школы Российской Федерации. – 2014. – № 1 (22). – С. 104–112.
14. Воевода А.А., Романников Д.О. Редуцирование пространства состояний сети Петри для объектов из одного класса // Научный вестник НГТУ. – 2011. – № 4 (45). – С. 146–150.
15. Романников Д.О., Марков А.В., Зимаев И.В. Обзор работ, посвященных разработке ПО с использованием UML и сетей Петри // Сборник научных трудов НГТУ. – 2011. – № 1 (63). – С. 91–104.
16. Марков А.В. Анализ отдельных частей дерева достижимости сетей Петри // Сборник научных трудов НГТУ. – 2013. – № 3 (73). – С. 58–74.
17. Воевода А.А., Марков А.В. Рекурсия в сетях Петри // Сборник научных трудов НГТУ. – 2012. – № 3 (69). – С. 115–122.
18. Воевода А.А., Марков А.В. Тестирование UML-диаграмм с помощью аппарата сетей Петри на примере разработки по для игры «Змейка» // Сборник научных трудов НГТУ. – 2010. – № 3 (61). – C. 51–60.
19. Воевода А.А., Зимаев И.В. Верификация workflow-моделей с примене-нием сетей Петри // Научный вестник НГТУ. – 2010. – № 4 (41). – C. 151–154.
20. Воевода А.А., Саркенов Д.О., Хассоунех В. Моделирование протоколов с учетом времени на цветных сетях Петри // Сборник научных трудов НГТУ. – 2004. – № 3 (37). – C. 133–136.
