有色Petri网作为一类特殊的Petri网模型语言,特别适用于并发、同步和资源共享起主要作用的系统。它结合了一般Petri网过程互操作特性和高级程序语言的数据类型定义及数据处理的能力。CPNs有比较正式的形式化定义及其解释,还包括一系列动态行为属性。Petri网是事件驱动系统建模的十分有用的工具。这些系统可以是异步的,可能包括顺序的和并行的操作,并可能涉及冲突、互斥及非确定性。有色Petri网增强了Petri网描述系统的能力。状态空间分析和性能分析是用CPNs进行生产过程分析的两个重要技术。一般地,为了便于进行状态空间分析,首先要对需要分析的CPNs模型作某些修改,从而得到一个包含有限状态空间的CPNs模型。虽然状态空间分析是进行业务过程分析的两个重要技术之一,但是如何从理论上借助状态空间分析去判定CPNs的各种动态属性,这方面的研究还少之又少。在这篇论文中,借助于状态空间分析从理论上研究了CPNs的各种动态属性的判定方法,从而为手工验证CPNs的各种动态属性提供理论基础。另外,本文用CPNs形式化描述方法来实现组装生产线模型,力图提供一套一致、简单、有效、充分的形式化方法来表示存在于组装生产过程中产生的逻辑关系。其最终目的是要达到：1)从实现角度提高组装生产线系统的研究效率；2)提高系统的可理解性和可维护性。最后,通过状态空间分析进行动态属性验证,得到系统模型的行为属性分析结果。