Аннотация
Современные технические системы – это, возможно, одни из самых сложных технических систем во всей человеческой деятельности. На сегодняшний день такие системы чаще всего состоят из интеграции программной и аппаратной частей. При этом рост сложности самой системы приводит к значительному увеличению сложности разработки и контроля за качеством программной системы. На сегодняшний день в индустрии разработки программного обеспечения нет формальных средств, которые могли бы гарантировать отсутствие программных ошибок. Большое влияние на сложность программного анализа оказывает значительное увеличение программных путей, в особенности из-за наличия условных операторов в циклах. В данной статье рассматривается подход уменьшения количества программных путей, который основан на символьной нотации. Согласно данному подходу программный цикл должен быть представлен как символьное выражение, которое определяет переменные ив котором условные операторы представлены в виде дополнительных переменных. После этого программа должна быть представлена в виде дерева с вершинами в виде контекстов. Далее полученное дерево контекстов может быть проанализировано в любом состоянии путем вычисления выражения, в котором содержатся возможные значения переменных вместо их символьного представления. Статья завершается формулированием общего алгоритма анализа программы. Задача получения формального алгоритма преобразования цикла является темой отдельного исследования и будет рассмотрена в последующих работах, также как и представление математического аппарата для вычисления возможных значений символьных выражений при подстановке в него возможных значений переменных.
Ключевые слова: программное обеспечение, тестирование, входные интервалы, формальная верификация, динамическая верификация, верификация, проверка моделей, модели программного обеспечения, графы, тотальная корректность программ
Список литературы
1. Орлов С.А., ЦилькерБ.Я.Технологии разработки программного обес-печения: современный курс по программной инженерии. –4-е изд. – СПб.: Питер, 2012. – 608с. – (Учебник для вузов) (Стандарт третьего поколения).
2. Верификация автоматных программ / С.Э. Вельдер, М.А. Лукин, А.А. Шалыто, Б.Р. Яминов; Санкт-Петербургский государственный универси-тет информационных технологий, механики и оптики. –СПб.: Изд-во СПбГУ ИТМО, 2011. – 242 с.
3. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. – М.: МЦНМО, 2002. – 416 с.
4. КарповЮ.Г. Modelchecking. Верификация параллельных и распреде-ленных программных систем. – СПб.: БХВ-Петербург, 2010. – 560 с.
5. Bush W., Pincus J., Sielaff D. A static analyzer for finding dynamic prog-ramming 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.
6. Falk H., Marwedel P. Source code optimization techniques for data flow dominated embedded software. – New York: Springer Science; Business Media, 2004. –226 p.–doi: 10.1007/978-1-4020-2829-8.
7. Cousot P., Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints // POPL'77: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Los Angeles, California, January, 17–19, 1977. – New York: ACMPress, 1977. – P. 238–252.–doi: 10.1145/512950.512973.
8. Coherent clusters in source code / S.Islam, J.Krinke, D.Binkley, M. Ha-rman // The Journal of Systems and Software.– 2014. – Vol. 88. – P. 1–24.–doi:10.1016/j.jss.2013.07.040.
9. Horwitz S., Reps T., Binkley D. Interprocedural slicing using dependence graphs //ACM Transactions on Programming Languages and Systems(TOPLAS). – 1990. –Vol. 12, iss. 1. – P. 26–60.–doi: 10.1145/77606.77608.
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(TOPLAS). – 1987. –Vol.9, iss. 3. – P. 319–349.– doi: 10.1145/24039.24041.
11. Handbook of automated reasoning / J.A.Robinson, A.Voronkov, eds.– Amsterdam: Elsevir Science; Cambridge: The Mit Press, 2001. – 2150 p.
12. Scholz B., Blieberger J., Fahringer T. Symbolic pointer analysis for detecting memory leaks // Proceedings of ACM SIGPLAN Workshop on "Partial Evaluation and Semantics-Based Program Manipulation" (PEPM’00), Boston, Massachusetts, USA, January 22–23, 2000.– New York: ACM Press, 2000. – P. 104–113. – doi: 10.1145/328690.328704.
13. Rugina R., Rinard M. Symbolic bounds analysis of pointers, array indices, and accessed memory regions // PLDI'00: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, Vancouver, Canada, June 18–21, 2000. – New York: ACM Press, 2000. – P. 182–195.– doi: 10.1145/358438.349325.
14. 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.–10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H.
15. Combining symbolic execution with model checking to verify parallel numerical programs / S.F.Siegel, A.Mironova, G.S.Avrunin, L.A. Clarke // ACM Transactions on Software Engineering and Methodology.– 2008. – Vol. 17,
iss. 2. – P. 10:1–10:34.– doi: 10.1145/1348250.1348256.
16. Burgstaller B., Scholz B., Blieberger J. A symbolic analysis framework for static analysis of imperative programming languages // The Journal of Systems and Software. – 2014. – Vol. 85, iss. 6. – P. 1418–1439. – doi:10.1016/j.jss.2011.11.1039.
17. Fahringer T., Scholz B. Advanced symbolic analysis for compilers. –Berlin; Heidelberg: Springer-Verlag,2003. – 136 p.– (Lecture Notes in Computer Science; vol. 2628).– doi: 10.1007/3-540-36614-8.
18. Burgstaller B. Symbolic evaluation of imperative programming languages: technical report N 183/1-138 / Vienna University of Technology, Department of Avtomation.– Vienna, 2005.– 146 p.
19. Воевода А.А., Романников Д.О. Способы представления программ и их анализ // Сборник научных трудов НГТУ. – 2014. – № 3 (77). – C. 81–99.
