摘  要

        随着人们要求的日益增高，现代汽车集成各种各样复杂的应用，在应用程序与硬件之间加入操作系统成为必然。如何验证带操作系统的汽车电子软件的实时性成了许多研究人员共同关注的问题。
        对于嵌入式系统实时性的验证，形式化推理分析与模型分析是现存的两大最重要的方法，但前者往往分析过程比较复杂，且没有直观的运行界面，不能模拟整个系统的真实运行情况。而模型分析方法则形式各异，各有所长。PETRI网适合于描述异步的、并发的计算机系统模型，它既有严格的数学表述方式，也有直观的图形运行界面，能分析系统的实时性、可靠性等各种性能。
        本文在TOPPERS操作系统基础上，以汽车自适应巡航控制系统为例，分析得出一种汽车电子软件的实时性验证方法。
        文章首先分别阐述现代汽车电子系统和车载操作系统的发展，并归纳总结对于实时性的验证所存在的方法，包括形式化推理、时间自动机、AADL建模等；接着文章在分析Petri网的时间扩展与性质基础上，得出一种利用时间Petri网来验证汽车电子系统实时性的方法，并制定从带时间参数的状态转换图到时间Petri网的映射规则；然后在TOPPERS操作系统的基础上设计实现验证实例汽车自适应巡航控制系统，并测试相关的任务运行时间；最后建立汽车自适应巡航控制系统相对应的时间Petri网模型，通过验证工具EXSPECT运行模型系统，在两种不同模式下分别分析验证其实时性并进行相关方面的比较。
        结果显示本文所提出的验证汽车电子软件实时性的方法能准确得出整个系统运行所耗费的时间，与传统的系统实时性验证方法相比，本文的方法通过一定的优化策略降低系统的复杂度，且能更直接的模拟系统的运行情况，并准确得出时间参数。

论文报告