检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
机构地区:[1]内蒙古大学计算机学院,呼和浩特010021 [2]内蒙古大学网络信息中心,呼和浩特010021
出 处:《计算机科学》2016年第11期66-70,106,共6页Computer Science
基 金:国家自然科学基金项目(61163011;61262082)资助
摘 要:CPN形式化建模适合为包含大量并发、通信、同步共享行为的软硬件系统建立形式模型,并完成系统功能和性能等方面的行为分析。在传统的CPN建模中,token的选取采用穷举法,由此造成生成的token数量较多、CPN模型生成的状态空间相当庞大甚至状态空间爆炸等问题。针对上述问题,提出将符号执行与CPN建模相结合,并在CPN模型的执行过程中采用一种基于token选取的方法,进而得到CPN模型的状态可达图。通过对OpenStack云平台支持创建的单一平面网络进行CPN建模,针对传统方法和所提方法生成的状态空间,分析了其规模的变化,验证了所提方法的有效性。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.
关 键 词:CPN 符号执行 token选择 OPENSTACK 单一平面网络
分 类 号:TP393.1[自动化与计算机技术—计算机应用技术]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:216.73.216.215