基于Token选取的OpenStack单一平面网络建模方法

CPN形式化建模适合为包含大量并发、通信、同步共享行为的软硬件系统建立形式模型,并完成系统功能和性能等方面的行为分析。在传统的CPN建模中,token的选取采用穷举法,由此造成生成的token数量较多、CPN模型生成的状态空间相当庞大甚至状态空间爆炸等问题。针对上述问题,提出将符号执行与CPN建模相结合,并在CPN模型的执行过程中采用一种基于token选取的方法,进而得到CPN模型的状态可达图。通过对OpenStack云平台支持创建的单一平面网络进行CPN建模,针对传统方法和所提方法生成的状态空间,分析了其规模的变化,验证了所提方法的有效性。

Modeling OpenStack Single Plane Network Based on Token Selection

CPN suits for modelling the hardware and the software systems,which contain a large number behaviors of concurrencies,communication,synchronous sharing,and analyzing system function and performance.In CPN modelling,the traditional exhaustive method of selecting token is adopted,and the large number of token could cause that the generated state space is quite huge so as to bring reachability state explosion.On account of the above problem,this paper combined symbolic execution with CPN modelling,used selection method during the execution of the CPN model,and then obtained the reachability state space of the CPN model.Furthermore,a single plane network created by an OpenStack cloud platform was used as an example to be modeled,and the state space and reachability state generated by the traditional method and the new method were compared.The results show that the proposed method is effective.