ВВЕДЕНИЕ В ВЕРИФИКАЦИЮ АВТОМАТНЫХ ПРОГРАММ НА ОСНОВЕ МЕТОДА MODEL CHECKING
Аннотация:
В статье применительно к автоматным программам (их поведение описывается одним конечным автоматом) излагается техника верификации, которая базируется на темпоральных логиках и называется Model Checking. Для автоматных программ удается автоматизировать процесс построения модели программы, подлежащей верификации.
Ключевые слова:
Постоянный URL
Статьи в номере
- СОВРЕМЕННОЕ СОСТОЯНИЕ И ПЕРСПЕКТИВЫ РАЗВИТИЯ ТОМОГРАФИИ
- РАЗРАБОТКА АЛГОРИТМИЧЕСКОГО И ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ ДЛЯ МОДЕЛИРОВАНИЯ АПЕРТУРЫ СБОМ – ЗОНДОВ НА ОСНОВЕ ЭКСПЕРИМЕНТАЛЬНОГО ИССЛЕДОВАНИЯ ДАЛЬНЕПОЛЬНОЙ ОСВЕЩЕННОСТИ
- ИСПОЛЬЗОВАНИЕ АВТОМАТОВ С ФЛАГАМИ ДЛЯ РЕШЕНИЯ
- ОПТИМИЗАЦИЯ ИНФОРМАЦИОННЫХ ПОДСИСТЕМ СЛЕДЯЩИХ ЭЛЕКТРОПРИВОДОВ ПРЕЦИЗИОННЫХ КОМПЛЕКСОВ СЛЕЖЕНИЯ
- ОПТИКО–ГЕОМЕТРИЧЕСКИЙ МЕТОД ИССЛЕДОВАНИЯ НАПРЯЖЕННО-ДЕФОРМИРОВАННЫХ СОСТОЯНИЙ ЭЛЕМЕНТОВ МИКРОЭЛЕКТРОНИКИ И МИКРОСЕНСОРНОЙ ТЕХНИКИ
- РАЗРАБОТКА АВТОМАТИЗИРОВАННОЙ СИСТЕМЫ КОНТРОЛЯ КАЧЕСТВА МИКРО- И НАНОСТРУКТУР
- ТЕКСТОВЫЙ ЯЗЫК АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
- АЛГОРИТМ АДАПТАЦИИ С АСТАТИЗМОМ ПЕРВОГО ПОРЯДКА ДЛЯ СТАБИЛИЗАЦИИ ЛИНЕЙНОГО ВОЗМУЩЕННОГО НЕСТАЦИОНАРНОГО ОБЪЕКТА
- ФОРМИРОВАНИЕ НАНОСВИТКОВ В ВЯЗКОЙ ЖИДКОСТИ