嵌入式系统广泛应用于无人机、智能家居、医疗设备等领域。对可靠性,正确性和实时性的高要求是嵌入式系统的基本特征。伴随着嵌入式技术的发展,嵌入式系统的复杂程度不断提高且对时间的依赖性不断增强。为了保证系统的正确性和有效性,需要在嵌入式系统的设计中采用形式化的建模方法。Petri网是一种使用直观的图形方式和形式化的证明方式对系统进行建模和分析的数学模型。但是经典Petri网缺少时间特性和数据表达能力,不能对嵌入式系统的实时性要求和数据流进行很好地描述。基于Petri网表示的嵌入式系统PRES+(Petri net based Representation for Embedded Systems)网可以描述实时嵌入式系统,但是对复杂嵌入式系统建模较为繁琐且不直观。针对经典Petri网和PRES+网的这些缺点,本文将抑止弧加入PRES+网中,得到基于带抑止弧的Petri网表示的嵌入式系统PIRES+(Petri net with Inhibitor arcs based Representation for Embedded Systems)网。PIRES+网提高了建模和验证复杂嵌入式系统的能力,但是在建模和验证复杂嵌入式系统的过程中存在状态空间爆炸问题。为了缓解这一问题,对PIRES+网进行化简操作,提出多种PIRES+网的性质保持化简规则,使得简化后的PIRES+网与原网具有相同的可达性、实时性、功能性,活性和有界性。给出PIRES+网完全等价性概念和两个PIRES+网具有相同的可达性、功能性和实时性的条件。提出基于串联库所的化简规则、基于串联变迁的化简规则、基于具有相同输入输出库所的化简规则、基于特定变迁和库所的化简规则、基于T型子网的化简和基于P型子网的规则。在某些约束下,化简后的PIRES+网与原PIRES+网具有相同的可达性、功能性和实时性。通过对3个应用实例的化简说明了化简规则的有效性。提出PIRES+网的状态概念,给出PIRES+网的活性和有界性的形式化定义。分别证明基于P型子网和基于T型子网化简规则对活性和有界性的保持性。对基于嵌入式系统的报警实例进行分析和化简,说明了基于P型子网和基于T型子网化简规则的可行性和有效性。最后,将6种化简规则系统地应用于多参数监护仪系统,在性质保持的前提下减少库所和变迁的数量,在一定程度上缓解了网系统的状态空间爆炸问题。