形式化方法

維基百科,自由的百科全書

形式化方法,中文也稱形式方法[1]正規方法[2]。在計算機科學軟件工程領域,形式化方法是基於數學的特種技術,適合於軟件硬件系統的描述開發驗證[3]。將形式化方法用於軟件和硬件設計,是期望能夠像其它工程學科一樣,使用適當的數學分析以提高設計可靠性強健性[4]。但是,由於採用形式化方法的成本高意味着它們通常只用於開發注重安全性的高度整合的系統[5]

參考文獻[編輯]

  1. ^ formal method - 形式方法. 雙語詞彙、學術名詞暨辭書資訊網. 國家教育研究院. [2020-09-05]. (原始內容存檔於2020-10-21). 
  2. ^ 郭大維. IEEE第四屆國際複雜系統工程研討會. 國立中正大學資訊工程學系. [2013-12-28]. (原始內容存檔於2013-12-30). 
  3. ^ R. W. Butler. What is Formal Methods?. 2001-08-06 [2006-11-16]. (原始內容存檔於2006-12-08). 
  4. ^ C. Michael Holloway. Why Engineers Should Consider Formal Methods (PDF). 16th Digital Avionics Systems Conference (27-30 October 1997). [2006-11-16]. (原始內容 (PDF)存檔於2006年11月16日). 
  5. ^ M. Archer, C. Heitmeyer and E. Riccobene. Proving invariants of I/O automata with TAME. Automated Software Engineering, 9, 201-232 (2002).