METHODS OF AUTOMATA-BASED PROGRAMS VERIFICATION
Аннотация:
This article discusses ways of converting automata-based programs to Kripke models, designed to check the properties related to the behavior of the system. These properties are described with temporal logic formulas. Several methods of such a transformation are proposed.
Ключевые слова:
Постоянный URL
Статьи в номере
- ПАРАДИГМА АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
- ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ ДЛЯ ГЕНЕРАЦИИ АВТОМАТОВ С БОЛЬШИМ ЧИСЛОМ ВХОДНЫХ ПЕРЕМЕННЫХ
- СОВМЕСТНОЕ ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ, КОНЕЧНЫХ АВТОМАТОВ И ИСКУССТВЕННЫХ НЕЙРОННЫХ СЕТЕЙ ДЛЯ ПОСТРОЕНИЯ СИСТЕМЫ УПРАВЛЕНИЯ БЕСПИЛОТНЫМ ЛЕТАТЕЛЬНЫМ АППАРАТОМ
- ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ И МЕТОДОВ СОКРАЩЕННЫХ ТАБЛИЦ ПЕРЕХОДОВ И ДЕРЕВЬЕВ РЕШЕНИЙ ДЛЯ ПОСТРОЕНИЯ АВТОМАТОВ УПРАВЛЕНИЯ МОДЕЛЬЮ БЕСПИЛОТНОГО ЛЕТАТЕЛЬНОГО АППАРАТА
- ПОСТРОЕНИЕ АВТОПИЛОТА ДЛЯ УПРОЩЕННОЙ МОДЕЛИ ВЕРТОЛЕТА С ПОМОЩЬЮ ГЕНЕТИЧЕСКОГО АЛГОРИТМА
- СОЗДАНИЕ СИСТЕМЫ УПРАВЛЕНИЯ ТАНКОМ ДЛЯ ИГРЫ ROBOCODE С ИСПОЛЬЗОВАНИЕМ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ
- РАЗРАБОТКА ИНСТРУМЕНТАЛЬНОГО СРЕДСТВА ДЛЯ ГЕНЕРАЦИИ КОНЕЧНЫХ АВТОМАТОВ С ИСПОЛЬЗОВАНИЕМ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ
- МЕТОД ПРЕДСТАВЛЕНИЯ АВТОМАТОВ ДЕРЕВЬЯМИ РЕШЕНИЙ ДЛЯ ИСПОЛЬЗОВАНИЯ В ГЕНЕТИЧЕСКОМ ПРОГРАММИРОВАНИИ
- ПРИМЕНИЕ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ ДЛЯ ПОСТРОЕНИЯ АВТОМАТОВ МУРА И СИСТЕМ ВЗАИМОДЕЙСТВУЮЩИХ АВТОМАТОВ МИЛИ НА ПРИМЕРЕ ЗАДАЧИ ОБ «УМНОМ МУРАВЬЕ»
- МЕТОДЫ ОПТИМИЗАЦИИ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ ДЛЯ ПОСТРОЕНИЯ КОНЕЧНЫХ АВТОМАТОВ
- МЕТОДЫ ВЕРИФИКАЦИИ МОДЕЛЕЙ АВТОМАТНЫХ ПРОГРАММ
- ВЕРИФИКАЦИЯ ПРОГРАММ, ПОСТРОЕННЫХ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА С ИСПОЛЬЗОВАНИЕМ ПРОГРАММНОГО СРЕДСТВА SMV
- ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ ВЕРИФИКАТОРА SPIN
- ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ ПРИ ПОМОЩИ ВЕРИФИКАТОРА UNIMOD.VERIFIER
- РАЗРАБОТКА ВЕРИФИКАТОРА АВТОМАТНЫХ ПРОГРАММ
- ПРИМЕНЕНИЕ АВТОМАТНОГО ПОДХОДА ДЛЯ СОЗДАНИЯ КОРРЕКТНЫХ JAVA CARD-ПРИЛОЖЕНИЙ
- РАЗРАБОТКА КОРРЕКТНЫХ JAVA CARD-ПРОГРАММ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА
- ВЕРИФИКАЦИИ ВЗАИМОДЕЙСТВИЯ ЧАСТЕЙ РЕАКТИВНОЙ СИСТЕМЫ, РЕАЛИЗОВАННЫХ С ПОМОЩЬЮ АВТОМАТНОГО ПОДХОДА
- МЕТОД АВТОМАТИЧЕСКОЙ ДИНАМИЧЕСКОЙ ВЕРИФИКАЦИИ АВТОМАТНЫХ ПРОГРАММ
- ДЕКЛАРАТИВНЫЙ ПОДХОД К ВЛОЖЕНИЮ И НАСЛЕДОВАНИЮ АВТОМАТНЫХ КЛАССОВ ПРИ ИСПОЛЬЗОВАНИИ ИМПЕРАТИВНЫХ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ
- НАСЛЕДОВАНИЕ АВТОМАТНЫХ КЛАССОВ С ИСПОЛЬЗОВАНИЕМ ДИНАМИЧЕСКИХ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ НА ПРИМЕРЕ RUBY
- ИНСТРУМЕНТАЛЬНОЕ СРЕДСТВО ДЛЯ ПОДДЕРЖКИ АВТОМАТНОГО ПРОГРАММИРОВАНИЯ UNIMOD 2. ПРОЕКТИРОВАНИЕ. ВАЛИДАЦИЯ. ВЕРИФИКАЦИЯ. РЕАЛИЗАЦИЯ
- ТЕКСТОВЫЙ ЯЗЫК АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
- ТЕКСТОВЫЙ ЯЗЫК АВТОМАТНОГО ПРОГРАММИРОВАНИЯ FSML ДЛЯ ИНСТРУМЕНТАЛЬНОГО СРЕДСТВА UNIMOD
- МЕТОД РАЗРАБОТКИ ТЕСТОВ ДЛЯ ПРОГРАММНЫХ ИНТЕРФЕЙСОВ ПРИЛОЖЕНИЙ НА ОСНОВЕ КОНЕЧНО-АВТОМАТНОЙ МОДЕЛИ ТЕСТИРОВАНИЯ
- ПОСТРОЕНИЕ СИСТЕМЫ АВТОМАТИЧЕСКОГО УПРАВЛЕНИЯ МОБИЛЬНЫМ РОБОТОМ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА
- ПРИМЕНЕНИЕ КОНЕЧНЫХ АВТОМАТОВ В ДОКУМЕНТООБОРОТЕ
- МЕТОД ОБУЧЕНИЯ СЛОЖНЫХ СИСТЕМ С БОЛЬШИМ ЧИСЛОМ ВХОДНЫХ ДАННЫХ И ВЫХОДНЫХ ВОЗДЕЙСТВИЙ