Верификация автоматных программ с использованием LTL


https://doi.org/10.18255/1818-1015-2007-1-31-43

Полный текст:


Аннотация

Рассматривается один из способов моделирования, спецификации и верификации программ, построенных на основе автоматного подхода к программированию. Технология автоматного программирования является достаточно эффективной при создании программного обеспечения для «реактивных» систем и систем логического управления. С точки зрения моделирования и анализа программных систем эта технология имеет ряд преимуществ по сравнению с традиционным подходом, так как исключает проблему адекватности построенной программной модели исходной программе. Набор взаимодействующих автоматов, описывающий логику программы, уже является адекватной моделью, по которой формальным образом строится программный модуль. Свойства программной системы в виде автоматов могут быть сформулированы и специфицированы естественным и понятным образом. Проверка свойств осуществляется в терминах, которые естественно вытекают из автоматной модели программы. Практическим результатом работы является применение инструментального средства SPIN и логики LTL для спецификации и верификации иерархических автоматных программ.

Об авторах

К. А. Васильева
Ярославский государственный университет
Россия


Е. В. Кузьмин
Ярославский государственный университет
Россия


Список литературы

1. Шалыто, А. А. Switch-технология. Алгоритмизация и программирование задач логического управления / А. А. Шалыто. - СПб.: Наука, 1998. - 628 с. (http://is.ifmo.ru/books/switch/1/).

2. Шалыто, А. А. Автоматное проектирование программ. Алгоритмизация и программирование задач логического управления / А. А. Шалыто // Известия Академии наук. Теория и системы управления. - 2000. - №6. - С. 63-81. (http://is.ifmo.ru, «Статьи»).

3. Шалыто, А. А. Алгоритмизация и программирование для задач логического управления и «реак¬тивных» систем / А. А. Шалыто // Автоматика и телемеханика. Обзоры. - 2001. - №1. - С. 3-39. (http://is.ifmo.ru, «Статьи»).

4. Шалыто, А. А. SWITCH-технология - автоматный подход к созданию программного обеспечения «реактивных» систем / А. А. Шалыто, Н. И. Туккель // Программирование. - 2001. - №5. - С. 45-62. (http://is.ifmo.ru/works/switch/1/).

5. Кузьмин, Е. В. Иерархическая модель автоматных программ / Е. В. Кузьмин // Моделирование и анализ информационных систем. - 2006. - Т. 13 (1). - С. 27-34.

6. Кларк, Э. М. Верификация моделей программ: Model Checking / Э. М. Кларк, О. Грамберг, Д. Пелед. - МЦНМО, 2002. - 416 с.

7. Кузьмин, Е. В. Структурированные системы переходов / Е.В. Кузьмин, В. А. Соколов. - М.: ФИЗ- МАТЛИТ, 2006. - 178 с.

8. Первушин, Е. В. Моделирование банкомата / Е. В. Первушин, А. А. Шалыто // СПбГУ ИТМО, 2003. http://is.ifmo.ru/projects/.

9. SPIN. http://spinroot.com/spin/whatispin.html.


Дополнительные файлы

Для цитирования: Васильева К.А., Кузьмин Е.В. Верификация автоматных программ с использованием LTL. Моделирование и анализ информационных систем. 2007;14(1):31-43. https://doi.org/10.18255/1818-1015-2007-1-31-43

For citation: Vasileva K.A., Kuzmin E.V. LTL Verification of Automaton Programs. Modeling and Analysis of Information Systems. 2007;14(1):31-43. (In Russ.) https://doi.org/10.18255/1818-1015-2007-1-31-43

Просмотров: 6

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)