一種基于狀態機的形式化驗證技術
2008-12-31 00:00:00林敬恩滕忠堅陳圣群
電腦知識與技術 2008年13期
摘要：狀態機作為一種描述實體間交互或者單個實體行為的建模圖，它具有豐富的直觀圖形化的符號。在許多模型的設計階段都采用它來建模。但是因為缺乏精確完整的語義定義，給它的形式化驗證帶來困難。本文給出一種形式化操作語義，并概述基于形式化規則的驗證技術。
關鍵詞：狀態機；操作語義；建模；驗證技術
中圖分類號：TP331 文獻標識碼：A 文章編號：1009-3044(2008)13-20720-03
