UML and Model Checking

之前談到Executable UML，但是那只能做模擬，卻不能給予一些錯誤的反例，來去驗證是否會發生，所以就必須透過正規方法(Formal Methods)來驗證UML設計是否正確，比較方便是利用Model Checking(算是正規方法的一種)來檢查。
目前Model Checking的工具包括SPIN、AsmL、SMV等等，理論主要是利用時序邏輯(Temporal Logic)和有限狀態機(Finite State Machine)，且不只用在軟體設計，硬體設計、安全分析、自動控制都有透過Model Checking來分析是否安全。
可是像SPIN就必需學Promela語言，AsmL要學C#，所以不知道有沒有工具能夠轉譯UML的狀態圖(State Diagram)，這樣就不需要再學其他語言，直接轉換就可以去驗證，幸運地，找到Hugo/RT這套直接透過ArgoUML就可以轉譯成SPIN、UPPAAL、KIV的格式，且SPIN跟UPPAAL還能做Assertion檢查，Assertion在這是一個假設的情境或劇情(正常或反例)，Model Checking工具如果出現Assertion的錯誤，就代表設計有錯誤，並且可以Report出這異常的路徑來修正設計，只可惜目前只支援XMI1.0很多UML工具都已經不支援1.0，所以只好使用很難用的ArguUML(0.16不能畫Sequence Diagram *_*，開發人員沒包裝好)，或是自行撰寫UTE(Hugo/RT的格式)的檔案，希望Hugo/RT趕快支援UML2.0跟XMI2.0，我看畢業前應該是不會出現。天啊!怎麼這麼冷(這有兩種涵義，天氣真的很冷，內容太冷沒人想看^_^)!!
補充(2005-03-07)
寫信去Hugo/RT的作者之一，詢問如何retranslation，意外幫忙找到一個bug，Hugo/RT網站上還將提供bug的人列出，^_^，我也在上面。
補充(2005-03-07)
詳細的Model Checking介紹。
補充(2005-06-14)，另一個介紹Model Checking的網頁，有相關的工具。