形式檢證

形式檢證 (Formal verification)은 하드웨어 및 소프트웨어 시스템의 脈絡에서 公式數學方法을 使用하여 特定形式仕樣 또는 屬性과 關聯하여 시스템의 正確性 을 證明 하거나 反證하는 行爲이다. ^[1] 形式檢證은 시스템의 形式仕樣을 위한 主要 인센티브이며 形式方法의 核心이다. 이는 電子設計自動化에서 分析 및 檢證의 重要한 次元을 나타내며 소프트웨어 檢證에 對한 한 가지 接近方式이다. 公式檢證을 使用하면 컴퓨터 保安認證에 對한 共通評價基準 프레임워크에서 가장 높은 評價保證水準(EAL7)李可能하다.

公式檢證은 暗號化 프로토콜, 組合回로, 內部 메모리가 있는 디지털 回로, 프로그래밍 言語의 소스 코드로 表現된 소프트웨어와 같은 시스템의 正確性을 立證하는 데 도움이 될 수 있다. 檢證된 소프트웨어 시스템의 代表的인 例로는 CompCert 檢證 C 컴파일러 와 seL4 높은 保證運營體制 커널 이 있다.

이러한 시스템의 檢證은 시스템의 數學的 모델 에 對한 公式的인 證據가 存在하는지 確認함으로써 遂行된다. ^[2] 시스템을 모델링하는 데 使用되는 數學的個體의 例로는 有限狀態機械 , 레이블이 있는 轉換 시스템, 魂節, 페트리 넷, 벡터 追加 시스템, 時間制限 오토마타, 하이브리드 오토마타, 프로세스 臺數, 프로그래밍 言語의 形式意味(예: 演算意味論, 標示意味論, 功利的意味論 및 호어 論理 ) 等이 있다. ^[3]

같이 보기 [ 編輯 ]

各州 [ 編輯 ]

↑ Sanghavi, Alok (2010年 5月 21日). “What is formal verification?”. 《EE Times Asia》.
↑ Sanjit A. Seshia; Natasha Sharygina; Stavros Tripakis (2018). 〈Chapter 3: Modeling for Verification〉. Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick. 《Handbook of Model Checking》 . Springer. 75?105쪽. doi : 10.1007/978-3-319-10575-8 . ISBN 978-3-319-10574-1 .
↑ Introduction to Formal Verification , Berkeley University of California, Retrieved November 6, 2013

[1] Sanghavi, Alok (2010年 5月 21日). “What is formal verification?”. 《EE Times Asia》.

[2] Sanjit A. Seshia; Natasha Sharygina; Stavros Tripakis (2018). 〈Chapter 3: Modeling for Verification〉. Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick. 《Handbook of Model Checking》 . Springer. 75?105쪽. doi : 10.1007/978-3-319-10575-8 . ISBN 978-3-319-10574-1 .

[3] Introduction to Formal Verification , Berkeley University of California, Retrieved November 6, 2013

[1]

[2]

[3]