Метод верификации параллельного и распределенного программного обеспечения на C# путем проведения трансформации абстрактного синтаксического дерева Roslyn в модель на Promela

Метод верификации параллельного и распределенного программного обеспечения на C# путем проведения трансформации абстрактного синтаксического дерева Roslyn в модель на Promela

Язык статьи
Английский
Аннотация
В статье мы описываем подход для формальной проверки параллельных и распределенных программ на C#. Мы используем технологию Microsoft Roslyn для получения синтаксической и семантической информации об интересных конструкциях в реальном коде, чтобы сгенерировать соответствующий код на модельном языке Promela, предназначенном для описания взаимодействующих систем на основе акторов. Затем мы проверяем проблемы параллельного и распределенного кода, используя предопределенные предикаты LTL для модельной программы. Мы можем определять проблемы гонки данных, неправильное использование блокировок, возможные взаимоблокировки в распределенных сервисных взаимодействиях с использованием подхода проверки модели. Описанный метод может быть использован для построения статического анализатора для платформы .NET.
УДК
Страницы
13-44
Файл
Номер