Рассматриваются вопросы асинхронного моделирования NCESсетей с помощью формализма, основанного на сетях Петри. <...> Приводятся правила трансформации 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сетей может быть использована при реализации NCES-сетей в мультипрограммных средах и на различных аппаратных платформах. <...> Асинхронность означает, что
срабатывания переходов не привязаны ни к каким внешним событиям и не
существует механизма глобального времени для срабатывания переходов. <...> Переход от NCES-сети к асинхронной модели (А-модели) описывается с помощью правил трансформации сетевых моделей. <...> 1 NCES-сети
Ниже (без потери общности) рассматриваются замкнутые одноуровневые NCES-сети, расширенные ингибиторными дугами. <...> Информатика, вычислительная <...>