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

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.

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

随着社会各个行业信息化程度不断提高，领域软件在很多行业的生产控制和业务管理过程中发挥着重要作用，领域软件的服务质量成为用户关注的核心。鉴于领域软件的重要性，构建高质量的领域软件，并持续保证其服务质量已经成为相关领域研究人员高度关注的问题。.本项目针对领域软件可信构建和质量评估中的关键问题进行研究，提出了一种基于规约语言的领域软件形式化程度度量方法，主要研究内容包括：研究度量证据的分析、形式化转化和量化，研究度量模型的构建，研究形式化程度等级的定义和映射，研究基于度量模型的领域软件可信构建与演化。重要研究进展和成果包括：建立了度量证据的分布层次分析框架，将软件生命周期中各个阶段和各个层次的度量证据分为功能需求证据、限制性证据、度量性证据三种类型进行研究，建立了度量证据的形式化描述和转化分析过程；建立了形式化程度的度量模型，研究了度量证据的获取和解析方法，以及度量证据在形式化分析和转化后的量化评价方法，基于度量需求、成本代价、技术条件描述度量计算逻辑，建立基于证据节点组合的度量模型；建立了形式化程度等级机制，基于度量模型建立细粒度、灵活的等级模型，模型中包括多个有序的等级及映射条件，映射条件是采用度量模型节点来描述形式化程度的各个等级，能够清晰地衡量领域软件的形式化程度；建立了基于度量模型的软件构建和演化框架，基于已经建立的度量模型、等级模型，分析和度量领域软件的形式化程度，基于度量数据分析领域软件存在的问题，指导领域软件的构建和演化工作。.本项目提出的领域软件形式化程度度量方法，具有较好的可操作性和可信性，能够量化地描述领域软件形式化程度，并支持基于度量模型和评估数据进行瓶颈问题分析和可信演化，为领域软件的质量评估分析和可信构建提供了形式化的支持。研究成果在电力和国防领域进行了初步的应用验证，能够在行业信息化过程中发挥重要作用，因此本项目研究成果具有较好的应用前景。