Формальная верификация окружения времени выполнения робототехнической системы

В данной работе была проведена формальная верификация многопоточного скриптового окружения методом проверки модели (model checking). Была создана документированная, корректная и адекватная модель, при построении которой были смоделированы компоненты и примитивы инструментария Qt, с помощью которого была написана исходная программа. Были сформулированы требования на естественном языке и разработаны спецификации к системе на языке LTL на основе ожидаемого поведения исходной системы. Верификатором SPIN были найдены тринадцать многопоточных ошибок в исходной программе.

Математика
Дипломы

Вуз: Санкт-Петербургский государственный университет (СПбГУ)

ID: 587d364d5f1be77c40d58bfa
UUID: 23676a60-d0b5-46e6-99d9-115eb3f05c1d
Язык: Русский
Опубликовано: больше 4 лет назад
Просмотры: 14

Никольский Кирилл Андреевич

Источник: Санкт-Петербургский государственный университет


0

Комментировать 0

Рецензировать 0

Скачать - 127025 bytes


Поделиться работой
Current View

Рецензии:

  Авторизуйтесь, чтобы добавить рецензию

- у работы пока нет рецензий -

Для лиц старше 18 лет