Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:004.05
Номер:1 (89)
ВЕРИФИКАЦИЯ ПАРАЛЛЕЛЬНЫХ АВТОМАТНЫХ ПРОГРАММ
Аннотация:
Рассмотрен интерактивный метод верификации параллельных автоматных программ, в которых иерархические автоматы могут реализовываться в разных потоках и взаимодействовать друг с другом. Верификация проводится при помощи инструментального средства Spin, включает в себя автоматическое построение модели на языке Promela, приведение LTL-формулы в формат, определяемый инструментальным средством Spin и построение контрпримера в терминах автоматов. Интерактивная верификация позволяет сократить время верификации и увеличить максимально возможный размер верифицируемых программ. Рассмотренный метод позволяет верифицировать параллельную систему иерархических автоматов, которые взаимодействуют между собой через сообщения и общие переменные. Особенность автоматной модели состоит в том, что каждый автомат объявляется как новый тип данных и может иметь произвольное (но заранее заданное) число экземпляров. Каждый конечный автомат в системе может запускать другой автомат в новом потоке или иметь вложенный автомат. Была проведена апробация инструментального средства Stater, разработанного на основе данного метода. На всех примерах Stater отработал правильно.
Ключевые слова:
Постоянный URL
Статьи в номере
- ПЛАЗМОННЫЕ СОЛИТОНЫ, КИНКИ И ВОЛНЫ ФАРАДЕЯ В ДВУМЕРНОЙ РЕШЕТКЕ МЕТАЛЛИЧЕСКИХ НАНОЧАСТИЦ
- ИССЛЕДОВАНИЕ ХАРАКТЕРИСТИК СИГНАЛОВ СПЕКТРАЛЬНОЙ ИНТЕРФЕРЕНЦИИ В БЛИЖНЕЙ ИК ОБЛАСТИ СПЕКТРА
- ЛОГИКА С ИСКЛЮЧЕНИЕМ НА АЛГЕБРЕ ФУРЬЕ-ДУАЛЬНЫХ ОПЕРАЦИЙ: НЕЙРОСЕТЕВОЙ МЕХАНИЗМ РЕДУЦИРОВАНИЯ КОГНИТИВНОГО ДИССОНАНСА
- ИЗВЛЕЧЕНИЕ МАТЕРИАЛЬНЫХ ПАРАМЕТРОВ ПЛАЗМОННОГО МУЛЬТИСЛОЯ ИЗ КОЭФФИЦИЕНТОВ ОТРАЖЕНИЯ И ПРОХОЖДЕНИЯ
- МЕТОД ИССЛЕДОВАНИЯ ЗАВИСИМОСТИ h-ПАРАМЕТРА АНИЗОТРОПНОГО СВЕТОВОДА ОТ РАДИУСА ИЗГИБА
- ТЕХНОЛОГИЧЕСКИЕ МЕТОДЫ СНИЖЕНИЯ УРОВНЯ ОПТИЧЕСКИХ ПОТЕРЬ В МИКРОСТРУКТУРИРОВАННЫХ ВОЛОКОННЫХ СВЕТОВОДАХ
- МНОГОЗОННОЕ ПРОСВЕТЛЯЮЩЕЕ ПОКРЫТИЕ НА ПОДЛОЖКЕ ИЗ ОПТИЧЕСКОГО СУЛЬФИДА ЦИНКА
- КОНТРОЛЬ СТРУКТУРЫ РАЗЛИЧНЫХ ВИДОВ БУМАГИ МЕТОДОМ АТОМНО-СИЛОВОЙ МИКРОСКОПИИ
- ЭНЕРГОСБЕРЕГАЮЩАЯ ТЕХНОЛОГИЯ РАСПЛАВЛЕНИЯ ХИМИЧЕСКИХ ВЕЩЕСТВ СВЕТОВЫМ ИЗЛУЧЕНИЕМ
- О ТЕХНОЛОГИЧЕСКИХ НЕСОВЕРШЕНСТВАХ ГЕОМЕТРИЧЕСКИХ ПАРАМЕТРОВ СИЛОВОГО СТЕРЖНЯ ДЛЯ ЗАГОТОВКИ ОПТИЧЕСКОГО ВОЛОКНА PANDA
- АНАЛИЗ ДАННЫХ НА ОСНОВЕ ПЛАТФОРМЫ SQL-MAPREDUCE
- О ВЛИЯНИИ АДАПТИВНЫХ ПОЛЬЗОВАТЕЛЬСКИХ ИНТЕРФЕЙСОВ НА НАДЕЖНОСТЬ И ЭФФЕКТИВНОСТЬ ФУНКЦИОНИРОВАНИЯ АВТОМАТИЗИРОВАННЫХ СИСТЕМ
- МЕТОД ОТОБРАЖЕНИЯ ЗАДАЧ НА КРУПНОГРАНУЛЯРНЫЕ РЕКОНФИГУРИРУЕМЫЕ ВЫЧИСЛИТЕЛЬНЫЕ СИСТЕМЫ
- ОЦЕНКА ПРИМЕНИМОСТИ МОДЕЛИ IRI-2012 ДЛЯ АВТОМАТИЗИРОВАННОЙ ОБРАБОТКИ ИОНОГРАММ ВЕРТИКАЛЬНОГО ЗОНДИРОВАНИЯ
- ОЦЕНКА ТОЧНОСТИ ВИЗУАЛИЗАЦИИ МЕСТОПОЛОЖЕНИЯ ОБЪЕКТА В ГЕОИНФОРМАЦИОННЫХ СИСТЕМАХ И СИСТЕМАХ ИНДИКАЦИИ НАВИГАЦИОННЫХ КОМПЛЕКСОВ ПИЛОТИРУЕМЫХ ЛЕТАТЕЛЬНЫХ АППАРАТОВ
- ПРИМЕНЕНИЕ МЕТОДОВ МАШИННОГО ОБУЧЕНИЯ ДЛЯ ОБНАРУЖЕНИЯ БАКТЕРИЙ В ПРОДУКТАХ ПИТАНИЯ
- ПРЕДСТАВЛЕНИЕ ДОКУМЕНТОВ В ЗАДАЧЕ КЛАСТЕРИЗАЦИИ АННОТАЦИЙ НАУЧНЫХ ТЕКСТОВ
- ИСПОЛЬЗОВАНИЕ КОНТЕЙНЕРА BC7 ДЛЯ ХРАНЕНИЯ ТЕКСТУР С ГЛУБИНОЙ ЦВЕТА 10 БИТ
- ПРЕДШЕСТВУЮЩАЯ И ПОСЛЕДУЮЩАЯ ФИЛЬТРАЦИЯ ШУМОВ В АЛГОРИТМАХ ВОССТАНОВЛЕНИЯ ИЗОБРАЖЕНИЙ
- ОЦЕНКА ВОЗМОЖНОСТИ ЭКРАННОЙ РЕПРОДУКЦИИ НАСЫЩЕННЫХ ПИГМЕНТОВ
- ЭКСПЛУАТАЦИОННЫЕ ХАРАКТЕРИСТИКИ РИСКА НАРУШЕНИЙ БЕЗОПАСНОСТИ ИНФОРМАЦИОННОЙ СИСТЕМЫ
- ИДЕНТИФИКАЦИЯ АНОНИМНЫХ ПОЛЬЗОВАТЕЛЕЙ ИНТЕРНЕТ-ПОРТАЛОВ НА ОСНОВАНИИ ТЕХНИЧЕСКИХ И ЛИНГВИСТИЧЕСКИХ ХАРАКТЕРИСТИК ПОЛЬЗОВАТЕЛЯ
- МЕТОДИКА РАСЧЕТА КОЭФФИЦИЕНТОВ ОБЛУЧЕННОСТИ ЦИЛИНДРИЧЕСКОГО КОСМИЧЕСКОГО ОБЪЕКТА ПОДСВЕТКОЙ ЗЕМЛИ
- АВТОНОМИЗАЦИЯ НЕЛИНЕЙНЫХ ДИНАМИЧЕСКИХ СИСТЕМ
- СОВРЕМЕННОЕ СОСТОЯНИЕ И ПЕРСПЕКТИВЫ РАЗВИТИЯ ОСНОВНЫХ ПОНЯТИЙ В ОБЛАСТИ МЕХАТРОНИКИ
- ОПЫТ ПРИМЕНЕНИЯ И ПЕРСПЕКТИВЫ ТЕХНОЛОГИИ АЛМАЗНОГО МИКРОТОЧЕНИЯ
- ОСОБЕННОСТИ ФОРМИРОВАНИЯ ПРЯМЫХ ЗУБЬЕВ ЦИЛИНДРИЧЕСКИХ КОЛЕС СТУПЕНЧАТЫМ ДОЛБЯКОМ
- ПРОБЛЕМА УЧЕТА ЗАВИСИМОСТИ КОЭФФИЦИЕНТА ОБЪЕМНОЙ ТЕПЛОЕМКОСТИ ОТ ТЕМПЕРАТУРЫ ПРИ МОДЕЛИРОВАНИИ ЛАЗЕРНО-ДУГОВОЙ НАПЛАВКИ
- МЕТОДЫ МОДЕЛИРОВАНИЯ ТЕМПЕРАТУРНОГО ПОЛЯ ПРИ БЕСКОНТАКТНОЙ ЛАЗЕРНОЙ ДЕФОРМАЦИИ ПЛАСТИНЫ
- ЧИСЛЕННОЕ МОДЕЛИРОВАНИЕ ТУРБУЛЕНТНОГО ПОТОКА ВОЗДУХА С ИСПОЛЬЗОВАНИЕМ МЕТОДА ОТСОЕДИНЕННЫХ ВИХРЕЙ
- СТРАТЕГИЯ МАРКЕТ-МЕЙКИНГА В СИСТЕМЕ ВЫСОКОЧАСТОТНОЙ АЛГОРИТМИЧЕСКОЙ ТОРГОВЛИ
- ОТ ТРАДИЦИОННОГО ДИСТАНЦИОННОГО ОБУЧЕНИЯ К МАССОВЫМ ОТКРЫТЫМ ОНЛАЙН-КУРСАМ
- ОБРАТИМАЯ ФОТОДЕСТРУКЦИЯ НАНОЧАСТИЦ СЕРЕБРА В ФОТО-ТЕРМО-РЕФРАКТИВНЫХ СТЕКЛАХ
- УРАВНЕНИЯ ПЕРЕНОСА ИЗЛУЧЕНИЯ В ИНФРАКРАСНОЙ ТОМОГРАФИИ В СЛУЧАЕ АКТИВНО-ПАССИВНОЙ ДИАГНОСТИКИ И ВЕЕРНОГО СКАНИРОВАНИЯ
- ПОЛУЧЕНИЕ СПЕКТРОВ ЭЛЕКТРОФИЗИОЛОГИЧЕСКИХ СИГНАЛОВ В РЕЖИМЕ РЕАЛЬНОГО ВРЕМЕНИ