Аннотация
В данной статье предлагается идея нового вида сетей Петри. Выполнен обзор различ-ных подходов к представлению программ, где акцент сделан на представление про-граммы в виде модели, основанной на сети Петри и последующей ее интерпретации. Все известные авторам модели программ, основанные на представлении с использованием сетей Петри, предполагают, что их моделирование выполняется на одном, заранее заданном наборе значений переменных. Таким образом, для проверки на всем множе-стве значений переменных необходимо выполнить перебор всех возможных значений, что приводит к гигантскому росту требуемых вычислений и фактической невозможности осуществить такую проверку. В работе предлагается использовать модифицированный вид сетей Петри, где вместо обычных значений в метках сети должны быть ис-пользованы метки, содержащие символы. Причем эти символы должны однозначно соответствовать переменным из оригинальной программы. Безусловно, такой подход усложняет анализ интерпретируемой модели, но также он делает возможным анализ модели программы в сетях Петри на всем спектре значений переменных. В работе приводится процесс построения такой сети Петри на примере простой программы, в кото-рой содержатся условные операторы и операторы присваивания для небольшого количества переменных, но предлагаемые принципы построения модифицированной сети Петри могут быть применены и для больших и сложных примеров. Работа заканчивается выводами о возможностях и перспективах предлагаемой идеи, а также вариантах дальнейших исследований, к которым относятся разработка формальных алгоритмов построения сети и ее анализа.
Ключевые слова: программное обеспечение, тестирование, входные интервалы, формальная верификация, динамическая верификация, верификация, проверка моделей, модели программного обеспечения, графы, тотальная корректность программ
Список литературы
1. 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.
2. 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.
3. Coherent clusters in source code / S. Islam, J. Krinke, D. Binkley, M. Har-man // The Journal of Systems and Software. – 2014. – Vol. 88. – P. 1–24. – doi:10.1016/j.jss.2013.07.040.
4. 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.
5. 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.
6. Scholz B., Blieberger J., Fahringer T. Symbolic pointer analysis for detect-ing memory leaks // Proceedings of ACM SIGPLAN Workshop on "Partial Evalua-tion and Semantics-Based Program Manipulation" (PEPM’00), Boston, Massachu-setts, USA, January 22–23, 2000. – New York: ACM Press, 2000. – P. 104–113. – doi: 10.1145/328690.328704.
7. 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.
8. Романников Д.О. Разработка программного обеспечения с применением UML диаграмм и сетей Петри для систем управления локальным оборудова-нием: дис. … канд. техн. наук: 05.13.11 / Новосибирский государственный технический университет. – Новосибирск, 2012. – 195 с.
9. Коротиков С.В. Применение сетей Петри в разработке программного обеспечения центров дистанционного контроля и управления: дис. … канд. техн. наук: 05.13.11 / Новосибирский государственный технический универ-ситет. – Новосибирск, 2007. – 216 с.
10. Воевода А.А., Романников Д.О., Зимаев И.В. Применение UML диа-грамм и сетей Петри при разработке встраиваемого программного обеспече-ния // Научный вестник НГТУ. – 2009. – № 4 (37). – C. 169–174.
11. Коротиков С.В., Воевода А.А. Применение сетей Петри в разработке программного обеспечения центров дистанционного управления и контроля // Научный вестник НГТУ. – 2007. – № 4 (29). – C. 15–32.
12. Воевода А.А., Марков А.В. Методика автоматизированного проектиро-вания программного обеспечения функционирования сложных систем на ос-нове совместного использования UML диаграмм и сетей Петри // Современ-ные технологии. Системный анализ. Моделирование. – 2014. – № 2 (42). – С. 110–115.
13. Воевода А.А., Марков А.В., Романников Д.О. Разработка программного обеспечения: проектирование с использованием UML диаграмм и сетей Петри на примере АСУ ТП водонапорной станции // Труды СПИИРАН. – 2014. – Вып. 3 (34). – С. 218–231.
14. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking: пер. с англ. – М.: МЦНМО, 2002. – 416 с.
15. Карпов Ю.Г. Model checking. Верификация параллельных и распреде-ленных программных систем. – СПб.: БХВ-Петербург, 2010. – 560 с.
