RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2007, том 14, номер 1, страницы 31–43 (Mi mais122)  

Эта публикация цитируется в 3 научных статьях (всего в 3 статьях)

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

К. А. Васильева, Е. В. Кузьмин

Ярославский государственный университет

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

Полный текст: PDF файл (202 kB)
Список литературы: PDF файл   HTML файл
УДК: 519.68/.69
Поступила в редакцию: 17.02.2007

Образец цитирования: К. А. Васильева, Е. В. Кузьмин, “Верификация автоматных программ с использованием LTL”, Модел. и анализ информ. систем, 14:1 (2007), 31–43

Цитирование в формате AMSBIB
\RBibitem{VasKuz07}
\by К.~А.~Васильева, Е.~В.~Кузьмин
\paper Верификация автоматных программ с использованием LTL
\jour Модел. и анализ информ. систем
\yr 2007
\vol 14
\issue 1
\pages 31--43
\mathnet{http://mi.mathnet.ru/mais122}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais122
  • http://mi.mathnet.ru/rus/mais/v14/i1/p31

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles

    Эта публикация цитируется в следующих статьяx:
    1. Kuzmin E.V., Sokolov V.A., “Modeling, specification, and verification of automaton programs”, Program. Comput. Softw., 34:1 (2008), 27–43  crossref  mathscinet  zmath  isi  elib
    2. Красс А.Л., Морозов Е.А., “Автоматное программирование в медицинской аппаратуре”, Эфферентная терапия, 15:3-4 (2009), 91–96  elib
    3. Клебанов А.А., Степанов О.Г., Шалыто А.А., “Применение шаблонов требований к формальной спецификации и верификации автоматных программ”, Научно-технический вестник Санкт-Петербургского гос. ун-та информационных технологий, механики и оптики, 69:5 (2010), 91–95
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:217
    Полный текст:62
    Литература:38
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019