Лукьянова Е. А.

Метод верификации свойств реактивной системы на модели

Авторы: 
Лукьянова Е. А.
Журнал: 
ТВИМ 2006 №2
Страница: 
60
В работе описывается подход к верификации асинхронных дискретных динамических реактивных систем, основанный на использовании темпоральной логики (CTL - Computation Tree Logic), сетей Петри (СП) и систем линейных диофантовых ограничений (СЛДО).

Метод моделирования реактивных систем с параллельными и последовательными процессами

Авторы: 
Дереза А. В.
Лукьянова Е. А.
Журнал: 
ТВИМ 2011 №1
Страница: 
107
Предлагается метод построения модели сложной многоблоковой реальной системы. Решается задача комбинирования последовательного и параллельного выполнения исходных процессов моделируемой системы за счет APPLY - операции для OBDD, представляющих автоматы соответствующих сетей Петри компонент исследуемой системы.

О компонентном анализе параллельных распраделенных систем.

Авторы: 
Лукьянова Е. А.
Журнал: 
ТВИМ 2011 №2
Страница: 
71
Представлена методология верификации параллельных и распределенных систем с помощью компонентных сетей Петри. Использование компонентных сетей Петри для моделирования параллельных и распределенных систем значительно уменьшает размеры модели и сокращает время верификации. Представленная методология изучена на примере верификации задачи о пяти философах.  

О способах построения и использовании компонентной сети Петри с ингибиторными дугами для анализа её исходной детальной модели Петри

Авторы: 
Лукьянова Е. А.
Журнал: 
ТВИМ 2012 №2
Страница: 
45
Приведјн алгоритм построения компонентной сети Петри с ингибиторными дугами (CNI-сети). Возможные способы построения CNI-сети разобраны на примерах.  Установлен факт использования компонентного анализа CNI-сети для исследования свойств детальной модели исследуемой системы.