之前談到UML and Model Checking，卻沒談到如何實際應用及檢查方式，這篇Model Checking and Code Generation for UML State Machines and Collaborations是之前說到的Hugo/RT轉換工具的Paper，首先下載ArgoUML一套open source的UML工具；再下載Hugo/RT 0.42，個人是選UPPAAL的Model Checking tool。
1.先用ArgoUML將系統畫出，主要是class diagram跟state diagram。
如下圖：
2.透過Hugo/RT轉換成中間碼，Hugo/RT也提供直接轉換成Model Checking的語言，但因有些功能無法轉換，必須自行輸入，所以建議轉成中間碼UTE格式。
3.編輯UTE檔案，加入collaboration、interaction及assertion，其中assertion可以利用CTL(Computation tree logic)來檢查deadlock和是否會發生某些條件。例如此例就是ATM是否會有兩次密碼錯誤卻還能進入VerifyingCard的狀態。
EF的keyword如下圖所示。代表是否存在這個狀況。
4.編輯好存檔，再利用Hugo/RT轉成UPPAAL的檔案，且下所需要檢查的interaction和assertion，便會產生ta及q副檔名的兩個檔案。
5.再來就利用UPPAAL來驗證，開始剛產生的ta檔案，選verifier的tag就可以驗證是否會有不想要的情況。從結果可看出，並沒有輸入錯誤兩次還能在VerifyingCard狀態(紅燈)，但卻可以輸入錯誤零次還能在VerifyingCard狀態(綠燈)。
本文只是介紹使用方法，詳細內容可以看Model Checking and Code Generation for UML State Machines and Collaborations及Hugo/RT網站。
雖然測試也可能找到相同的錯誤或不一致情況，但是Model Checking在OOA時就可以去驗證檢查，Testing則必須要到OOP之後有程式碼才能檢查，所以成本會比Model Checking還要高(越晚修改，cost越高)，且Model Checking主要是檢查規格上的錯誤，無法去驗證效能和壓力，而這些主要是測試所要確認的。
2006-07-24 補充：本文的範例，蒸氣鍋爐，已刊登在IEICE TRANSACTIONS on Information and Systems，Constraint-Based Software Specifications and Verification Using UML。
Embedded.com - An introduction to model checking有詳細介紹Model Checking。
