一、基本資訊

標題：SAwUML – UML-based, contractual software architectures and their formal analysis using SPIN
時間：2018
出版源：Computer Languages, Systems & Structures
領域分類：軟體架構；UML；按合同設計；PROMELA;正式驗證

二、研究背景

問題定義：基於UML的合同軟體體系結構及其使用SPIN的形式分析
難點：複雜的設計決策,瞭解SAwUML，
相關工作：SAwUML結構；SAwUML行為；將SAwUML翻譯成ProMeLa；

三、創新方法

1.SAwUML的工具支援
2.

四、實驗

實驗1：案例分析

要探究的問題:SAwUML中的加油站規範；ProMeLa加油站規範的翻譯；
結論：如果結果等於客戶請求的所選金額，則requestMade資料設定為false以發出新的氣體請求。如果結果不等於所選的數量，則元件狀態不會更改。泵方法不會返回任何值以傳送回收銀臺元件。
收銀員元件的客戶提供的埠和releasePump所需的埠各自操作一種方法。雖然收銀員提供的埠被轉換為單個保護動作序列，但所需埠被轉換為兩個保護序列。最後，泵元件的油和來自凱西爾 提供的埠也被轉換為單個保護動作序列

實驗2：工具評估

要探究的問題：死鎖的正式驗證；對不完整性的正式驗證；使用者定義屬性的形式驗證；
結論：因為客戶元件最初將requestMade資料設定為false ，所以永遠不會滿足。因此，這將阻止一系列方法 - 要求加油站系統達到其目標，即客戶付款，收銀員接收付款和釋放氣體，然後泵接收釋放氣體請求並向客戶傳送氣體。直觀地說，死鎖情況發生此因為客戶的將繼續努力進行付款或無限期地泵請求永遠不會發生，而收銀臺付款無限期等待，並釋放氣體要求無限期的等待泵。因此，這些元件都不能達到最終狀態。
如果對於所需的埠方法沒有滿足任何請求前置條件，則不傳送方法請求。如果提供的埠方法請求沒有滿足任何行為規範，則將方法呼叫請求重新寫回通道以便稍後重新評估。不完整性與需要埠的客戶和出納組件有關。
每當客戶支付燃氣費時，出納員最終要求泵釋放燃氣，最終泵將為客戶釋放燃氣。指定了LTL屬性後，我們使用了轉換器並獲得了ProMeLa模型，該模型還包括LTL屬性的轉換，併成功使用SPIN模型檢查器正式驗證了LTL屬性的規範。注意，在驗證不成功的情況下，發生斷言違規錯誤，這可以通過給出的錯誤報告來觀察。

五、結論

作者的總結：在本文中，我們提出了一種名為SAwUML 的新軟體體系結構建模語言。SAwUML基於眾所周知的UML軟體建模語言，使用其元件和序列圖來確定結構和行為設計決策的規範。SAwUML使用“ 按合同設計”擴充套件了序列圖方法並允許元件從彼此請求/提供的方法的合同行為規範。SAwUML由建模編輯器支援，用於以線性時態邏輯（LTL）的形式指定軟體體系結構和任何系統級屬性。建模編輯器還使用正式的ProMeLa語言實現SAwUML的精確翻譯，從而可以使用SPIN模型檢查器對軟體體系結構進行形式驗證。SAwUML目前支援詳盡檢查死鎖和不完整的行為規範。從業者還可以自動檢查LTL屬性規範。
自己的評價：軟體架構一直是軟體設計中最關鍵的部分，它涉及幾個複雜的設計決策，這些決策對於成功構建軟體系統非常重要。一些重要的設計決策是關於從獨立元件組成系統的結構設計決策，行為和互動設計決策，非功能系統屬性的決策以及與併發相關的問題的決策。可以在軟體設計的早期架構階段指定和分析這樣的設計決策，並且可以做出正確和最佳的決策，從而使軟體系統滿足質量要求。

參考文獻：
【1】：R.N. Taylor, N. Medvidovic, E.M. Dashofy Software architecture – Foundations, theory, and practice 978-0-470-16774-8, Wiley (2010)
【2】：M. Ozkaya Do the informal & formal software modeling notations satisfy practitioners for software architecture modeling? Inf Softw Technol, 95 (2017), pp. 15-33, 10.1016/j.infsof.2017.10.008
【3】：Object Management Group. OMG unified modeling language secification – version 2.5. http://www.omg.org/spec/UML/2.5/; 2015. URL http://www.omg.org/spec/UML/2.5/.
【4】：A. Pataricza, I. Majzik, G. Huszerl, G. Várnai UML-based design and formal analysis of a safety-critical railway control software module Tarnai G., Schnieder E. (Eds.), [Formal methods for railway operation and control systems], L’Harmattan Kiadó, Budapest (2003), pp. 125-132
【5】：J. Cabot, R. Claris, D. Riera On the verification of UML/OCL class diagrams using constraint programming J Syst Softw, 93 (2014), pp. 1-23, 10.1016/j.jss.2014.03.023