Асинхронное моделирование NCES-сетей

NCES-сети асинхронное моделирование асинхронные модели сети Петри Петри сети Model Checking сетевые системы верификация моделей

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

Рассматриваются вопросы асинхронного моделирования NCESсетей с помощью формализма, основанного на сетях Петри. <...> Асинхронное моделирование рассматривается как шаг к формальной верификации NCES-сетей с помощью метода Model Checking. <...> Ключевые слова: асинхронное моделирование, сетевые системы «условие– событие», сети Петри, проверка моделей, трансформация моделей. <...> In the paper questions of asynchronous modelling of net condition/event systems (NCES) using a formalism based on Petri nets, are considered. <...> Rules for transforming NCES to the asynchronous model are represented. <...> The asynchronous modelling is considered as the starting point to formal verification of NCES by means of the model checking method. <...> Поволжский регион Результативным методом формальной верификации моделей с конечным, возможно очень большим, числом состояний (к каким относятся при определенных ограничениях и NCES-сети) является Model Checking (проверка моделей) [5]. <...> Она успешно использовалась в качестве метода формальной верификации недетерминированных автоматов [7], сетей Петри [8], а также сетевых моделей, основанных на сетях Петри, таких как PRES-сети [9] и сети Петри с дуальными переходами [10]. <...> Моделирование NCES-сетей «в лоб» как синхронно-асинхронной системы в верификаторах типа SMV затруднительно из-за сложности явного вычисления разрешенных шагов [12], вычисление же разрешенных шагов в асинхронной модели производится автоматически. <...> Асинхронность означает, что срабатывания переходов не привязаны ни к каким внешним событиям и не существует механизма глобального времени для срабатывания переходов. <...> Переход от NCES-сети к асинхронной модели (А-модели) описывается с помощью правил трансформации сетевых моделей. <...> 1 NCES-сети Ниже (без потери общности) рассматриваются замкнутые одноуровневые NCES-сети, расширенные ингибиторными дугами. <...> Информатика, вычислительная техника бытийный режим работы переходов; m0: P N0 = {0, 1, …} – начальная маркировка. <...> Маркировка m сети NCES есть отображение m: P N0. <...> Событийный режим em(t) перехода t определяет, как связаны входящие событийные дуги – конъюнктивно (AND) или дизъюнктивно (OR <...>

• Похожие документы из РУАЭСТ
• |
• Похожие документы из Руконт