軟體工程/質量/靜態分析簡介

靜態程式分析是指在不實際執行由該軟體構建的程式的情況下對計算機軟體進行的分析（對正在執行的程式進行的分析稱為動態分析）。在大多數情況下，分析是在原始碼的某個版本上進行的，而在其他情況下，則是在目的碼的某種形式上進行的。該術語通常應用於由自動化工具執行的分析，而人工分析被稱為程式理解、程式認知或程式碼審查。

工具執行的分析複雜程度各不相同，從僅考慮單個語句和宣告的行為，到在分析中包含程式的完整原始碼。從分析中獲得的資訊的使用範圍從突出顯示可能的編碼錯誤（例如 lint 工具）到形式化方法，這些方法在數學上證明了關於給定程式的屬性（例如，其行為與規範匹配）。

可以說，軟體度量和逆向工程是靜態分析的形式。

靜態分析在商業上的一個越來越多的應用是在驗證安全關鍵計算機系統中使用的軟體的屬性，以及定位可能存在漏洞的程式碼。例如，醫療軟體越來越複雜，美國食品藥品監督管理局（FDA）已將使用靜態程式碼分析作為提高軟體質量的一種手段。

形式化方法

形式化方法是應用於軟體（和硬體）分析的術語，其結果完全透過使用嚴格的數學方法獲得。使用的數學技術包括指稱語義、公理語義、操作語義和抽象解釋。

已證明，除了程式狀態空間是有限的假設之外，查詢所有可能的執行時錯誤，或者更一般地說，任何形式的違反程式最終結果規範的現象，都是不可判定的：不存在可以始終如一地正確回答給定程式是否可能或不可能出現執行時錯誤的機械方法。這一結果可以追溯到 1930 年代丘奇、庫爾特·哥德爾和圖靈的工作（見停機問題和 Rice 定理）。與大多數不可判定問題一樣，人們仍然可以嘗試給出有用的近似解。

形式化靜態分析的一些實現技術包括

• 模型檢驗考慮具有有限狀態或可以透過抽象簡化為有限狀態的系統；
• 資料流分析是一種基於格子的技術，用於收集有關可能值的集合的資訊；
• 抽象解釋模擬每個語句對抽象機器狀態的影響（即它基於每個語句和宣告的數學屬性來“執行”軟體）。這種抽象機器過擬合了系統的行為：因此，抽象系統變得更易於分析，但以不完整性為代價（並非原始系統的所有屬性都對抽象系統成立）。但是，如果執行得當，抽象解釋是可靠的（抽象系統的每個屬性都可以對映到原始系統的真實屬性）。Frama-c 框架和 Polyspace 很大程度上依賴於抽象解釋。
• 正如 Hoare 邏輯首先建議的那樣，在程式程式碼中使用斷言。有些程式語言有工具支援（例如，SPARK 程式語言（Ada 的一個子集）和 Java 建模語言 - JML - 使用 ESC/Java 和 ESC/Java2，以及 C 語言的 ANSI/ISO C 規範語言）。

參考書目

• 課程大綱和讀物，來自 Alex Aiken 的斯坦福 CS295 課程。
• Nathaniel Ayewah、David Hovemeyer、J. David Morgenthaler、John Penix、William Pugh，“使用靜態分析查詢錯誤” IEEE 軟體，第 25 卷，第 5 期，第 22-29 頁，2008 年 9/10 月，doi:10.1109/MS.2008.130
• Brian Chess、Jacob West（Fortify Software）（2007）。使用靜態分析進行安全程式設計. Addison-Wesley. ISBN 978-0321424778.
• Adam Kolawa（Parasoft），靜態分析最佳實踐 白皮書
• 透過精確的靜態和執行時分析改進軟體安全，Benjamin Livshits，第 7.3 節“用於安全性的靜態技術”，斯坦福博士論文，2006 年。
• Flemming Nielson、Hanne R. Nielson、Chris Hankin（1999 年，2004 年修正）。程式分析原理. 施普林格. ISBN 978-3540654100. {{cite book}}: 檢查日期值：|year= (幫助)CS1 maint: multiple names: authors list (link)
• “抽象解釋和靜態分析，” 2003 年語義學與應用國際冬季研討會，由 David A. Schmidt 主持

外部連結

• SAMATE 專案，自動化靜態分析工具資源
• 將靜態分析整合到軟體開發流程中
• 程式碼質量改進 - 編碼標準一致性檢查（DDJ）
• 第 59 期：靜態程式碼分析 採訪（播客）來自軟體工程廣播
• 為編碼標準實施自動化治理 解釋了為什麼以及如何將靜態程式碼分析整合到構建流程中