根据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]技术，也就是用数学的符号，表达出系统设计的规格，从而减少工程师间错误沟通的可能性，进而提升系统设计的品质。
...
...