基於規約語言的領域軟體形式化程度度量方法研究

《基於規約語言的領域軟體形式化程度度量方法研究》是依託吉林大學，由包鐵擔任項目負責人的面上項目。

基本介紹

• 中文名：基於規約語言的領域軟體形式化程度度量方法研究
• 項目類別：面上項目
• 項目負責人：包鐵
• 依託單位：吉林大學

項目摘要

形式化方法是軟體可靠性分析和高可靠軟體構建的最有力工具，形式化方法的套用程度能夠反映出軟體的質量情況，目前仍然缺乏對形式化程度的系統的度量方法，因此本項目提出一種基於規約語言的領域軟體形式化程度度量方法,並基於此方法輔助領域軟體進行構建和演化。主要研究包括：分析形式化程度度量證據的分布層次，並對主要的形式化證據的描述與轉化進行研究；通過獲取、解析和評估度量證據生成標準評估證據，構建度量模型來表示度量需求；基於度量模型定義形式化等級機制，描述和映射領域軟體形式化程度。 項目組在軟體構建和形式化技術方面進行了大量基礎研究工作，能夠保證項目順利進行。預期成果包括：提出領域軟體形式化程度的度量方法，建立形式化評估模型和等級體系，建立基於該方法的領域軟體可信構建和演化機制。項目研究能夠清晰有效地描述領域軟體的形式化程度，基於評估結果分析制約領域軟體質量的瓶頸因素，為形式化地構建高可靠軟體提供支持。

結題摘要

隨著社會各個行業信息化程度不斷提高，領域軟體在很多行業的生產控制和業務管理過程中發揮著重要作用，領域軟體的服務質量成為用戶關注的核心。鑒於領域軟體的重要性，構建高質量的領域軟體，並持續保證其服務質量已經成為相關領域研究人員高度關注的問題。 本項目針對領域軟體可信構建和質量評估中的關鍵問題進行研究，提出了一種基於規約語言的領域軟體形式化程度度量方法，主要研究內容包括：研究度量證據的分析、形式化轉化和量化，研究度量模型的構建，研究形式化程度等級的定義和映射，研究基於度量模型的領域軟體可信構建與演化。重要研究進展和成果包括：建立了度量證據的分布層次分析框架，將軟體生命周期中各個階段和各個層次的度量證據分為功能需求證據、限制性證據、度量性證據三種類型進行研究，建立了度量證據的形式化描述和轉化分析過程；建立了形式化程度的度量模型，研究了度量證據的獲取和解析方法，以及度量證據在形式化分析和轉化後的量化評價方法，基於度量需求、成本代價、技術條件描述度量計算邏輯，建立基於證據節點組合的度量模型；建立了形式化程度等級機制，基於度量模型建立細粒度、靈活的等級模型，模型中包括多個有序的等級及映射條件，映射條件是採用度量模型節點來描述形式化程度的各個等級，能夠清晰地衡量領域軟體的形式化程度；建立了基於度量模型的軟體構建和演化框架，基於已經建立的度量模型、等級模型，分析和度量領域軟體的形式化程度，基於度量數據分析領域軟體存在的問題，指導領域軟體的構建和演化工作。 本項目提出的領域軟體形式化程度度量方法，具有較好的可操作性和可信性，能夠量化地描述領域軟體形式化程度，並支持基於度量模型和評估數據進行瓶頸問題分析和可信演化，為領域軟體的質量評估分析和可信構建提供了形式化的支持。研究成果在電力和國防領域進行了初步的套用驗證，能夠在行業信息化過程中發揮重要作用，因此本項目研究成果具有較好的套用前景。