VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SMV TOOL
Аннотация:
We consider the method of verification of automata-based programs using Model Checking method. To verify the model the tool SMV is used. In the proposed approach, transition system is not built in explicit form. This allows the program to verify systems with large number of states.
Ключевые слова:
Постоянный URL
Статьи в номере
- ПАРАДИГМА АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
- ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ ДЛЯ ГЕНЕРАЦИИ АВТОМАТОВ С БОЛЬШИМ ЧИСЛОМ ВХОДНЫХ ПЕРЕМЕННЫХ
- СОВМЕСТНОЕ ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ, КОНЕЧНЫХ АВТОМАТОВ И ИСКУССТВЕННЫХ НЕЙРОННЫХ СЕТЕЙ ДЛЯ ПОСТРОЕНИЯ СИСТЕМЫ УПРАВЛЕНИЯ БЕСПИЛОТНЫМ ЛЕТАТЕЛЬНЫМ АППАРАТОМ
- ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ И МЕТОДОВ СОКРАЩЕННЫХ ТАБЛИЦ ПЕРЕХОДОВ И ДЕРЕВЬЕВ РЕШЕНИЙ ДЛЯ ПОСТРОЕНИЯ АВТОМАТОВ УПРАВЛЕНИЯ МОДЕЛЬЮ БЕСПИЛОТНОГО ЛЕТАТЕЛЬНОГО АППАРАТА
- ПОСТРОЕНИЕ АВТОПИЛОТА ДЛЯ УПРОЩЕННОЙ МОДЕЛИ ВЕРТОЛЕТА С ПОМОЩЬЮ ГЕНЕТИЧЕСКОГО АЛГОРИТМА
- СОЗДАНИЕ СИСТЕМЫ УПРАВЛЕНИЯ ТАНКОМ ДЛЯ ИГРЫ ROBOCODE С ИСПОЛЬЗОВАНИЕМ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ
- РАЗРАБОТКА ИНСТРУМЕНТАЛЬНОГО СРЕДСТВА ДЛЯ ГЕНЕРАЦИИ КОНЕЧНЫХ АВТОМАТОВ С ИСПОЛЬЗОВАНИЕМ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ
- МЕТОД ПРЕДСТАВЛЕНИЯ АВТОМАТОВ ДЕРЕВЬЯМИ РЕШЕНИЙ ДЛЯ ИСПОЛЬЗОВАНИЯ В ГЕНЕТИЧЕСКОМ ПРОГРАММИРОВАНИИ
- ПРИМЕНИЕ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ ДЛЯ ПОСТРОЕНИЯ АВТОМАТОВ МУРА И СИСТЕМ ВЗАИМОДЕЙСТВУЮЩИХ АВТОМАТОВ МИЛИ НА ПРИМЕРЕ ЗАДАЧИ ОБ «УМНОМ МУРАВЬЕ»
- МЕТОДЫ ОПТИМИЗАЦИИ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ ДЛЯ ПОСТРОЕНИЯ КОНЕЧНЫХ АВТОМАТОВ
- МЕТОДЫ ВЕРИФИКАЦИИ МОДЕЛЕЙ АВТОМАТНЫХ ПРОГРАММ
- ВЕРИФИКАЦИЯ ПРОГРАММ, ПОСТРОЕННЫХ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА С ИСПОЛЬЗОВАНИЕМ ПРОГРАММНОГО СРЕДСТВА SMV
- ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ ВЕРИФИКАТОРА SPIN
- ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ ПРИ ПОМОЩИ ВЕРИФИКАТОРА UNIMOD.VERIFIER
- РАЗРАБОТКА ВЕРИФИКАТОРА АВТОМАТНЫХ ПРОГРАММ
- ПРИМЕНЕНИЕ АВТОМАТНОГО ПОДХОДА ДЛЯ СОЗДАНИЯ КОРРЕКТНЫХ JAVA CARD-ПРИЛОЖЕНИЙ
- РАЗРАБОТКА КОРРЕКТНЫХ JAVA CARD-ПРОГРАММ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА
- ВЕРИФИКАЦИИ ВЗАИМОДЕЙСТВИЯ ЧАСТЕЙ РЕАКТИВНОЙ СИСТЕМЫ, РЕАЛИЗОВАННЫХ С ПОМОЩЬЮ АВТОМАТНОГО ПОДХОДА
- МЕТОД АВТОМАТИЧЕСКОЙ ДИНАМИЧЕСКОЙ ВЕРИФИКАЦИИ АВТОМАТНЫХ ПРОГРАММ
- ДЕКЛАРАТИВНЫЙ ПОДХОД К ВЛОЖЕНИЮ И НАСЛЕДОВАНИЮ АВТОМАТНЫХ КЛАССОВ ПРИ ИСПОЛЬЗОВАНИИ ИМПЕРАТИВНЫХ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ
- НАСЛЕДОВАНИЕ АВТОМАТНЫХ КЛАССОВ С ИСПОЛЬЗОВАНИЕМ ДИНАМИЧЕСКИХ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ НА ПРИМЕРЕ RUBY
- ИНСТРУМЕНТАЛЬНОЕ СРЕДСТВО ДЛЯ ПОДДЕРЖКИ АВТОМАТНОГО ПРОГРАММИРОВАНИЯ UNIMOD 2. ПРОЕКТИРОВАНИЕ. ВАЛИДАЦИЯ. ВЕРИФИКАЦИЯ. РЕАЛИЗАЦИЯ
- ТЕКСТОВЫЙ ЯЗЫК АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
- ТЕКСТОВЫЙ ЯЗЫК АВТОМАТНОГО ПРОГРАММИРОВАНИЯ FSML ДЛЯ ИНСТРУМЕНТАЛЬНОГО СРЕДСТВА UNIMOD
- МЕТОД РАЗРАБОТКИ ТЕСТОВ ДЛЯ ПРОГРАММНЫХ ИНТЕРФЕЙСОВ ПРИЛОЖЕНИЙ НА ОСНОВЕ КОНЕЧНО-АВТОМАТНОЙ МОДЕЛИ ТЕСТИРОВАНИЯ
- ПОСТРОЕНИЕ СИСТЕМЫ АВТОМАТИЧЕСКОГО УПРАВЛЕНИЯ МОБИЛЬНЫМ РОБОТОМ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА
- ПРИМЕНЕНИЕ КОНЕЧНЫХ АВТОМАТОВ В ДОКУМЕНТООБОРОТЕ
- МЕТОД ОБУЧЕНИЯ СЛОЖНЫХ СИСТЕМ С БОЛЬШИМ ЧИСЛОМ ВХОДНЫХ ДАННЫХ И ВЫХОДНЫХ ВОЗДЕЙСТВИЙ