В работе рассматриваются эксперименты с конечными полуавтоматами, направленные на идентификацию финального (текущего) состояния проверяемой системы после подачи соответствующей входной последовательности. В исследуемой модели действия разделены на входные и выходные, однако в модели отсутствуют специально выделенные семейства начальных и финальных состояний. В статье определяются подходящий синхронизирующий и установочный эксперименты, и предлагаются методы их синтеза для специального класса входо-выходных полуавтоматов, у которых в каждом состоянии определены переходы или только по входным, или только по выходным действиям, а также в графе переходов отсутствуют циклы по выходным символам. Для описанного класса входо-выходных полуавтоматов устанавливаются необходимые и достаточные условия существования безусловных синхронизирующего и установочного экспериментов.
В статье рассказывается о недавних достижениях на пути к строгой верификации промышленных операционных систем (ОС). Под промышленной ОС имеется в виду система, активно используемая в некоторой области, развиваемая и сопровождаемая на протяжении значительного времени. Статья не касается исследовательских ОС, разработанных обычно с целью проверки некоторых идей. Рассматривается декомпозиция задача верификации ОС на подзадачи верификации ее различных частей и отдельных свойств и применение для этого разнообразных методов верификации. В статье делается попытка описать и осмыслить опыт, полученный в рамках нескольких проектов по верификации различных частей ОС в ИСП РАН.
Технология передачи пакетов с принудительной буферизацией традиционно используется в современных сетевых устройствах, таких как коммутаторы и маршрутизаторы. Но иногда она является существенным препятствием для улучшения качества обслуживания, поскольку минимальное время доставки пакета ограничено произведением количества промежуточных узлов на время передачи пакета в канале. Технология сквозной передачи пакетов устраняет это ограничение, так как для переадресации пакета используется только заголовок пакета, который содержит адрес назначения. Таким образом, технология сквозной передачи пакетов имеет значительные возможности для улучшения качества обслуживания. Модели вычислительной решетки со сквозной коммутацией пакетов были разработаны в форме раскрашенных сетей Петри. Модель состоит из узлов коммутации пакетов и генераторов трафика; который может быть представлен в виде моделей пушек генерирующих злонамеренный трафик, замаскированный под обычный мультимедийный. Настоящая работа – это дальнейшее развитие методов анализа прямоугольных коммуникационных решеток для узлов, реализующих сквозную коммутацию пакетов. Методы предназначены для применения при проектировании вычислительных решеток, в разработке новых телекоммуникационных устройств и в интеллектуальных системах защиты. Предварительные оценки показывают, что технология сквозной коммутации пакетов наследует некоторые негативные эффекты, которые ассоциируются с традиционной доставкой пакетов с принудительной буферизацией. Серия экспериментов с моделью выявила возможность блокировки решетки в условиях рабочей нагрузки. Полученные результаты применимы для интеллектуального обнаружения вторжений и планирования противодействия злонамеренному трафику.
В статье представлены подходы к проектированию и реализации программного обеспечения для подготовки нормализованной воды, архитектура, полученные автоматные диаграммы данного процесса, основанные на спецификациях и требованиях. Обсуждаются компоненты системы, уровни абстракции, точки верификации, проблемы при разработке приложения. Показан способ разработки подобных надежных систем.
Разыменование нулевого указателя остаётся одной из основных проблем в современных объектно-ориентированных языках. Очевидное добавление ключевых слов, чтобы различать между всегда ненулевыми и возможно нулевыми ссылками, оказывается недостаточным во время инициализации объекта, когда некоторые поля, объявленные как всегда ненулевые, могут временно быть нулевыми до окончания инициализации. Предлагаемое решение избегает явного кодирования этих промежуточных состояний в текстах программ в пользу статически проверяемых правил допустимости, которые не зависят от специальных условно ненулевых типов. Рассматриваются примеры инициализации объектов, предложенные ранее, и представляются новые для сравнения применимости различных подходов. Удобство использования предлагаемой схемы оценивается на открытых библиотеках с миллионом строк кода, которые были адаптированы, чтобы удовлетворять этим правилам.
Данная работа представляет дальнейшее развитие метода верификации финитной итерации. Она расширяет смешанную аксиоматическую семантику, предложенную для верификации C-light программ. Это расширение включает в себя метод верификации финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию, выражающую действие тела цикла. Это правило было реализовано в генераторе условий корректности, являющемся частью нашей системы верификации C-light программ. Для доказательства порождённых условий корректности используется индукция, вызывающая сложности у SMT-решателей. На стадии доказательства в нашей системе используется SMT-решатель Z3. Для преодоления упомянутой трудности была предложена стратегия переписывания условий корректности. Она позволяет автоматически верифицировать финитную итерацию в Z3. Также статья описывает применение доказателя теорем PVS для автоматического доказательства подобных условий корректности. Рассмотрен пример, иллюстрирующий применение этих методов.
Целью этого исследования является демонстрация возможности автоматизированной миграции программного кода на новый набор библиотек. Задача миграции кода – не редкость в современных программных проектах. Например, такая задача может возникнуть, когда необходимо перенести проект на другую библиотеку или на другую программную платформу. Разработанный в данной работе метод и прототип инструмента миграции основаны на ранее созданном авторами формализме для описания семантики библиотек. Данный формализм предлагает описывать поведение библиотек с помощью системы расширенных конечных автоматов.
В статье представлена метамодель программных библиотек, а также простой в использовании DSL для описания конкретных библиотек. Представленная метамодель напрямую формирует метод миграции, также описанный в данной статье. Процесс миграции разбит на пять шагов, и для каждого шага предложен алгоритм выполнения.
Рассмотренные модели и алгоритмы реализованы в прототипе инструмента автоматизированной миграции программного кода. Разработанный прототип инструмента был протестирован на нескольких синтетических примерах кода, а также на реальном проекте. Результаты эксперимента показывают, что миграция кода может быть успешно автоматизирована, и разработанный прототип служит доказательством концепции. Созданные модели и алгоритмы формируют основу для более мощных методов и инструментов миграции.
В статье представлен подход к реализации статической проверки типов для динамически-типизированного языка Jolie.