Аннотация
В данной работе рассматриваются различные способы представления программ: от графов и логики Хоара до сетей Петри, также предложен новый способ представления программ, который заключается в записи программы в символах (переменных) и составлении зависимостей между переменными. Предлагаемый способ позволяет значительно снизить число ветвлений при анализе в программе: если при обычном анализе участка программы, в котором условный оператор находится в цикле, состоящем из n итераций, необходимо рассматривать 2n вариантов, то предлагаемый способ позволяет значительно снизить число вариантов. Одним из промежуточных результатов предлагаемого способа является система отношений между переменными, с помощью которой можно проверить выполнимость различных условий в коде программы. Результатом такой проверки является подтверждение того, что условие выполняется, или контрпример, показывающий, при каких данных условие может быть не выполнено. Предлагаемый способ был опробован на следующих примерах: с использованием условных операторов, с использованием циклов и задачи коммивояжёра. Положительный результат был получен для всех задач, за исключением последней, для которой будут выполнены дополнительные исследования.
Ключевые слова: тестирование, входные интервалы, формальная верификация, динамическая верификация, верификация, проверка моделей, модели программного обеспечения, графы
Список литературы
1. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ. Model checking. – М.: МЦНМО, 2002. – 416 с.
2. Coherent clusters in source code / S. Islam, J. Krinke, D. Binkley, M. Harman // Journal of systems and software. – 2014. – Vol. 88. – Р. 1–24.
3. Horwitz S., Reps T., Binkley D. Interprocedural slicing using dependence graphs // ACM Transactions on programming languages and systems. – 1990. – Vol. 12, iss. 1. – P. 26–60. – doi: 10.1145/77606.77608.
4. 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. – doi: 10.1145/24039.24041.
5. Шелехов В.И. Методы доказательства корректности программ с хорошей логикой [Электронный ресурс] // Международная конференция «Современные проблемы математики, информатики и биоинформатики», посвященная 100-летию со дня рождения члена-корреспондента АН СССР А.А. Ляпунова, 11–14 октября 2011 г.: доклады. – Новосибирск, 2011. – С. 1–21. – URL: http://conf.nsc.ru/files/conferences/Lyap-100/fulltext/74974/75473/Shelekhov_ prlogic.pdf (дата обращения: 31.10.2014).
6. Марков А.В., Романников Д.О. Алгоритм трансляции диаграммы активности в сеть Петри // Доклады Академии наук высшей школы Российской Федерации. – 2014. – №1 (22). – С. 104–112.
7. Воевода А.А., Марков А.В., Романников Д.О. Разработка программного обеспечения: проектирование с использованием UML диаграмм и сетей Петри на примере АСУ ТП водонапорной станции // Труды СПИИРАН. – 2014. – Вып. 3 (34). – С. 218–232.
8. Романников Д.О. Нахождение ошибок обращения к несуществующим элементам массива на основании результатов анализа сети Петри // Сборник научных трудов НГТУ. – 2012. – №1 (67). – C. 115–120.
9. Романников Д.О. О поиске входных интервалов // Сборник научных трудов НГТУ. – 2014. – № 1 (75). – С. 140–145.
10. Falk H., Marwedel P. Source code optimization techniques for data flow dominated embedded software. – New York: Springer Science: Business Media, 2004. – 226 p.
11. Глухих М.И., Ицыксон В.М., Цесько В.А. Использование зависимостей для повышения точности статического анализа программ // Моделирование и анализ информационных систем. – 2011. – Т. 18, № 4. – С. 68–79.
12. 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. – doi: 10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H.
