Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:004.4’242
Номер:5 (69)
Скачать PDF0 Кбайт
ПРИМЕНЕНИЕ ШАБЛОНОВ ТРЕБОВАНИЙ К ФОРМАЛЬНОЙ СПЕЦИФИКАЦИИ И ВЕРИФИКАЦИИ АВТОМАТНЫХ ПРОГРАММ
Аннотация:
Верификация на модели (model checking) является глубоко проработанной технологией проверки корректности программного обеспечения, однако при этом она недостаточно широко используется на практике. Одной из причин является сложность составления формальных требований на языке темпоральных логик. В настоящей работе описывается подход для записи верифицируемых требований на подмножестве естественного языка в контексте автоматного программирования. В частности, приводится анализ применимости шаблонов требований к формальной спецификации автоматных программ, а также описывается грамматика для вывода требований.
Ключевые слова:
Постоянный URL
Статьи в номере
- ИССЛЕДОВАНИЕ ПАРАМЕТРОВ ПОВЕРХНОСТНО ОКРАШЕННЫХ ПОЛИМЕРНЫХ ЛИНЗ
- МЕТОД УСТРАНЕНИЯ ВЛИЯНИЯ СИГНАЛА ПОМЕХИ НА ЧУВСТВИТЕЛЬНОСТЬ ПРИЕМА ГИДРОАКУСТИЧЕСКОЙ АНТЕННЫ НА ОСНОВЕ ВОЛОКОННЫХ БРЭГГОВСКИХ РЕШЕТОК
- ПОЛУЧЕНИЕ ОПТИЧЕСКИХ ПОВЕРХНОСТЕЙ ЭЛЕМЕНТОВ НА ОСНОВЕ СУЛЬФИДА ЦИНКА
- ЦИФРОВАЯ ОБРАБОТКА ДИФРАКЦИОННЫХ КАРТИН ФРАУНГОФЕРА ПРИ КОНТРОЛЕ ГЕОМЕТРИЧЕСКИХ ПАРАМЕТРОВ ОБЪЕКТОВ
- ИССЛЕДОВАНИЕ ПАРАМЕТРОВ МИКРОСТРУКТУРЫ ПЛЕНОК ХРОМА И ИХ ВЛИЯНИЯ НА РЕЗУЛЬТАТЫ ЛОКАЛЬНОГО ТЕРМОХИМИЧЕСКОГО ОКИСЛЕНИЯ ПОД ДЕЙСТВИЕМ ЛАЗЕРНОГО ИЗЛУЧЕНИЯ
- ИССЛЕДОВАНИЕ СТРУКТУРЫ ТОНКИХ МЕТАЛЛИЧЕСКИХ ПЛЕНОК ПОСЛЕ ВОЗДЕЙСТВИЯ ФЕМТОСЕКУНДНЫХ ЛАЗЕРНЫХ ИМПУЛЬСОВ
- ИССЛЕДОВАНИЕ ВОЗДЕЙСТВИЯ УФ ИЗЛУЧЕНИЯ НА ПОВЕРХНОСТЬ ТОНКИХ ПЛЕНОК
- ИССЛЕДОВАНИЕ ПРОЦЕССА ФОРМИРОВАНИЯ СВЕТОКОНТРАСТНОГО РАСТРА ПОСРЕДСТВОМ ЛАЗЕРНОГО МАРКИРОВАНИЯ
- УПРАВЛЕНИЕ НЕТРИВИАЛЬНЫМИ МАЯТНИКОВЫМИ СИСТЕМАМИ В УСЛОВИЯХ ПАРАМЕТРИЧЕСКОЙ И ФУНКЦИОНАЛЬНОЙ НЕОПРЕДЕЛЕННОСТЕЙ
- СИНТЕЗ СИСТЕМЫ УПРАВЛЕНИЯ ЭЛЕКТРОПРИВОДА АЗИМУТАЛЬНОЙ ОСИ АЛТАЙСКОГО ТЕЛЕСКОПА ТИ-3.12
- РАСЧЕТ КОЭФФИЦИЕНТОВ ПРОХОЖДЕНИЯ И ОТРАЖЕНИЯ В СИСТЕМЕ СВЯЗАННЫХ КВАНТОВЫХ ВОЛНОВОДОВ
- ПРОГРАММНЫЙ КОМПЛЕКС ДЛЯ АНАЛИЗА ЭФФЕКТИВНОСТИ АЛГОРИТМОВ РЕШЕНИЯ НЕЛИНЕЙНЫХ ЗАДАЧ ОБРАБОТКИ НАВИГАЦИОННОЙ ИНФОРМАЦИИ
- КОМПЕНСАЦИЯ РАДИАЛЬНЫХ ЭЛЕКТРОМАГНИТНЫХ СИЛ ВЕНТИЛЬНОГО ДВИГАТЕЛЯ, ВЫЗВАННЫХ НЕСИММЕТРИЕЙ СТАТОРНОЙ ОБМОТКИ
- ДВУХЧАСТИЧНАЯ МОДЕЛЬ ПРОВОДНИКА С КВАНТОВЫМ КОЛЬЦОМ
- РАСЧЕТ СОСТАВНЫХ ЧАСТЕЙ СПЕКТРОМЕТРИЧЕСКОГО ПОЗИЦИОННО-ЧУВСТВИТЕЛЬНОГО ДЕТЕКТОРА НЕЙТРОНОВ
- ОБ УЧЕТЕ ИСТОЧНИКОВ ЭЛЕКТРОМАГНИТНОГО ПОЛЯ В СОВМЕСТНОМ МЕТОДЕ КОНЕЧНЫХ И ГРАНИЧНЫХ ЭЛЕМЕНТОВ
- РАЗРАБОТКА АЛГОРИТМА ФОРМИРОВАНИЯ ПАКЕТОВ ЗАКАЗОВ В УСЛОВИЯХ ВИРТУАЛЬНОГО ПРЕДПРИЯТИЯ
- ИМИТАЦИЯ ГИДРОСТАТИЧЕСКОГО ДАВЛЕНИЯ ПРИ ИСПЫТАНИЯХ ПУСКОВЫХ УСТРОЙСТВ АВТОНОМНЫХ НЕОБИТАЕМЫХ ПОДВОДНЫХ АППАРАТОВ В ЦЕХОВЫХ УСЛОВИЯХ
- ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ ДЛЯ ПОСТРОЕНИЯ АВТОМАТОВ УПРАВЛЕНИЯ СИСТЕМАМИ СО СЛОЖНЫМ ПОВЕДЕНИЕМ НА ОСНОВЕ ОБУЧАЮЩИХ ПРИМЕРОВ И СПЕЦИФИКАЦИИ
- АЛГОРИТМ ВОССТАНОВЛЕНИЯ ТРЕХМЕРНОЙ МОДЕЛИ ЛИЦА ПО ФОТОГРАФИИ
- ОСОБЕННОСТИ ОПТИМИЗАЦИИ ВЫЧИСЛЕНИЙ В ПРИКЛАДНЫХ ПРОГРАММАХ НА ЯЗЫКЕ С НА ПРИМЕРЕ ОЦЕНИВАНИЯ ОПЦИОНОВ ЕВРОПЕЙСКОГО ТИПА
- СТАТИСТИЧЕСКИЙ АНАЛИЗ СТРУКТУРЫ НАНОПОРИСТЫХ СТЕКОЛ ПО ИЗОБРАЖЕНИЯМ, ПОЛУЧЕННЫМ МЕТОДОМ КОНФОКАЛЬНОЙ СКАНИРУЮЩЕЙ ЛАЗЕРНОЙ МИКРОСКОПИИ
- АЛГОРИТМЫ ПРОГРАММ ДЛЯ РЕШЕНИЯ ПРЯМЫХ И ОБРАТНЫХ ЗАДАЧ ТЕПЛОПРОВОДНОСТИ ПРИ ИСПОЛЬЗОВАНИИ ДИФФЕРЕНЦИАЛЬНО-РАЗНОСТНЫХ МОДЕЛЕЙ
- ПЕРСПЕКТИВЫ РАЗВИТИЯ ИННОВАЦИОННЫХ НАПРАВЛЕНИЙ ИССЛЕДОВАНИЙ В ОБЛАСТИ ЛАЗЕРНЫХ СИСТЕМ И БИОМЕДИЦИНСКИХ ОПТИЧЕСКИХ ТЕХНОЛОГИЙ
- МЕТОД ОПТИЧЕСКОЙ ДИФФУЗИОННОЙ СПЕКТРОСКОПИИ ДЛЯ IN VIVO ИССЛЕДОВАНИЯ ДИНАМИКИ ОКСИГЕНАЦИИ ОПУХОЛИ
- ПРЕДМЕТНО-ОРИЕНТИРОВАННЫЕ ЯЗЫКИ В ОПИСАНИИ ЗАДАЧ НАУЧНЫХ СОРЕВНОВАНИЙ
- ИНТЕРАКТИВНЫЙ ТРЕНАЖЕРНЫЙ КОМПЛЕКС ДЛЯ ГОСУДАРСТВЕННЫХ ОБРАЗОВАТЕЛЬНЫХ УЧРЕЖДЕНИЙ
- СОВЕРШЕНСТВОВАНИЕ УПРАВЛЕНИЯ КОНКУРЕНТОСПОСОБНОСТЬЮ ТОРГОВОГО ПРЕДПРИЯТИЯ В УСЛОВИЯХ СЕРВИСНО-ОРИЕНТИРОВАННОЙ ЭКОНОМИКИ
- ГЕНЕРИРУЕМЫЕ ЗАДАЧИ В СИСТЕМЕ ДЛЯ ОРГАНИЗАЦИИ УДАЛЕННОЙ РАБОТЫ С ЗАДАЧАМИ
- ИССЛЕДОВАНИЕ ДЕФЕКТОВ СИСТЕМЫ Si/SiO2, ИНДУЦИРОВАННЫХ ЛАЗЕРНЫМ ВОЗДЕЙСТВИЕМ
- P-I-N СТРУКТУРЫ НА ОСНОВЕ GaAs ДЛЯ ДЕТЕКТОРОВ РЕНТГЕНОВСКОГО ИЗЛУЧЕНИЯ
- ВОПРОСУ О ПЕРЕВОДЕ 32-х РАЗРЯДНЫХ ПРИЛОЖЕНИЙ В 64-х РАЗРЯДНЫЕ