《面向數值程式安全性與魯棒性的抽象解釋技術》是依託中國人民解放軍國防科技大學，由陳立前擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：面向數值程式安全性與魯棒性的抽象解釋技術
- 項目類別：青年科學基金項目
- 項目負責人：陳立前
- 依託單位：中國人民解放軍國防科技大學
中文摘要,結題摘要,
中文摘要
計算機軟體尤其是嵌入式軟體的設計與運行，與系統及環境的數學與物理模型密不可分，往往會涉及大量數值運算。計算機軟體的許多可信性質和程式缺陷與程式中的數值性質密切相關。因此，研究數值程式安全性與魯棒性的分析方法，對提高軟體的可信性具有重要意義。本項目針對計算機中數值程式的特點，即數值數據類型值表示範圍的有限性、浮點運算的不精確性、輸入數據伴隨的非確定性等特點，面向數值程式的安全性與魯棒性，以抽象解釋為理論支撐，開展相關靜態分析技術研究。擬突破數值不變式生成、數值程式的安全性與魯棒性分析等關鍵技術，力求在新型數值抽象域設計、浮點程式分析、命令式程式魯棒性分析等關鍵科學問題的研究中獲得進展和突破，設計並實現相應的數值程式分析工具原型，針對航空航天等領域典型嵌入式軟體的數值相關性質進行示範套用。本項目將形成面向數值程式的靜態分析方法、技術和工具，對計算機軟體的可信保障具有重要實際套用價值。
結題摘要
軟體的可信性已成為現代軟體質量問題的焦點。計算機軟體尤其是嵌入式軟體的設計與運行，與系統及環境的數學物理模型密不可分，往往會涉及大量數值運算。因此，計算機軟體中的許多可信性質（如輸出的有界性）或缺陷（如除零錯、算術溢出、數組越界等常見運行時錯誤）往往和程式中的數值性質密切相關。本項目針對計算機中數值程式的特點，即數值型數據類型值表示範圍的有限性、浮點運算的非精確性、輸入數據伴隨的非確定性等特點，以抽象解釋為理論支撐，從源程式級別，面向數值程式的安全性與魯棒性開展分析與驗證技術研究。 經過三年的研究，項目組依據計畫，完成了各項研究內容，達到了預期的研究目標。在面向數值不變式生成的新型數值抽象域的設計與實現、套用相關數值程式安全性的分析、數值程式魯棒性的分析、數值程式分析工具原型的設計與實現等方面形成了較為系統、深入的研究成果，在基準測試程式和航天工業代碼上的套用驗證了項目成果的有效性。進展要點如下： (1) 針對已有數值抽象域在表達能力方面存在的凸性局限性，提出了多種能夠表達非凸性質的數值抽象域，包括絕對值八邊形抽象域、區間冪集抽象域等； (2) 針對中斷機制在數值運算密集型嵌入式控制軟體中廣泛使用的特徵，提出了面向中斷驅動型程式的可靠數值性質分析方法； (3) 針對浮點計算不精確性導致的程式魯棒性問題，提出了面向浮點程式的基於自組合的魯棒性分析方法； (4) 設計並實現了一個面向C程式的數值程式分析工具原型CAI，支持程式中數值相關運行時錯誤的檢測； (5) 在基準測試程式以及航天工業代碼上開展了實驗驗證，驗證了方法的有效性。 至2015年，共發表學術論文9篇，其中SCI收錄2篇，EI收錄5篇。部分論文發表在Science of Computer Programming、SAS 2014、EMSOFT 2015等程式語言與嵌入式軟體領域的重要國際期刊會議上，並有一篇論文獲得EMSOFT 2015最佳論文提名。目前，發表的論文已被牛津大學、倫敦大學瑪麗皇后學院、巴黎高等師範學院、慕尼黑工業大學等大學的同行學者引用。
