Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:004.4’242
Номер:8 (53)
Скачать PDF0 Кбайт
ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ ВЕРИФИКАТОРА SPIN
Аннотация:
Рассматривается способ использования верификатора SPIN для верификации автоматных программ. При использовании этого верификатора модель описывается на языке Promela, а требования – на языке LTL. В работе предлагается метод автоматизированного преобразования автоматных программ в модели на языке Promela. Для преобразования формулы на языке LTL в вид, пригодный для использования верификатором, разработано специальное программное средство. Использование предлагаемого метода иллюстрируется на примере верификации модели банкомата.
Ключевые слова:
Постоянный URL
Статьи в номере
- ПАРАДИГМА АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
- ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ ДЛЯ ГЕНЕРАЦИИ АВТОМАТОВ С БОЛЬШИМ ЧИСЛОМ ВХОДНЫХ ПЕРЕМЕННЫХ
- СОВМЕСТНОЕ ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ, КОНЕЧНЫХ АВТОМАТОВ И ИСКУССТВЕННЫХ НЕЙРОННЫХ СЕТЕЙ ДЛЯ ПОСТРОЕНИЯ СИСТЕМЫ УПРАВЛЕНИЯ БЕСПИЛОТНЫМ ЛЕТАТЕЛЬНЫМ АППАРАТОМ
- ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ И МЕТОДОВ СОКРАЩЕННЫХ ТАБЛИЦ ПЕРЕХОДОВ И ДЕРЕВЬЕВ РЕШЕНИЙ ДЛЯ ПОСТРОЕНИЯ АВТОМАТОВ УПРАВЛЕНИЯ МОДЕЛЬЮ БЕСПИЛОТНОГО ЛЕТАТЕЛЬНОГО АППАРАТА
- ПОСТРОЕНИЕ АВТОПИЛОТА ДЛЯ УПРОЩЕННОЙ МОДЕЛИ ВЕРТОЛЕТА С ПОМОЩЬЮ ГЕНЕТИЧЕСКОГО АЛГОРИТМА
- СОЗДАНИЕ СИСТЕМЫ УПРАВЛЕНИЯ ТАНКОМ ДЛЯ ИГРЫ ROBOCODE С ИСПОЛЬЗОВАНИЕМ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ
- РАЗРАБОТКА ИНСТРУМЕНТАЛЬНОГО СРЕДСТВА ДЛЯ ГЕНЕРАЦИИ КОНЕЧНЫХ АВТОМАТОВ С ИСПОЛЬЗОВАНИЕМ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ
- МЕТОД ПРЕДСТАВЛЕНИЯ АВТОМАТОВ ДЕРЕВЬЯМИ РЕШЕНИЙ ДЛЯ ИСПОЛЬЗОВАНИЯ В ГЕНЕТИЧЕСКОМ ПРОГРАММИРОВАНИИ
- ПРИМЕНИЕ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ ДЛЯ ПОСТРОЕНИЯ АВТОМАТОВ МУРА И СИСТЕМ ВЗАИМОДЕЙСТВУЮЩИХ АВТОМАТОВ МИЛИ НА ПРИМЕРЕ ЗАДАЧИ ОБ «УМНОМ МУРАВЬЕ»
- МЕТОДЫ ОПТИМИЗАЦИИ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ ДЛЯ ПОСТРОЕНИЯ КОНЕЧНЫХ АВТОМАТОВ
- МЕТОДЫ ВЕРИФИКАЦИИ МОДЕЛЕЙ АВТОМАТНЫХ ПРОГРАММ
- ВЕРИФИКАЦИЯ ПРОГРАММ, ПОСТРОЕННЫХ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА С ИСПОЛЬЗОВАНИЕМ ПРОГРАММНОГО СРЕДСТВА SMV
- ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ ПРИ ПОМОЩИ ВЕРИФИКАТОРА UNIMOD.VERIFIER
- РАЗРАБОТКА ВЕРИФИКАТОРА АВТОМАТНЫХ ПРОГРАММ
- ПРИМЕНЕНИЕ АВТОМАТНОГО ПОДХОДА ДЛЯ СОЗДАНИЯ КОРРЕКТНЫХ JAVA CARD-ПРИЛОЖЕНИЙ
- РАЗРАБОТКА КОРРЕКТНЫХ JAVA CARD-ПРОГРАММ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА
- ВЕРИФИКАЦИИ ВЗАИМОДЕЙСТВИЯ ЧАСТЕЙ РЕАКТИВНОЙ СИСТЕМЫ, РЕАЛИЗОВАННЫХ С ПОМОЩЬЮ АВТОМАТНОГО ПОДХОДА
- МЕТОД АВТОМАТИЧЕСКОЙ ДИНАМИЧЕСКОЙ ВЕРИФИКАЦИИ АВТОМАТНЫХ ПРОГРАММ
- ДЕКЛАРАТИВНЫЙ ПОДХОД К ВЛОЖЕНИЮ И НАСЛЕДОВАНИЮ АВТОМАТНЫХ КЛАССОВ ПРИ ИСПОЛЬЗОВАНИИ ИМПЕРАТИВНЫХ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ
- НАСЛЕДОВАНИЕ АВТОМАТНЫХ КЛАССОВ С ИСПОЛЬЗОВАНИЕМ ДИНАМИЧЕСКИХ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ НА ПРИМЕРЕ RUBY
- ИНСТРУМЕНТАЛЬНОЕ СРЕДСТВО ДЛЯ ПОДДЕРЖКИ АВТОМАТНОГО ПРОГРАММИРОВАНИЯ UNIMOD 2. ПРОЕКТИРОВАНИЕ. ВАЛИДАЦИЯ. ВЕРИФИКАЦИЯ. РЕАЛИЗАЦИЯ
- ТЕКСТОВЫЙ ЯЗЫК АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
- ТЕКСТОВЫЙ ЯЗЫК АВТОМАТНОГО ПРОГРАММИРОВАНИЯ FSML ДЛЯ ИНСТРУМЕНТАЛЬНОГО СРЕДСТВА UNIMOD
- МЕТОД РАЗРАБОТКИ ТЕСТОВ ДЛЯ ПРОГРАММНЫХ ИНТЕРФЕЙСОВ ПРИЛОЖЕНИЙ НА ОСНОВЕ КОНЕЧНО-АВТОМАТНОЙ МОДЕЛИ ТЕСТИРОВАНИЯ
- ПОСТРОЕНИЕ СИСТЕМЫ АВТОМАТИЧЕСКОГО УПРАВЛЕНИЯ МОБИЛЬНЫМ РОБОТОМ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА
- ПРИМЕНЕНИЕ КОНЕЧНЫХ АВТОМАТОВ В ДОКУМЕНТООБОРОТЕ
- МЕТОД ОБУЧЕНИЯ СЛОЖНЫХ СИСТЕМ С БОЛЬШИМ ЧИСЛОМ ВХОДНЫХ ДАННЫХ И ВЫХОДНЫХ ВОЗДЕЙСТВИЙ