Formal Verification of Software Source Code

View Statistics Email Alert RSS Feed

Information

Details

Project title

Code/計畫編號

NSC95-2221-E019-035

Translated Name/計畫中文名

軟體程式碼的正規驗證

Project Coordinator/計畫主持人

Yee-Jsong Juan

Funding Organization/主管機關

National Science and Technology Council

Department/Unit

Department of Computer Science and Engineering

Website

https://www.grb.gov.tw/search/planDetail?id=1311003

Year

2006

Start date/計畫起

31-08-2006

Expected Completion/計畫迄

31-07-2007

Bugetid/研究經費

511千元

ResearchField/研究領域

資訊科學--軟體

報告到CERT[41]的軟體安全事件從1998 到2002 已增加了2,099%。另外根據計算機經濟學的報告, 在2004 年全世界軟體缺陷的經濟影響已經達到幾十億美元。很多軟體產品的生產已經被嚴重延誤, 例如Windows Server 2003 因為缺陷問題被延誤9 個月上市。相同的軟體問題也嚴重發生在現下的台灣。主要原因導致軟體的不幸包括1)軟體產品的越來越高的複雜性2)今天的開放式網路環境。在軟體裡的一個bug 至少是一個DoS (Denial of Service)攻擊的隱藏危機。同樣問題將繼續存在[1], 因為我們在軟體理解和減輕軟體危險的工作做的不夠好。越來越多嚴重的軟體問題在最近和將來將繼續發生。我們必需投入更多的工作才能生產好的軟體給用戶安心。新近的研究[5-16]已經顯示, 軟體正規驗證技術對發現軟體的缺陷非常有用。另外的研究顯示[3] 在2001 年鑑定的軟體安全性的缺陷種類中, 多於半數理論上可被軟體正規驗證技術找出來。此研究計劃將發展新的軟體程式碼的正規驗證技術。我們的技術將降低軟體系統在實際上面臨的主要缺陷問題。我們的技術將增強軟體系統的可靠性和增加軟體的生產力以及減少軟體開發的時間。另外此研究計劃所發展出的軟體正規驗證技術工具將對台灣自由軟體[41]的發展有重要的貢獻。

Keyword(s)

軟體缺陷
程式碼
軟體正規驗證技術
bug
開放式網路
自由軟體
高效率分析

DSpace CRIS

Formal Verification of Software Source Code

Details

Description