Аннотация
Данная статья посвящена анализу работы Баргсталлера, Шольца и Блибегрера по преобразованию программы в символьный домен с целью дальнейшего анализа. В данной работе приводится математический аппарат для описания программы в терминах символьного вычисления: предлагается использовать понятия контекста, состояния, условных переходов, суперконтекста и других для формульного описания программы. Приведены примеры преобразования программы в символьный домен. В работе вышеприведенных авторов основным достижением считается предложенный способ описания циклов. Данный способ позволяетполучить не только формальное представление цикла, но и свернуть потенциально бесконечное число вариантов путей программы к конечному числу. В работе рассмотрены примеры из оригинальной статьи, но все примеры достаточно простые и не содержат более 8 строк, что в конечном итоге приводит к тому, что по ним нельзя сделать вывод о применимости метода.
В ходе анализа исследуемой работы был выявлен следующий ряд недостатков: 1) метод «сворачивания» числа путей в цикле не дает заявленного результата в случае, если в цикле есть ветвление; 2) неочевидно, как будет выглядеть предлагаемое формальное описание циклов в случае вложенных циклов. Причем в циклах с большим числом вложенности должны быть зависимости по итерируемым переменным, т. е. выражения вида a[i][j] = b[i][j] или подобные; 3) отсутствует описание символьного представления для массивов,что особенно важно для перебора элементов массива в циклах в виде a[i].
Ключевые слова: программное обеспечение, тестирование, верификация, поверка моделей, символьный анализ, корректность программ, динамическая верификация, символьный фреймворк, графы, программные циклы, тотальная корректность программ
Список литературы
1. Burgstaller B., Scholz B., Blieberger J. A symbolic analysis framework for static analysis of imperative programming languages // Journal of Systems and Software. – 2012. – Vol. 85, iss. 6. – P. 1418–1439. – doi: 10.1016/j.jss.2011.11.1039.
2. Tarjan R.E. A unified approach to path problems // Journal of the ACM (JACM). – 1981. – Vol. 28, iss. 3. – P. 577–593. – doi: 10.1145/322261.322272.
3. Hecht M.S. Flow analysis of computer programs. –New York:Elsevier: North Holland, 1977. – 232p.
4. ВоеводаА.А., РоманниковД.О.Ометодеанализапрограмм // СборникнаучныхтрудовНГТУ. – 2014. – №4 (78). – C. 125–138. – doi: 10.17212/2307-6879-2014-4-125-138.
5. Воевода А.А., Романников Д.О. Способы представления программ и их анализ // Сборник научных трудов НГТУ. – 2014. – №3 (76). – C. 81–98.
6. Романников Д.О.О поиске входных интервалов // Сборник научных трудов НГТУ. – 2014. – №1 (75). – C. 140–145.
7. Abramsky S., Hankin C. An introduction to abstract interpretation[Electronic resource]. – URL: https://www.cs.virginia.edu/~weimer/2007-615/reading/AbramskiAI.pdf (accessed 20.04.2015).
8. Cousot P., Cousot R. A gentle introduction to formal verification of computer systems by abstract interpretation // Logics and Languages for Reliability and Security. – Amsterdam: IOS Press, 2010. – P. 1–29. – (NATO Science Series – D: Information and Communication Security; vol. 25). – doi: 10.3233/978-1-60750-100-8-1.
9. Глухих М.И., Ицыксон В.М., Цесько В.А.Использование зависимостей для повышения точности статического анализа программ // Моделирование и анализ информационных систем. – 2011.– Т. 18, №4. – C. 68–79.
10. 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.
11. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ. ModelChecking: пер. сангл. – М.: МЦНМО, 2002. – 416 c.
12. КарповЮ.Г.ModelChecking. Верификация параллельных и распределенных программных систем. – СПб.: БХВ-Петербург, 2010. –560 с.
13. 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.
14. Ferrante J., Ottenstein K.J., Warren J.D. The program dependence graph and its use in optimization // ACM Transactions on Programming Languages
and Systems (TOPLAS). – 1987. – Vol. 9,iss. 3. – 1987. – P. 319–349. – doi: 10.1145/24039.24041.
15. Воевода А.А., Марков А.В., Романников Д.О.Разработка программного обеспечения: проектирование с использованием UML диаграмм и сетей Петри на примере АСУ ТП водонапорной станции // Труды СПИИРАН. – 2014. – Вып. 3 (34). – C. 218–231.
16. Романников Д.О. Нахождение ошибок обращения к несуществующим элементам массива на основании результатов анализа сети Петри // Сборник научных трудов НГТУ. – 2012. – №1 (67). – C. 115–120.
17. Марков А.В., Романников Д.О. Алгоритм трансляции диаграммы активности в сеть Петри // Доклады Академии наук высшей школы Российской Федерации. – 2014. –№1 (22). – C. 104–112.
18. Воевода А.А., Романников Д.О.Редуцирование пространства состоя-ний сети Петри для объектов из одного класса// Научный вестник НГТУ. – 2011. –№4 (45). –C. 146–150.
19. Романников Д.О., Марков А.В., Зимаев И.В. Обзор работ, посвященных разработке ПО с использованием UML и сетей Петри // Сборник научных трудов НГТУ. – 2011. – №1 (63). – C. 91–104.
20. Марков А.В. Анализ отдельных частей дерева достижимости сетей Петри // Сборник научных трудов НГТУ. – 2013. – №3 (73). – C. 58–74.
21. Воевода А.А., Марков А.В.Рекурсия в сетях Петри // Сборник научных трудов НГТУ. – 2012. – №3(69). – С. 115–122.
22. Воевода А.А., Марков А.В. Тестирование UML-диаграмм с помощью аппарата сетей Петри на примере разработки по для игры "Змейка" // Сборник научных трудов НГТУ. – 2010. – №3 (61). – C. 51–60.
23. Воевода А.А., Зимаев И.В. Верификация workflow-моделей с примене-нием сетей Петри // Научный вестник НГТУ. – 2010. – № 4 (41). – C. 151–154.
24. Воевода А.А., Саркенов Д.О., Хассоунех В. Моделирование протоколов с учетом времени на цветных сетях Петри // Сборник научных трудов НГТУ. – 2004. – №3 (37). – C. 133–136.
