Model Checking

2007 年的 Turing Award 得主前幾天剛剛公佈，這次頒給三個人 Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis，他們做的是 model checking。這門神奇的學問剛好在去年 FLOLAC '07 王老師開了一門課介紹。我們玩的第一套軟體是 Spin，可以用指定的程式語言描述一個 protocol，然後自動驗證這套 protocol 是否滿足給定的 linear temporal logic formulae。Temporal logic 是一類帶有時間描述與推論的邏輯，在這類邏輯下我們可以表示「永遠」、「終會」、「在某事成真前」的概念，所以就可以表述像「永遠不可能有兩個以上的 processes 都在 critical region 裡面」、「永遠都有 process 終究能夠進入 critical region」的陳述。我們試了 Peterson's algorithm 和 bakery algorithm（among others），後者的一般實作還被抓出錯誤（這時會把導致錯誤的執行方式顯示出來！），因為原始的 bakery algorithm 用的號碼牌必須是 unbounded integers。總之真的是很神奇（也很難，我把它封為 FLOLAC'07-hard XD），拿個 Turing Award 滿正常的 XD。

--
底層用到 automata theory 喔！