一、基本信息

標題：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屬性規范。
自己的評價：軟件架構一直是軟件設計中最關鍵的部分，它涉及幾個復雜的設計決策，這些決策對于成功構建軟件系統非常重要。一些重要的設計決策是關于從獨立組件組成系統的結構設計決策，行為和交互設計決策，非功能系統屬性的決策以及與并發相關的問題的決策?？梢栽谲浖O計的早期架構階段指定和分析這樣的設計決策，并且可以做出正確和最佳的決策，從而使軟件系統滿足質量要求。

參考文獻：
【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

轉載于:https://www.cnblogs.com/-Wwl/p/10095803.html

總結

以上是生活随笔為你收集整理的SAwUML – UML-based, contractual software architectures and their formal analysis using SPIN的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。