形式化方法,中文也稱形式方法[1]、正規方法[2]。在計算機科學和軟件工程領域,形式化方法是基於數學的特種技術,適合於軟件和硬件系統的描述、開發和驗證[3]。將形式化方法用於軟件和硬件設計,是期望能夠像其它工程學科一樣,使用適當的數學分析以提高設計的可靠性和強健性[4]。但是,由於採用形式化方法的成本高意味着它們通常只用於開發注重安全性的高度整合的系統[5]。
M. Archer, C. Heitmeyer and E. Riccobene. Proving invariants of I/O automata with TAME. Automated Software Engineering, 9, 201-232 (2002).