Аннотация
Существенным недостатком способов анализа программного обеспечения (ПО), основанных на переборе всех возможных начальных вариантов, является «взрывной» рост числа вариантов анализа (в различных методах этот термин называется по-разному: в проверке моделей – размер тотального множества переходов, в сетях Петри – пространство состояний и т. д.), который приводит к невозможности анализа ПО. Одним из основных источников значительного увеличения числа вариантов для анализа являются конструкции с програм-мными циклами, особенно содержащие условные операторы внутри цикла. Потенциально такие циклы могут приводить к фактически бесконечному числу вариантов для анализа. В работе предлагается метод упрощения анализа ПО, который предполагает преобразование выражений в циклах с целью уменьшения количества вариантов анализа (сокращение размера тотального множества переходов или поиск идентичных участков пространства состояний). Рассматриваемый способ основывается на представлении выражений в цикле в виде функции, зависящей от числа итераций. При этом выражения в цикле преобразовываются в нерекуррентные соотношения, а анализ ПО сводится к решению набора систем нелинейных уравнений или к другим видам анализа полученных выражений. Необходимо заметить, что анализ полученных функций также является достаточно сложной задачей, но ее решение авторам кажется более перспективным, чем решения, основанные на полном переборе. В работе приводятся примеры применения данного метода для преобразования выражений в цикле к функциям от числа итераций, а также примеры анализа программ с помощью анализа полученных функций.
Ключевые слова: программное обеспечение, цепи рекуррентности, рекуррентные соотношения, проверка моделей, сети Петри, пространство состояний, программные циклы, символьный анализ, граф состояния, пространство переходов
Список литературы
1. Орлов С.А. Технология разработки программного обеспечения. – СПб.: Питер, 2012. – 609 с.
2. Романников Д.О. Разработка программного обеспечения с применением UML диаграмм и сетей Петри для систем управления локальным оборудованием: дис. … канд. техн. наук. – Новосибирск, 2012. – 195 с.
3. Коротиков С.В. Применение сетей Петри в разработке программного обеспечения центров дистанционного контроля и управления: дис. … канд. техн. наук. – Новосибирск, 2007. – 216 с.
4. Марков А.В. Автоматизация проектирования и анализа программного обеспечения с использованием языка UML и сетей Петри: дис. … канд. техн. наук. – Новосибирск, 2015. – 176 с.
5. Clarke E.M., Grumberg O., Peled D. Model checking. – Cambridge: MIT Press, 1999. – 330 p.
6. Карпов Ю.Г. Model checking. Верификация параллельных и распределенных программных систем. – СПб.: БХВ-Петербург, 2010. – 560 с.
7. Воевода А.А., Романников Д.О. Сравнение методов преобразования программного цикла с использованием символьной нотации // Сборник научных трудов НГТУ. – 2015. – № 1 (79). – С. 65–76.
8. Engelen R.A. van The CR# algebra and its application in loop analysis and optimization: technical report TR-041223 / Florida State University. – Florida, 2004. – 13 p.
9. Scholz B., Blieberger J., Fahringer T. Symbolic pointer analysis for detecting memory leaks // Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation (PEPM'00). – New York, 1999. – P. 104–113.
10. Burgstaller V., Scholz V., Blieberger V. A symbolic analysis framework for static analysis of imperative programming languages // Journal of Systems and Software. – 2012. – Vol. 85, iss. 6. – P. 1418–1439.
11. A unified framework for nonlinear dependence testing and symbolic analysis / R.A. van Engelen , J. Birch, Y. Shou, B. Walsh, K.A. Gallivan // Supercomputing: Proceedings of the 18th Annual International Conference, (ICS'04), 2004. – New York, 2004. – P. 106–115.
12. Воевода А.А., Романников Д.О. Символьные метки в сетях Петри при анализе программ // Сборник научных трудов НГТУ. – 2015. – № 2 (80). – С. 80–86.
13. Cousot V., Cousot R. A gentle introduction to formal verification of computer systems by abstract interpretation // Logics and Languages for Reliability and Security / J. Esparza, O. Grumberg, M. Broy, eds. – Washington: IOS Press, 2010. – P. 1–29. – (NATO science for peace and security series. Sub-series D. Information and communication security; vol. 25).
14. Bachmann O., Wang P.S., Zima E.V. Chains of recurrences – a method to expedite the evaluation of closed-form functions // Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC'94, Oxford, England, UK, 20–22 July 1994. – New York: ASM, 1994. – P. 242–249.
15. Kislenkov V., Mitrofanov V., Zima E. Multidimensional chains of recurrences // Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation, ISSAC'98, Rostock, Germany, 13–15 August 1998. – New York: ASM, 1998. – P. 199–206.
16. Bachmann O. Chains of recurrences: PhD diss. of philosophy / Kent State University. – Kent, 1996. – 145 p.
