《嵌入式控制軟體的形式化規格說明構建的工程方法》是依託華東師範大學，由繆煒愷擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：嵌入式控制軟體的形式化規格說明構建的工程方法
- 項目類別：青年科學基金項目
- 項目負責人：繆煒愷
- 依託單位：華東師範大學
項目摘要,結題摘要,
項目摘要
針對形式化方法在工業界嵌入式控制軟體開發過程中難以有效套用的問題，本課題主要研究嵌入式控制軟體的形式化規格說明構建工程方法，建立工程化形式化規格說明構建過程，並通過規格說明審查和測試保障規格說明的一致性和有效性。主要研究內容包括：為嵌入式控制軟體形式化規格說明語言SPARDL提供與形式化語義一致的圖形化描述；建立圖形化描述引導的形式化規格說明工程化構建過程，引導開發者從原始需求出發通過不同階段構建形式化規格說明；研究規格說明審查以保證規格說明的一致性；研究規格說明測試技術以保證規格說明的有效性。研究測試用例生成、測試過程動畫模擬及測試結果分析等方法；開發相應的軟體工具。課題將豐富當前的形式化建模理論與方法，為工業界嵌入式控制軟體的開發者提供有效而實用的形式化規格說明構建工程方法。該課題對提高嵌入式控制軟體的質量有重要意義，研究成果可有效推動形式化方法在工業界嵌入式控制軟體開發中的實際套用。
結題摘要
在當前的工業界嵌入式控制軟體開發領域，形式化方法的實際套用仍面臨許多現實困難。從軟體需求分析角度看，存在如下主要問題：1)缺乏面向領域的合適的形式化建模語言。2)缺乏系統化的形式化規格說明構建的工程方法。3) 形式化規格說明有效性(validity)檢測手段不完善,效率低，缺乏實用的手段。 面對這一挑戰，我們提出一種構造嵌入式控制軟體形式規格說明的形式工程方法。受國家自然科學基金青年基金資助，課題執行期間取得了如下研究成果：1）提出了一種面向嵌入式控制軟體需求建模的輕量級形式化建模語言；2）結合形式化工程方法，建立了一種演化式的形式化模型構建方法，提高了形式化建模過程的效率；3）提出了一種基於圖形的需求審查方法，有效地提升了需求審查的錯誤探測能力；4）提出了一種基於場景的需求模型測試方法，支持在需求分析階段即可進行仿真分析；5）研發了面向軌道交通車輛控制軟體的需求建模工具，使得該方法在企業獲得直接套用，顯示了該方法具有明確的工程套用價值。
