OSEK/VDX作为分布式实时系统的标准,已被汽车电子行业广泛采用。为提高汽车的整体性能,应用程序的设计趋于并行和复杂化,OSEK/VDX程序的正确性验证得到了越来越多的关注。车载OSEK/VDX应用程序的验证方法目前主要是测试和模型检验。然而,由于并行程序在运行过程中存在的高度不确定性及交互复杂性,传统验证方法存在测试不完备与状态爆炸等问题。针对上述问题,本文提出一种基于Petri网及其展开的OSEK/VDX程序建模与验证方法。主要研究内容如下:(1)给出一种基于颜色Petri网的OSEK/VDX关键组件与应用程序建模方法,可根据具体的应用程序构建相应的Petri网模型;(2)提出颜色Petri网的展开与反向展开方法,给出了具体的展开与反向展开算法。进而,将系统中并发任务安全性验证问题转换为Petri网目标标识的可覆盖性问题,并借助所提出的反向展开技术实现了 OSEK/VDX应用程序部分安全性问题的验证。相比传统的验证方法,本方法可以有效缩小需搜索的状态空间、缓解状态爆炸问题。(3)时间因素是影响OSEK/VDX应用程序安全性的一个重要指标,传统基于Petri网的程序验证方法往往忽略时间属性。本文将时间要素引入基于Petri网的OSEK/VDX应用程序建模方法中,给出考虑时间因素后的OSEK/VDX程序正确性验证问题。在此基础上,借助颜色Petri网的展开与反向展开技术对程序的死锁、任务安全性与任务同步等问题进行了分析。