针对形式化方法在工业界嵌入式控制软件开发过程中难以有效应用的问题，本课题主要研究嵌入式控制软件的形式化规格说明构建工程方法，建立工程化形式化规格说明构建过程，并通过规格说明审查和测试保障规格说明的一致性和有效性。主要研究内容包括：为嵌入式控制软件形式化规格说明语言SPARDL提供与形式化语义一致的图形化描述；建立图形化描述引导的形式化规格说明工程化构建过程，引导开发者从原始需求出发通过不同阶段构建形式化规格说明；研究规格说明审查以保证规格说明的一致性；研究规格说明测试技术以保证规格说明的有效性。研究测试用例生成、测试过程动画模拟及测试结果分析等方法；开发相应的软件工具。课题将丰富当前的形式化建模理论与方法，为工业界嵌入式控制软件的开发者提供有效而实用的形式化规格说明构建工程方法。该课题对提高嵌入式控制软件的质量有重要意义，研究成果可有效推动形式化方法在工业界嵌入式控制软件开发中的实际应用。
