基本介紹
- 中文名：抽象機符號
- 外文名：Abstract machine symbol
- 類別：計算機套用
UML建模的形式化方法研究和套用,B方法簡介,抽象機,UML用例模型的B形式化描述方法,B方法概述,抽象機的精化,
UML建模的形式化方法研究和套用
形式化方法是建立在嚴格數學基礎上的軟體開發方法，能夠精確地、無二義地描述系統，並且有嚴格的證明。B方法是一種較為實用的形式化軟體開發方法，覆蓋了從抽象規約到可執行代碼生成的過程，擁有強有力的支持工具。B方法使用抽象機符號（A\1N）來構造模型，並支持規範說明的類型檢測和動態驗證。B方法的支持工具可用動畫等方式模擬運行規範說明，根據需求和測試場景檢查獲得的規範說明是否符合需求，對提高軟體的可靠性有著非常顯著的作用。
B方法簡介
B方法屬於基於模型的規格說明符號語言範疇，是一種基於對象的形式化語言。J一RAbrial是對軟體形式化方法及其套用做出了最重要貢獻的人物之一。從20世紀70年代開始研究數據結構的程式的形式化規範問題，20世紀70年代後期在牛津大學程式設計研究組（PRG）訪問期間完成了有關形式化規範語言z的開創性工作。為了將形式化方法與軟體更好地平滑銜接，J一RAbrial從20世紀80年代前期開始了B語言和B方法的研究和開發。1985年至1988年，PRG在一項為期三年的R&D項目中研製開發了B語台‘方法和抽象機符號表示法。
B方法的口的是希望為整個軟體開發過程提供堅實的數學基礎。隨著B方法的發展和成熟，B方法是國際上最受重視的實用性軟體形式化方法之一，用它編寫軟體系統規範，進行系統設計和編程。它已經被成功地套用到許多關鍵性的工業開發項目中。一個早期的重要實例是巴黎捷運列車的信號系統，這一系統為減少列車的陽J距、提高整個捷運系統的安全性做出了顯著貢獻。
B方法是一種用於描述、設計計一算機軟體的嚴格方法，其作用一直延伸到代碼生成。B方法的中心思想是C.A.R.Hoare和E.W.Dijkstra的程式作為一個數學對象、前一後謂詞、不確定性最弱前置謂詞的概念。B方法使得軟體系統的需求定義、規格說明、可執行軟體組件實現處於一個統一的數學框架之下，以基於集合理論和符號表示法來書寫。
通常最初的需求是以自然語言表示，或者使用圖表，邏輯表格，B方法是藉助數學的符號表示方法和謂詞邏輯、集合、序列、函式及其他的抽象數據類型，以一種精確的方法來描述軟體需求與設計。抽象機符號表示法（AbstractMaChineNotation:AMN）是B方法的規格說明與設計語言。廣義代換語言（GeneraliZedSubstitUtionLanguage）提供了A訓的形式語義，標識抽象機的操作。使用B方法開發時，首先要在用自然語言描述系統需求的基礎上，描述系統的主要狀態，構造反映需求的B方法形式規約，不變式給出這些狀態需要滿足的屬性，操作給出這些狀態的變化。由此得到的模型反映了軟體系統實現的功能。然後對所得到的形式規約進行驗證和產生證明義務（由B方法上具完成），確認該規約實現了系統的功能。
抽象機
在接受了形式化地描述一個軟體系統的任務之後，需要一種能用於說明軟體系統是什麼、處理起來比較簡單的通用模型，這一模型能更容易地閱讀一個給定系統的描述，抽象機就是這樣的一個模型。抽象機 （AbstractMachine:AM）是B方法的一個基本機制，其概念非常接近模組、類或抽象類型。
按照抽象機模型的方式去理解軟體系統，就是說，總用一個狀態以及各種各樣能夠改變這一狀態的操作方式去理解它們。對這些系統的分析就構成了抽象機對應於狀態定義的靜態行為和對應於有關操作的動態行為。
靜態行為即狀態的描述:首先是構成了狀態的組成成分所需要的變數;其次是描述了系統的靜態規則有關的不變式。不變式是一個邏輯語句，基於有關變數並利用謂詞演算和集合論的形式語言進行描述。
動態行為即操作的描述:操作就是在不變式的限制範圍之內修改抽象機器中的狀態。
抽象機的各個子句如下：
MACHINE子句；CONSTRAINTS子句；SET子句；CONSTANTS子句；PROPERITIES子句；VARIABLES子句；DEFINITIONS子句；INVARIANTS子句；INITIALISATION子句；ASSERTION子句；OPERATI0N子句。
UML用例模型的B形式化描述方法
以UML用例模型為主要研究對象，在分析UML用例模型概念和B抽象機符號的基礎上，對用例模型建模元素的抽象語法進行描述，建立兩者之間的映射，實現UML用例模型圖到B形式規約的轉換。首先用半形式化的UML用例模型為目標系統建立需求模型，然後根據給出方法構建目標系統的B形式化規約，再利用B方法支持工具對規約進行動態分析和模型驗證，得出可靠的形式規約，為在此基礎上進行的形式推導和精化提供了正確的起點。最後，通過對電梯控制系統的實例分析，進一步詳述了UML用例模型到B方法形式規約的轉換方法及過程，並利用B方法的支持工具ProB對所得到的形式化模型進行了動態分析和模型檢測。
B方法概述
B方法當前正為產業界和學術界越來越多的人們所關注，研究工作是在20世紀80年代的初期和中期由J.R Abrial以及BP研究中心的MATRA和GEC Alsthom研究小組進行的，目的是希望為實際軟體開發過程提供一個堅實的數學基礎。B方法以Z語言的研究為背景，在引入一些面向對象機制等特點的同時，保留了Z語言的優點，即基於所熟悉且便於理解的數學基礎。在B方法的形成過程中，吸收了將程式作為一個數學對象、前-後謂詞、不確定性最弱前置謂詞的概念以及‘’Programming fromSpecification‘’的重要思想。
B方法是一廣譜方法，包含了高度抽象的數學描述和可執行的描述。它藉助數學符號表示方法，如謂詞邏輯、集合、序列、函式及其他的抽象數據類型，在軟體開發的各個階段採用統一的AMN（Abstract Machine Notation），以一種精確的方法描述系統規約和系統設計，使程式和程式的規約說明處於統一的數學框架下，支持規約說明特性推理（包括內部一致性驗證和精化驗證），減少出現語義錯誤的可能性。
在B方法中，軟體系統模型由一個或多個相互依存地抽象機構成，稱為B模型。B模型由三種類型的B組件共同表達：機器（MACHINE）、精化（REFINEMENT）、實現（IMPLEMENTATION）。通常，B模型有一個MACHINE 組件來描述目標系統的規約，有多個精化來描述系統的開發過程，有一個實現表達系統的最終實現細節，其中實現是一種特殊的精化，是系統精化的最後階段，可藉助工具直接轉化為可執行代碼（如C語言代碼）。為了確保規約本身及精化過程的一致性，B方法提供了正確性驗證機制，自動產生證明義務，並且兩個商業支持工具（B-Toolkit和Atelier-B）都能自動證明大部分的證明義務。從本質上看，B方法處理的是軟體生存周期的核心方面，即技術性的規範，通過一系列精化步驟進行設計，產生層次性體系結構，以及可執行代碼的生成。
抽象機的精化
精化是一種技術，用於將軟體系統的‘’抽象模型‘’（其規範）變換為另一種更加具體的模型表示（即精化結果）。後一種模型可能在兩個方面更具體：首先，它可能包含了與原來非形式規範有關的更多細節；其次，它可能更接近於實現。
B方法通過分層模組方式構造大型的軟體系統的基本思想是：抽象機的數學模型要經過多次精化，直到最後的精化結果能夠直接在計算機上執行。這樣的一個精化結果可能引入另外一些抽象機（其他模組）作為最終實現的基礎。由於這種原因，最終精化的結果被稱為實現。
一次精化可以從MACHINE到一個REFINEMENT組件，或從一個REFINEMENT組件到另一個REFINEMENT組件，或者從REFINEMENT組件到IMPLEMENTATION組件。精化過程向規約中引入了所有非形式規約中表達的性質，在每一步精化過程中都必須證明精化關於其抽象的正確性，且都需要通過廣義代換整體性地重新構造初始的抽象機。在B方法中，軟體開發過程就是一個對規約（抽象機集合）逐步精化直至實現的過程。
