В работе рассматриваются эксперименты с конечными полуавтоматами, направленные на идентификацию финального (текущего) состояния проверяемой системы после подачи соответствующей входной последовательности. В исследуемой модели действия разделены на входные и выходные, однако в модели отсутствуют специально выделенные семейства начальных и финальных состояний. В статье определяются подходящий синхронизирующий и установочный эксперименты, и предлагаются...

В статье рассказывается о недавних достижениях на пути к строгой верификации промышленных операционных систем (ОС). Под промышленной ОС имеется в виду система, активно используемая в некоторой области, развиваемая и сопровождаемая на протяжении значительного времени. Статья не касается исследовательских ОС, разработанных обычно с целью проверки некоторых идей. Рассматривается декомпозиция задача верификации...

Технология передачи пакетов с принудительной буферизацией традиционно используется в современных сетевых устройствах, таких как коммутаторы и маршрутизаторы. Но иногда она является существенным препятствием для улучшения качества обслуживания, поскольку минимальное время доставки пакета ограничено произведением количества промежуточных узлов на время передачи пакета в канале. Технология сквозной передачи пакетов устраняет это ограничение...

В статье представлены подходы к проектированию и реализации программного обеспечения для подготовки нормализованной воды, архитектура, полученные автоматные диаграммы данного процесса, основанные на спецификациях и требованиях. Обсуждаются компоненты системы, уровни абстракции, точки верификации, проблемы при разработке приложения. Показан способ разработки подобных надежных систем.

Разыменование нулевого указателя остаётся одной из основных проблем в современных объектно-ориентированных языках. Очевидное добавление ключевых слов, чтобы различать между всегда ненулевыми и возможно нулевыми ссылками, оказывается недостаточным во время инициализации объекта, когда некоторые поля, объявленные как всегда ненулевые, могут временно быть нулевыми до окончания инициализации. Предлагаемое решение избегает явного кодирования...

Данная работа представляет дальнейшее развитие метода верификации финитной итерации. Она расширяет смешанную аксиоматическую семантику, предложенную для верификации C-light программ. Это расширение включает в себя метод верификации финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию...

Целью этого исследования является демонстрация возможности автоматизированной миграции программного кода на новый набор библиотек. Задача миграции кода – не редкость в современных программных проектах. Например, такая задача может возникнуть, когда необходимо перенести проект на другую библиотеку или на другую программную платформу. Разработанный в данной работе метод и прототип инструмента миграции...

В статье представлен подход к реализации статической проверки типов для динамически-типизированного языка Jolie.