目前用以保证系统设计品质的方法大致可分三种:传统的测试(testing)[BA00,KFNFN99]、模拟(simulation)[LK00]、与新近的技术:正规(formal)验证(verification)[CE81, CES86, Pnueli77]。测试是指在软/硬体产品已经生产出来后,将选定的输入信号送入待测物件(Device under Testing;DUT),以检验产品设计的正确与否。模拟则不需要用到实际的待测物件,而用一个数学模型代替,观察此数学模型的行为,以推断产品设计的正确与否。而最近渐渐受到重视的formal验证技术,则是完全在数学模型的抽象层次,企图证明系统设计架构的正确性。
“Formal”一词,缘起于“formal methods”,最早期的代表是IBM的维也纳研究中心所开发出来的VDM (Vienna Development Methods)[Jones90]技术,也就是用数学的符号,表达出系统设计的规格,从而减少工程师间错误沟通的可能性,进而提升系统设计的品质。 ... ...