嵌入式控制软件是当前诸多控制系统的核心部件.各类安全攸关系统,例如轨道交通系统、航空航天系统和核电控制系统等,其内嵌的控制软件的功能是否正确、安全直接关系到人们的生命与财产安全.经过长期的研究和实践,学术界和工业界都意识到系统需求作为软件工程生命周期的起始点,是确保软件质量的根本途径.因此,如何从源头上保障软件开发流程的正确性一直以来是软件工程领域重要的研究课题.然而,在工业界的软件开发中,系统需求的正确性只能靠人工审查来保证,人工审查自然语言系统需求的方法不但低效,而且无法确认需求的正确性,仍缺少一种对需求进行确认的形式化建模分析方法.需求确认是保障所构建的形式化规约质量的重要工程活动,而量纲分析作为需求确认中的一个重要手段,可以检查出因量纲的错误定义而产生的潜在缺陷,减少因量纲使用不当所造成的错误.基于此,我们针对轨道交通领域的特点,提出了一种基于形式化工程方法的需求建模与量纲分析研究,结合软件需求工程的基本原理,从原始需求出发逐步完成需求规约的构建,并给出了需求规约确认的其中一种方法,以确认软件需求规约准确、充分地描述人们对软件期望的功能,为该领域的需求分析提供保障.本文的主要贡献是:(1)提出了一种嵌入式控制软件需求建模的形式化工程方法;(2)提出了一种列车控制领域专用的需求描述语言ATPRDL(Automatic Train Protection Requirement Description Language),并对相应的需求文档进行建模;(3)针对嵌入式控制软件的特点,提出了一种领域专用的面向需求层的量纲分析方法,并构建了领域适用的量纲系统;(4)开发了一款工具用于支撑该方法的实际应用,使工程师可以快捷地进行量纲分析.通过应用本文提出的方法,我们对真实的轨道交通列车控制软件的需求进行了实验,实验结果表明此方法具有良好的可用性,并在实际的列车控制软件开发项目中,展现了优于工业界传统手工审查方法的缺陷发现能力和时间效率.