基于规约语言的领域软件形式化程度度量方法研究

项目名称： 基于规约语言的领域软件形式化程度度量方法研究

项目编号： No.61472160

项目类型： 面上项目

立项/批准年度： 2015

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

项目作者： 包铁

作者单位： 吉林大学

项目金额： 80万元

中文摘要： 形式化方法是软件可靠性分析和高可靠软件构建的最有力工具，形式化方法的应用程度能够反映出软件的质量情况，目前仍然缺乏对形式化程度的系统的度量方法，因此本项目提出一种基于规约语言的领域软件形式化程度度量方法,并基于此方法辅助领域软件进行构建和演化。主要研究包括：分析形式化程度度量证据的分布层次，并对主要的形式化证据的描述与转化进行研究；通过获取、解析和评估度量证据生成标准评估证据，构建度量模型来表示度量需求；基于度量模型定义形式化等级机制，描述和映射领域软件形式化程度。 项目组在软件构建和形式化技术方面进行了大量基础研究工作，能够保证项目顺利进行。预期成果包括：提出领域软件形式化程度的度量方法，建立形式化评估模型和等级体系，建立基于该方法的领域软件可信构建和演化机制。项目研究能够清晰有效地描述领域软件的形式化程度，基于评估结果分析制约领域软件质量的瓶颈因素，为形式化地构建高可靠软件提供支持。

中文关键词： 软件度量；形式化程度；等级评估；规约语言

英文摘要： Formal method is the most powerful tool for software reliability analysis and high reliability software construction. The application degree of formal methods for software can reflect the quality of the the software. Yet，former researches didn't provide systematic measurement for the degree of domain software formalization.This project research on measurement for the degree of domain software formalization, an measure method for the degree of domain software formalization based on specification language is put forward, and the construction and evolution for domain software is conduct according to this method. The research topics include: analysis for location hierarchy of degree measure evidence of software formalization, and research on description and transformation of main formal evidence; generation of evaluation evidence through of requirement,resolve and evaluation to measure evidence, construction of measure model which can express measure requirement; definition for the formal rating mechanism based on measure model, descrption and mapping to degree of formalization. The project team have carrid out a lot of basic research on software construction and formalization technology. The solide early foundation will ensure that the project will succesfully complete. The main results include: the measure method for the degree of domain software formalization, construction of formal evaluation model and formal hierarchy, construction of reliable building and evolution mechanism for domain software based on the method.Due to the introduction of this method, not only the degree of domain software formalization will be described clearly, but bottleneck factors will be found for quality of domain software based on the evaluation conclusion. And full support will be also provided for formal construction for high reliability software.

英文关键词： Software Measurement;Degree of Formalization;Level Evaluation;Specification Language