A method of sample models of program construction in terms of Petri nets

В данной работе рассматривается с формальной точки зрения метод построения сетей Петри, имитирующих поведение императивных программ. Примеры сетей Петри с заданными характеристиками являются необходимыми в процессе программирования новых алгоритмов анализа моделей программ, в частности, они могут использоваться для разработки и оптимизации алгоритмов композиции и декомпозиции сетей Петри, построения дерева достижимости, проверки инвариантов и т.д. Способ построения состоит из двух стадий. На первой стадии описываются шаблонные конструкции, из которых будет состоять результирующая сеть, и параметры, с которыми будет выполняться построение. С помощью этих параметров можно регулировать конечный размер, а также абсолютное или относительное количество определённых конcтрукций в результирующей сети. На второй стадии с помощью автоматического итерационного процесса может быть сгенерирована сеть Петри любого размера, ограниченного оперативной памятью компьютера. В первом разделе статьи приводится необходимый минимум определений и вводится новый вариант операции композиции сетей Петри по местам. Свойства коммутативности и ассоциативности бинарного вида предложенной операции позволяют сливать несколько сетей Петри в произвольном порядке. Далее вводится понятие шаблонной конструкции в виде маркированной сети Петри, обладающей входным и выходным интерфейсами, а также правилами композиции шаблонных конструкций с использованием этих интерфейсов. Множество шаблонных конструкций объединяются в набор, для которого определяются правила эволюции. Свойство полноты набора гарантирует, что в результате эволюции набора будет получена сеть Петри, имитирующая поведение императивной программы. В статье приводится вариант полного набора шаблонных конструкций и пример генерации сети Петри, имитирующей последовательную императивную программу.
Статья публикуется в авторской редакции.