根據Moore定律，硬體的複雜度是每十八個月增加一倍，而工程師的設計生產力卻跟不上這個速率。徒然增加設計團隊的人力，卻不能在根本的生產力工具上改進，只會提高整合的困難。這由目前各大型計畫，超過一半的預算是花在整合（integration）與驗證（verification）上，可以得知[Silburt98]。

目前用以保證系統設計品質的方法大致可分三種：傳統的測試（testing）[BA00,KFNFN99]、模擬（simulation）[LK00]、與新近的技術：正規（formal）驗證（verification）[CE81,CES86, Pnueli77]。測試是指在軟／硬體產品已經生產出來後，將選定的輸入信號送入待測物件（Device under Testing；DUT），以檢驗產品設計的正確與否。模擬則不需要用到實際的待測物件，而用一個數學模型代替，觀察此數學模型的行為，以推斷產品設計的正確與否。而最近漸漸受到重視的formal驗證技術，則是完全在數學模型的抽象層次，企圖證明系統設計架構的正確性。

“Formal”一詞，緣起於“formal methods”，最早期的代表是IBM的維也納研究中心所開發出來的VDM （Vienna Development Methods）[Jones90]技術，也就是用數學的符號，表達出系統設計的規格，從而減少工程師間錯誤溝通的可能性，進而提昇系統設計的品質。
...
...