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

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

项目编号： No.61402178

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 缪炜恺

作者单位： 华东师范大学

项目金额： 24万元

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

中文关键词： 形式化工程方法；形式化规格说明；需求工程；需求确认；规格说明分析

英文摘要： 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 c

英文关键词： formal engineering methods；formal specification；requirements engineering；requirements validation；specification analysis