在当前的工业界嵌入式控制软件开发领域，形式化方法的实际应用仍面临许多现实困难。从软件需求分析角度看，存在如下主要问题：1)缺乏面向领域的合适的形式化建模语言。2)缺乏系统化的形式化规格说明构建的工程方法。3) 形式化规格说明有效性(validity)检测手段不完善,效率低，缺乏实用的手段。 面对这一挑战，我们提出一种构造嵌入式控制软件形式规格说明的形式工程方法。受国家自然科学基金青年基金资助，课题执行期间取得了如下研究成果：1）提出了一种面向嵌入式控制软件需求建模的轻量级形式化建模语言；2）结合形式化工程方法，建立了一种演化式的形式化模型构建方法，提高了形式化建模过程的效率；3）提出了一种基于图形的需求审查方法，有效地提升了需求审查的错误探测能力；4）提出了一种基于场景的需求模型测试方法，支持在需求分析阶段即可进行仿真分析；5）研发了面向轨道交通车辆控制软件的需求建模工具，使得该方法在企业获得直接应用，显示了该方法具有明确的工程应用价值。