使用Alloy Models

Question

我正在開發一個關於SA 論壇中間件中HA應用程序實時升級的項目。 在我的部分研究中，我需要爲我的輸入升級活動文件 製作一個UML配置文件，並驗證該文件是否存在某些依賴性約束。現在我想在我的工作中使用ALLOY 而不是UML，因爲它比UML更抽象和形式化。 （ 當然UML + OCL將是正式的。）。現在我的問題是，如果UML + OCL是正式的，那麼 使用ALLOY有什麼好處？ 一般來說，使用Alloy對抗UML有什麼好處？

Answer 1

據我所知，沒有工具可以讓你檢查你的OCL約束與UML 模型，並生成和可視化有效實例，所以如果你打算對模型+規範進行形式分析，合金可能是更好的選擇。即使你不打算做大量的分析，Alloy也能夠生成和可視化有效的實例，這對確保你的模型和規格正確無疑很有幫助。