软件系统的开发是一个包含可行性分析、需求分析、编码、执行、测试、运行维护等多个阶段的复杂过程。特别是开发分布式的、具有并行性、时间性、不确定性等特点的系统更具有挑战性。很多该类软件系统在初始搭建时没有充分考虑是否满足相应的性质要求和性能标准,而是在软件实现之后才来测量评估,当发现问题时,必须从头开始修改软件设计,因此对大型软件系统的开发势必会付出很大的代价,导致进度延误、生产效率降低。因此,软件系统的建模与性质分析验证成为软件工程领域的一个研究热点。目前为止,多种建模方法已经被广泛地应用于软件系统的开发过程中,其中主要包括结构化建模方法、形式化建模方法、面向对象建模方法以及统一建模语言(UML)等。这些方法在软件开发过程中发挥了一定的作用,有些方法也得到了广泛的认可和使用,但也都存在着一定的缺点,如对系统性质缺乏有效的分析验证。着色Petri网作为一种高级Petri网,在保持传统Petri网严格的数学定义的基础上,又与Standard ML相结合,引入了颜色集、变量等元素,加之成熟的计算机辅助工具CPN Tools的帮助,使其在大型系统的建模仿真以及性能分析方面,特别是针对分布式的具有并发、异步特性的系统发挥着越来越大的作用。本文对几种比较流行的传统建模方法进行深入的研究,在对其优缺点进行对比分析的基础之上,提出了基于着色Petri网的建模与系统性质分析验证方法。详细阐述了着色Petri网基本概念、建模方法与建模过程以及四种常用的基于着色Petri网的系统性质分析验证方法。本文的主要工作包括,首先深入研究传统的并行任务调度算法,然后以传统并行任务调度为基础为其建立CPN模型,分析讨论利用着色Petri网建立系统模型的方法与过程,最后通过仿真执行、可达树、关联矩阵以及状态空间分析等方法对其性质进行分析验证。本文对于深入开展软件系统建模方法的研究提供了一种新的思路,对提高软件系统的设计开发效率和可靠性具有一定的理论和实践价值。