导　　师： 李文军

学科专业： H1202

授予学位： 硕士

作　　者： ;

机构地区： 中山大学

摘　　要： PETRI网是描述和分析并行与分布系统的有力工具,为扩展PETRI网的建模与分析能力,使之能够处理时间相关的问题,人们将时间约束引入PETRI网模型中,形成带时间约束的PETRI网.MERLIN定义的时间PETRI网就是其中最常用的形式化模型之一.由于MERLIN模型采用强时间语义,冲突变迁的选择会受到时间约束影响,因此无法有效建模外部环境触发的冲突选择,而且可调度分析能力也受到局限.为此,本文提出一种新的时间PETRI网模型——基于弱时间语义选择的时间PETRI网,并给出它的形式语义、可达性分析方法和工具设计.本文的主要贡献有:(1)提出基于弱时间语义选择的时间PETRI网模型,该模型允许冲突变迁的持续使能时间超过它的时间上界,因此任何冲突变迁都有被选择的可能,从而解决了MERLIN模型建模外部环境触发的冲突选择上的不足.(2)利用时间变迁系统(TIMED TRANSITON SYSTEM)给出基于弱时间语义选择的时间PETRI网的语义,并在此基础上证明了MERLIN模型的状态集是该模型状态集的子集.(3)利用时间戳状态类的概念,给出基于弱时间语义选择的时间PETRI网模型的可达性分析方法,并证明通过该方法得到的全局时间戳满足合理性与完备性.(4)使用XML作为时间PETRI网的定义语言,采用分离时间类型与PETRI网的设计思想,使工具的实现更具扩展性.本文的主要工作已在第十届联合国际计算机会议(JICC2004)上发表.

关 键 词： 时间 网 弱时间语义 选择 可达性分析

分 类 号： [TP393]

领　　域： [自动化与计算机技术] [自动化与计算机技术]