随着处理器的计算能力的迅速提高、嵌入式技术的迅猛发展和嵌入式系统应用领域的不断拓宽，使得嵌入式软件的规模以及复杂性的不断增长，从而导致了开发时间和费用也在不断的增长，如何快速有效的开发嵌入式软件成为目前亟待解决的问题。为了解决上面的问题，全球最大的软件工业标准化组织OMG(Object Management Group)提出了模型驱动框架MDA(Model Driven Architecture)开发方法。MDA方法将软件开发过程分成两个主要阶段：模型级和代码级。模型主要关注系统的设计正确性，从而达到以较小代价修改软件错误的目的。　　 面向嵌入式软件的开发工具目前正在从基于代码的传统开发环境向基于模型的开发环境发展。而一个基于模型的嵌入式生产线开发环境，应该是集成模型开发工具和其他相关工具，包含了建模、模型仿真验证、代码生成、测试等嵌入式软件开发的全过程。这符合嵌入式软件开发工具发展趋势，也具备相应的理论、技术和产品基础。　　 模型驱动验证是基于模型的嵌入式软件生产线的一个重要部分，这个关键部分会影响到系统的质量和后期的工作，如果在前期能够及时发现出存在的问题，可以节省大量的人力物力。当今主流的嵌入式实时系统中，实时性是一个关键的性能指标，对于这类系统就是要求它们在合法的时间内完成相应的行为，不会发生超时现象，这就要求验证任务间的可调度性来判断系统实时性是否符合要求。由Clark和Emerson提出形式化的模型验证的方法以开始应用在任务的可调度分析上，该方法的基本原理是为要检测的系统建立形式化模型，阐明所要验证的性质，然后使用算法去检查该模型是否满足所述性质。　　 本文的研究是基于模型的软件嵌入式生产线开发环境，在这条主线上把重点放在研究和解决模型方面的形式化验证问题，对嵌入式模型实时性中的可调度问题进行研究。　　 论文先介绍了基于模型的嵌入式软件生产线的背景与意义，并分析了国内外的发展情况，接着说明课题的来源和本文研究的内容；在此基础上提出基于模型的嵌入式生成线的总体需求分析；接着重点介绍模型验证调度检测工具SCT(Scheduling CheckTool)的设计，包括SCT所分析的系统的相关定义和规定以及任务的两个行为自动机模型的设计实现，在这些前提下对SCT工具进行总体设计，并对每部分进行实现，其中重点放在调度仿真算法进行设计与实现；接着在LambdaPRO的基础上集成相关工具，实现基于模型的嵌入式软件生成线的整个开发过程，并通过一个实例应用来说明验证这个开发流程。论文最后对本文的工作进行总结，并对后继研究和发展进行了展望。