Menu
Publications
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Editor-in-Chief
Nikiforov
Vladimir O.
D.Sc., Prof.
Partners
VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS
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
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
