嵌入式控制软件的形式化规格说明构建的工程方法

The application of formal methods to industry embedded control software development is not adequately effective as people expected. To tackle this challenge, this project focuses on an engineering method for constructing formal specification of embedded control software. We establish an engineering process for formal specification construction and offer specification review and testing technologies to ensure the consistency and validity of the formal specification. Specifically, our research includes following issues: providing graphic notations with consistent formal semantics for the SPARDL formal specification language; establishing a diagram guided engineering process for formal specification construction to guide the developer construct formal specification from the scratch via particular modeling phases; developing a set of specification review and testing techniques to ensure the consistency and validity of specification; exploring test case generation, animation of testing and test result analysis techniques. We also develop software tools to support our proposed engineering method. This research will enrich both formal modeling theories and methods, and provide industry practitioners with an effective and practical engineering method for formal specification construction. It is also of great significance to quality of embedded control software. The research results can effectively promote the application of formal methods in industry software development.

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

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