随着多核处理器的发展，Ada并发程序已经普遍应用于现代嵌入式软件系统设计中，如何保证其正确性和可靠性成为一个十分重要的问题。模型检测验证并发程序已成为一种趋势，其关键问题是建模，通常采用手工方式，但是这种方式存在成本高、易引入模型错误等缺点。同时，模型检测还面临一个状态爆炸问题。因此，本文的主要研究工作着眼于利用程序切片技术减少状态，以及Ada程序的模型提取技术，实现使用模型检测工具SPIN自动检测Ada程序。针对模型提取技术，本文设计了一套对Ada程序提取PROMELA模型的方法，较好地处理了大部分Ada语言特性，比如创建类型和子类型、并发任务机制等。同时，实现了一个自动化模型提取工具AdaToSpin，分为词法分析、语法分析的分析模块和Ada到PROMELA的转换模块。针对状态爆炸问题，本文提出了一种基于LTL性质的Ada并发程序切片方法。分为三步：首先，分析程序中语句间的各种依赖关系，构造Ada程序的并发程序依赖图；其次，根据系统待验证的性质LTL公式，提取切片准则；最后，根据得到的依赖关系和切片准则，利用程序切片算法计算切片。同时，实现了一个Ada并发程序切片系统Ada_ProgramSlice。将程序切片技术应用于模型检测，有效的缩小状态空间。最后，根据本文的研究成果，结合实例验证了基于程序切片的Ada程序模型检测技术在自动提取模型和解决状态爆炸问题方面是有效的。