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)上发表.