VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS

M. . Lukin


Read the full article 

Abstract

The paper deals with an interactive method of automatic verification for parallel automata-based programs. The hierarchical state machines can be implemented in different threads and can interact with each other. Verification is done by means of Spin tool and includes automatic Promela model construction, conversion of LTL-formula to Spin format and counterexamples in terms of automata. Interactive verification gives the possibility to decrease verification time and increase the maximum size of verifiable programs. Considered method supports verification of the parallel system for hierarchical automata that interact with each other through messages and shared variables. The feature of automaton model is that each state machine is considered as a new data type and can have an arbitrary bounded number of instances. Each state machine in the system can run a different state machine in a new thread or have nested state machine. This method was implemented in the developed Stater tool. Stater shows correct operation for all test cases.


Keywords: state machines, parallel automata-based programs, verification, model checking, linear temporal logic, Spin

References
1. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ:  Model Checking М.: МЦНМО, 2002. 416 с.
2. Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПб: Наука, 2011. 244 с.
3. Карпов Ю.Г. Model Checking: верификация параллельных и распределенных программных систем. СПб: БХВ-Петербург, 2010. 560
4. Официальный сайт инструментального средства http://spinroot.com, свободный. Яз. англ. (дата обращения 03.09.2013).
5. Gnesi S., Mazzanti F. On the fly model checking of communicating UML state machines. 2004 [Электрон- ный ресурс]. Режим доступа: http://fmt.isti.cnr.it/WEBPAPER/onthefly-SERA04.pdf, свободный. Яз. англ. (дата обращения 25.11.2013).
6. Gnesi S., Mazzanti F. A model checking verification environment for UML statecharts // Proc. of XLIII Congresso Annuale AICA. 2005 [Электронный ресурс]. Режим доступа: http://fmt.isti.cnr.it/~gnesi/matdid/aica.pdf, свободный. Яз. англ. (дата обращения 20.07.2013).
7. Канжелев С.Ю., Шалыто А.А. Автоматическая генерация автоматного кода // Информационно- управляющие системы. 2006. № 6 (25). С. 35–42.
8. Виноградов Р.А., Кузьмин Е.В., Соколов В.А. Верификация автоматных программ средствами CPN/Tools // Моделирование и анализ информационных систем. 2006. Т. 13. № 2. С. 4–15.
9. Васильева К.А., Кузьмин Е.В. Верификация автоматных программ с использованием LTL // Модели- рование и анализ информационных систем. 2007. Т.14. № 1. С. 3–14.
10. Лукин М.А. Верификация автоматных программ. Бакалаврская работа. СПбГУ ИТМО, 2007 [Элек- тронный ресурс]. Режим доступа: http://is.ifmo.ru/papers/_lukin_bachelor.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
11. Яминов Б.Р. Автоматизация верификации автоматных UniMod-моделей на основе инструментального средства Bogor. Бакалаврская работа. СПбГУ ИТМО, 2007 [Электронный ресурс]. Режим доступа: http://is.ifmo.ru/papers/jaminov_bachelor.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
12. Вельдер С.Э., Шалыто А.А. О верификации простых автоматных систем на основе метода Model Checking // Информационно-управляющие системы. 2007. № 3 (28). С. 27–38.
13. Ma G. Model checking support for CoreASM: model checking distributed abstract state machines using Spin. 2007 [Электронный ресурс]. Режим доступа: http://summit.sfu.ca/item/8056, свободный. Яз. англ. (дата обращения 25.11.2013).
14. David A., Möller O., Yi W. Formal Verification of UML Statecharts with Real-time Extensions // Lecture Notes in Computer Science. 2002. V.2306. P. 218–232.
15. Егоров К.В., Шалыто А.А. Методика верификации автоматных программ // Информационно- управляющие системы. 2008. № 5 (36). С. 15–21.
16. Курбацкий Е.А. Верификация программ, построенных на основе автоматного подхода с использова- нием программного средства SMV // Научно-технический вестник СПбГУ ИТМО. 2008. № 8 (53). С. 137–144.
17. Лукин М.А., Шалыто А.А. Верификация автоматных программ с использованием верификатора SPIN // Научно-технический вестник СПбГУ ИТМО. 2008. № 8 (53). С. 145–162.
18. Гуров В.С., Яминов Б.Р. Верификация автоматных программ при помощи верификатора UNIMOD.VERIFIER // Научно-технический вестник СПбГУ ИТМО. 2008. № 8 (53). С. 162–176.
19. Егоров К.В., Шалыто А.А. Разработка верификатора автоматных программ // Научно-технический вестник СПбГУ ИТМО. 2008. № 8 (53). С. 177–188.
20. Гуров В.С., Мазин М.А., Шалыто А.А. Автоматическое завершение ввода условий в диаграммах со- стояний // Информационно-управляющие системы. 2008. № 1 (32). С. 24–33.
21. Prashanth C.M., Shet K.C. Efficient Algorithms for Verification of UML Statechart Models // Journal of Software. 2009. V. 4. N 3. P. 175–182.
22. Лукин М.А. Верификация визуальных автоматных программ с использованием инструментального средства SPIN. Магистерская диссертация. СПбГУ ИТМО, 2009 [Электронный ресурс]. Режим дос- тупа: http://is.ifmo.ru/papers/_lukin_master.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
23. Тимофеев К.И., Астафуров А.А., Шалыто А.А. Наследование автоматных классов с использованием динамических языков программирования (на примере языка RUBY) // Информационно-управляющие системы. 2009. № 4 (41). С. 21–25.
24. Ремизов А.О., Шалыто А.А. Верификация автоматных программ // Сборник докладов научно- технической конференции «Состояние, проблемы и перспективы создания корабельных информаци- онно-управляющих комплексов ОАО «Концерн Моринформсистема-Агат». М., 2010. С. 90–98 [Элек- тронный ресурс]. Режим доступа: http://is.ifmo.ru/works/_2010_05_25_verific.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
25. Клебанов А.А., Степанов О.Г., Шалыто А.А. Применение шаблонов требований к формальной спе- цификации и верификации автоматных программ // Семантика, спецификация и верификация про- грамм: теория и приложения: Труды семинара. 2010. С. 124–130 [Электронный ресурс]. Режим досту- па: http://is.ifmo.ru/works/_2010-10-01_klebanov.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
26. Вельдер С.Э., Шалыто А.А. Верификация автоматных моделей методом редуцированного графа пе- реходов // Научно-технический вестник СПбГУ ИТМО. 2009. № 6 (64). С. 66–77. 27. Янкин Ю.Ю., Шалыто А.А. Автоматное программирование ПЛИС в задачах управления электропри- водом // Информационно-управляющие системы. 2011. № 1 (50). С. 50–56
Copyright 2001-2017 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика