基于 ASK-CTL 的有色 Petri 网模型检验算法研究

来源 :计算机应用与软件 | 被引量 : 0次 | 上传用户：wjkylin

【摘要】

：

针对使用CPN Tools工具建立系统CPN(Colored Petri Net)模型并进行仿真所得到的状态空间报告中出现的死标识是否会影响系统的安全性和模型的正确性进行研究,提出基于ASK-CTL的有色Petri网模型检验算法及死标识合理性验证算法。算法描述了系统有色Petri网的建模与仿真过程,根据得到的状态空间报告判断是否存在死标识,对存在的死标识采用非标准状态空间查询法使用ML语言编辑相关

【作者】

：

马国富刘文良周建勇刘久富

【机构】

：

安阳工学院信息工程系,南京航空航天大学自动化学院

【出处】

：

计算机应用与软件

【发表日期】

：

2015年10期

【关键词】

：

模型检验死标识电梯门系统 CPN 模型 Model checkingDeadMarkinsElevator door systemCPN model

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

其他文献

一种改进的Condensation人脸特征点跟踪算法

Condensation跟踪算法只能完成一些简单的目标跟踪。由于人脸容易出现被遮挡,姿态和表情也经常发生变化,导致人脸特征点极易跟踪失败。针对这些复杂变化,提出一种改进的Condensation人脸特征点跟踪算法。该算法对跟踪的特征点利用增量PCA方法实现特征基和均值的在线更新,同时,加入一个遗忘因子,使得在新样本的更新过程中,考虑了旧样本的存在,更新了均值。实验证明,该算法可以有效地克服复杂变化

期刊

人脸特征点跟踪增量PCA更新CONDENSATION遗忘因子Facial feature point tracking Incremental PCA

基于功能的惯性平台机内测试技术

针对新型惯导平台的发展要求,结合机内测试技术对惯导平台进行了研究,通过深入分析平台的工作原理、测试方法、机内测试的原则,利用DSP+FPGA的技术和多传感器冗余知识对平台

期刊

惯性平台机内测试信息冗余

基于业务安全性的电力通信网双路由配置方法研究

针对现有电力通信业务路由配置方法集中于单路由算法无法从根本上保证信息安全传输的问题,提出基于业务安全性的最佳双路由算法ODR(Optimal Double Route),为每一条业务配置两条安全性最高的节点分离路径。首先,综合考虑站点和光缆的安全性,以及电力通信网的特殊性,构建通信网业务的双路由问题模型。其次,根据该问题模型改进Bhandari算法实现节点分离路径对的搜索。最后,通过实例测试业务配

期刊

安全性双路由电力通信业务节点分离路径SecurityDual-routePower communication servicesNode-disjoin

基于空间关系的改进菱形块匹配策略

研究运动估计(ME)中的经典块匹配算法(BMA)并重点分析菱形(DS)算法,然后利用相邻块之间空间关系,设计一种新的块匹配策略,以相邻宏块的搜索结果进行预测匹配,以减少搜索点数。最后以平均每块搜索点数和平均峰值信噪比为衡量指标验证了该算法的有效性。

期刊

块匹配运动估计菱形算法视频压缩Block matchMotion estimationDiamond algorithmVideo compressio

浅谈新形势下的高校系科领导班子建设

高校的系科领导班子建设是高校党的建设和思想政治工作的重要内容.当前,加强高校的系科领导班子建设,就是要按照江泽民总书记"三个代表"的要求,切实加强思想、组织和作风建设

期刊

领导班子建设高校“三个代表”重要思想思想政治工作党的建设作风建设江泽民

基于 ASK-CTL 的有色 Petri 网模型检验算法研究

与本文相关的学术论文