Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra  

作　　者：Dmitry A.Zaitsev Tatiana R.Shmeleva Jan Friso Groote 

机构地区：[1]IEEE [2]the Vistula University [3]the A.S. Popov Odessa National Academy of Telecommunications [4]the Eindhoven University of Technology

出　　处：《IEEE/CAA Journal of Automatica Sinica》2019年第3期733-742,共10页自动化学报（英文版）

基　　金：supported in part by NATO(ICS.NUKR.CLG982689)

摘　　要：A model of a hypertorus communication grid has been constructed in the form of an infinite Petri net. A grid cell represents either a packet switching device or a bioplast cell. A parametric expression is obtained to allow a finite specification of an infinite Petri net. To prove properties of an ideal communication protocol, we derive an infinite Diophantine system of equations from it, which is subsequently solved. Then we present the programs htgen and ht-mcrl2-gen, developed in the C language, which generate Petri net and process algebra models of a hypertorus with a given number of dimensions and grid size. These are the inputs for the respective modeling tools Tina and mCRL2, which provide model visualization, step simulation, state space generation and reduction, and structural analysis techniques. Benchmarks to compare the two approaches are obtained. An ad-hoc induction-like technique on invariants,obtained for a series of generated models, allows the calculation of a solution of the Diophantine system in a parametric form.It is proven that the basic solutions of the infinite system have been found and that the infinite Petri net is bounded and conservative. Some remarks regarding liveness and liveness enforcing techniques are also presented.A model of a hypertorus communication grid has been constructed in the form of an infinite Petri net. A grid cell represents either a packet switching device or a bioplast cell. A parametric expression is obtained to allow a finite specification of an infinite Petri net. To prove properties of an ideal communication protocol, we derive an infinite Diophantine system of equations from it, which is subsequently solved. Then we present the programs htgen and ht-mcrl2-gen, developed in the C language, which generate Petri net and process algebra models of a hypertorus with a given number of dimensions and grid size. These are the inputs for the respective modeling tools Tina and mCRL2, which provide model visualization, step simulation, state space generation and reduction, and structural analysis techniques. Benchmarks to compare the two approaches are obtained. An ad-hoc induction-like technique on invariants,obtained for a series of generated models, allows the calculation of a solution of the Diophantine system in a parametric form.It is proven that the basic solutions of the infinite system have been found and that the infinite Petri net is bounded and conservative. Some remarks regarding liveness and liveness enforcing techniques are also presented.

关 键 词：Computing grid conservativeness DEADLOCK hypertorus INFINITE PETRI NETS process ALGEBRA systems BIOLOGY 

分 类 号：TP[自动化与计算机技术]