VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS
Аннотация:
The paper deals with an interactive method of automatic verification for parallel automata-based programs. The hierarchical state machines can be implemented in different threads and can interact with each other. Verification is done by means of Spin tool and includes automatic Promela model construction, conversion of LTL-formula to Spin format and counterexamples in terms of automata. Interactive verification gives the possibility to decrease verification time and increase the maximum size of verifiable programs. Considered method supports verification of the parallel system for hierarchical automata that interact with each other through messages and shared variables. The feature of automaton model is that each state machine is considered as a new data type and can have an arbitrary bounded number of instances. Each state machine in the system can run a different state machine in a new thread or have nested state machine. This method was implemented in the developed Stater tool. Stater shows correct operation for all test cases.
Ключевые слова:
Постоянный URL
Статьи в номере
ОПТИЧЕСКИЙ КОНТРОЛЬ В СИСТЕМЕ УПРАВЛЕНИЯ КАЧЕСТВОМ ПРОИЗВОДСТВА ПОРШНЕВЫХ КОЛЕЦ
ПРИМЕНЕНИЕ ОПТИКО-СПЕКТРАЛЬНЫХ ТЕХНОЛОГИЙ ДЛЯ КОНТРОЛЯ И ДИАГНОСТИКИ ОТБЕЛЬНЫХ ПРОИЗВОДСТВ В ЦЕЛЛЮЛОЗНО-БУМАЖНОЙ ПРОМЫШЛЕННОСТИ
ДИСТАНЦИОННАЯ ЛАЗЕРНАЯ ИДЕНТИФИКАЦИЯ ТИПА СТРОИТЕЛЬНОГО МАТЕРИАЛА
ОПТИМИЗАЦИЯ ДИНАМИЧЕСКИХ ПАРАМЕТРОВ ОПТИЧЕСКОГО ЩУПА ТРИГГЕРНОГО ТИПА
- Анализ геномных вариантов клеток Escherichia coli К-12, устойчивых к инфекции фагом Т7
- Тест
- АНАЛИЗ МЕТОДОВ ОБРАБОТКИ ИНТЕРФЕРОМЕТРИЧЕСКИХ ДАННЫХ В СПЕКТРАЛЬНОЙ ОПТИЧЕСКОЙ КОГЕРЕНТНОЙ ТОМОГРАФИИ
- ВОССТАНОВЛЕНИЕ ИЗОБРАЖЕНИЯ С ЦИФРОВОЙ ФУРЬЕ-ГОЛОГРАММЫ В УСЛОВИЯХ ПРЕВЫШЕНИЯ ЧАСТОТЫ НАЙКВИСТА
- ОПРЕДЕЛЕНИЕ МАЛЫХ СМЕЩЕНИЙ ПОВЕРХНОСТИ ОБЪЕКТОВ МЕТОДОМ ЦИФРОВОЙ ГОЛОГРАФИИ
- ТЕРАГЕРЦОВЫЕ СПЕКТРЫ ПРОПУСКАНИЯ И ОТРАЖЕНИЯ КАТАРАКТАЛЬНО ИЗМЕНЕННЫХ ХРУСТАЛИКОВ ГЛАЗА ЧЕЛОВЕКА
- ФОРМИРОВАНИЕ РЕКУРРЕНТНОЙ АЛГОРИТМИЧЕСКОЙ СРЕДЫ КОРРЕКЦИИ МНОГОКРАТНЫХ ИСКАЖЕНИЙ СИСТЕМАТИЧЕСКИХ КОДОВ НА ОСНОВЕ КВАЗИСИНДРОМОВ В ТЕМПЕ АППАРАТНОГО ВРЕМЕНИ
- ИССЛЕДОВАНИЕ ФИЗИЧЕСКИХ ПРОЦЕССОВ В ИМПУЛЬСНОЙ КСЕНОНОВОЙ ЛАМПЕ ПРИ РАБОТЕ В ЭЛЕКТРИЧЕСКОЙ СХЕМЕ НАКАЧКИ НА ОСНОВЕ МОДУЛЯТОРА С ЧАСТИЧНЫМ РАЗРЯДОМ НАКОПИТЕЛЬНОЙ ЕМКОСТИ
- СИНТЕЗ ОПТИМАЛЬНЫХ ИСКУССТВЕННЫХ НЕЙРОННЫХ СЕТЕЙ С ПОМОЩЬЮ МОДИФИЦИРОВАННОГО ГЕНЕТИЧЕСКОГО АЛГОРИТМА
- ИДЕНТИФИКАЦИЯ И НАСТРОЙКА СИСТЕМЫ УПРАВЛЕНИЯ ЭЛЕКТРОПРИВОДА АЗИМУТАЛЬНОЙ ОСИ ТЕЛЕСКОПА
- ПРОБЛЕМНО-ОРИЕНТИРОВАННАЯ АГЕНТНАЯ ПЛАТФОРМА ДЛЯ СОЗДАНИЯ ПОЛИМОДЕЛЬНЫХ КОМПЛЕКСОВ ПОДДЕРЖКИ УПРАВЛЕНИЯ БЕЗОПАСНОСТЬЮ РЕГИОНА
- СИСТЕМЫ ДУБЛИРОВАННЫХ ВЫЧИСЛИТЕЛЬНЫХ КОМПЛЕКСОВ С ПЕРЕРАСПРЕДЕЛЕНИЕМ ЗАПРОСОВ
- ПРИМЕНЕНИЕ ПОСЛЕДОВАТЕЛЬНОСТЕЙ ДЕ БРЕЙНА ДЛЯ ПОСТРОЕНИЯ ПСЕВДОРЕГУЛЯРНЫХ КОДОВЫХ ШКАЛ
- ЗАДАЧИ РАЗВИТИЯ IT-ИНФРАСТРУКТУРЫ ПРЕДПРИЯТИЯ
- КИНЕМАТИЧЕСКОЕ УПРАВЛЕНИЕ ДВУХПАРАМЕТРИЧЕСКОЙ СКАНИРУЮЩЕЙ АНТЕННОЙ
- КОЛИЧЕСТВЕННОЕ ОПИСАНИЕ НЕЛИНЕЙНОЙ ДИНАМИКИ ПОРИСТОЙ АКРИЛОВОЙ ТОНКОЙ ПЛЕНКИ
- МЕТОДИКА РАСЧЕТА СВОБОДНОКОНВЕКТИВНОГО ТЕПЛООБМЕНА НА ТВЕРДЫХ ПОВЕРХНОСТЯХ В ШИРОКОМ ИНТЕРВАЛЕ ТЕМПЕРАТУР
- МАТЕМАТИЧЕСКИЕ МОДЕЛИ ОЦЕНКИ ИНФРАСТРУКТУРЫ СИСТЕМЫ ЗАЩИТЫ ИНФОРМАЦИИ НА ПРЕДПРИЯТИИ
- ПОИСК ВРЕДОНОСНЫХ ПРОГРАММ НА ОСНОВЕ АНАЛИЗА ПРОЦЕССА РАСПРОСТРАНЕНИЯ
- ВЕРОЯТНОСТНАЯ МОДЕЛЬ ОЦЕНКИ ИНФОРМАЦИОННОГО ВОЗДЕЙСТВИЯ
- МЕХАНИЗМЫ И ПОСЛЕДСТВИЯ ПРЕДНАМЕРЕННЫХ ЭЛЕКТРОМАГНИТНЫХ ВОЗДЕЙСТВИЙ НА ПЕРЕДАЧУ ДАННЫХ
- ИНТЕГРИРОВАННЫЕ ТЕХНОЛОГИИ ПРОЕКТИРОВАНИЯ ИЗДЕЛИЙ ИЗ ПОЛИМЕРНЫХ КОМПОЗИЦИОННЫХ МАТЕРИАЛОВ
- ОБЕСПЕЧЕНИЕ КАЧЕСТВА ПОВЕРХНОСТЕЙ ДЕТАЛЕЙ НА ЭЛЕКТРОЭРОЗИОННОМ ОБОРУДОВАНИИ
- НАУЧНЫЕ ПРЕДПОСЫЛКИ МЕНЕДЖМЕНТА ИНТЕЛЛЕКТУАЛЬНОЙ СОБСТВЕННОСТИ В РЕШЕНИИ ЗАДАЧ ИННОВАЦИОННОГО РАЗВИТИЯ РОССИИ
- МЕТОДОЛОГИЧЕСКИЕ ОСНОВЫ УСТОЙЧИВОСТИ И УСТОЙЧИВОГО РАЗВИТИЯ ПРЕДПРИНИМАТЕЛЬСКИХ СТРУКТУР КАК СОЦИАЛЬНО-ЭКОНОМИЧЕСКИХ СИСТЕМ
- СОВЕРШЕНСТВОВАНИЕ СИСТЕМЫ УПРАВЛЕНИЯ РИСКАМИ ПРИ ПЕРЕМЕЩЕНИИ ТОВАРОВ И ТРАНСПОРТНЫХ СРЕДСТВ ЧЕРЕЗ ТАМОЖЕННУЮ ГРАНИЦУ РОССИЙСКОЙ ФЕДЕРАЦИИ
- РАСПРЕДЕЛЕНИЕ ВЕНЧУРНЫХ ИНВЕСТИЦИЙ ПО СТАДИЯМ ИННОВАЦИЙ В РОССИИ И США
- МОДЕЛЬ УПРАВЛЕНИЯ ПРОЕКТАМИ КОМПЕТЕНТНОСТНО-ОРИЕНТИРОВАННЫХ ОСНОВНЫХ ОБРАЗОВАТЕЛЬНЫХ ПРОГРАММ ВУЗА
- ТЕМПЕРАТУРНАЯ ЗАВИСИМОСТЬ ПОКАЗАТЕЛЯ ПРЕЛОМЛЕНИЯ ВОДНЫХ РАСТВОРОВ ЭТИЛЕНГЛИКОЛЯ И ПРОПИЛЕНГЛИКОЛЯ
- АРХИТЕКТУРА ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ АВТОМАТИЗИРОВАННОГО РАБОЧЕГО МЕСТА РАЗРАБОТЧИКА БОРТОВОГО АВИАЦИОННОГО ОБОРУДОВАНИЯ
- РЕАЛИЗАЦИЯ ЖИЗНЕННОГО ЦИКЛА «ПРОЕКТИРОВАНИЕ-ПРОИЗВОДСТВО-ЭКСПЛУАТАЦИЯ» БОРТОВОГО ОБОРУДОВАНИЯ НА ПРЕДПРИЯТИЯХ АВИАЦИОННОЙ ПРОМЫШЛЕННОСТИ
- О РАБОТАХ ПО ЗАЩИТЕ ИНФОРМАЦИИ ОТ ПРЕДНАМЕРЕННЫХ ЭЛЕКТРОМАГНИТНЫХ ВОЗДЕЙСТВИЙ
- ВАРИАНТЫ ОБЪЕДИНЕНИЯ РАЗНОТИПНЫХ КАНАЛОВ ВЫЧИСЛИТЕЛЬНОЙ СЕТИ
- ОЦЕНКА ФУНКЦИОНАЛЬНОЙ БЕЗОПАСНОСТИ ДУБЛИРОВАННЫХ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ
- ОБЗОР СИСТЕМ ФИНАНСОВОГО ПЛАНИРОВАНИЯ, ПРЕДСТАВЛЕННЫХ НА РЫНКЕ КАЗАХСТАНА
- МУЗЫКАЛЬНО-КОМПЬЮТЕРНЫЕ ТЕХНОЛОГИИ В СИСТЕМЕ СОВРЕМЕННОГО МУЗЫКАЛЬНОГО ОБРАЗОВАНИЯ