一種基于B方法的需求描述轉(zhuǎn)化為AADL模型的研究

王日磊 陳奎 史巖

摘要：目前，航空、航天等領(lǐng)域?qū)ο到y(tǒng)的可靠性有著極高的要求，業(yè)界也在研究和探討通過構(gòu)建系統(tǒng)的體系結(jié)構(gòu)模型保證后續(xù)驗(yàn)證、開發(fā)等階段的一致性，從而提升系統(tǒng)的可靠性。首先需要確保構(gòu)建的系統(tǒng)模型滿足系統(tǒng)的原始需求，只有這樣，才能保證后續(xù)基于模型的開發(fā)、驗(yàn)證等輸出的系統(tǒng)產(chǎn)品與原始需求保持一致性。文章提出了一種以形式化B方法對(duì)系統(tǒng)需求進(jìn)行形式化描述，通過構(gòu)建B方法與AADL模型的轉(zhuǎn)換規(guī)則，從而輸出系統(tǒng)的AADL模型，從而支持基于AADL模型直接生成對(duì)應(yīng)測(cè)試用例對(duì)系統(tǒng)開展驗(yàn)證、開發(fā)等工作。

關(guān)鍵詞：B方法；AADL；模型驅(qū)動(dòng)

中圖分類號(hào)：TP311.5? ? 文獻(xiàn)標(biāo)識(shí)碼：A? ?文章編號(hào)：1674-0688（2023）01-0058-04

0 引言

任務(wù)關(guān)鍵型系統(tǒng)是一種對(duì)實(shí)時(shí)性、可靠性和安全性等都有嚴(yán)格要求的系統(tǒng)，如應(yīng)用在航空航天發(fā)動(dòng)機(jī)管理系統(tǒng)、交通運(yùn)輸信號(hào)管理系統(tǒng)等。所以，任務(wù)關(guān)鍵型系統(tǒng)的研發(fā)過程中應(yīng)該采取何種技術(shù)或流程開發(fā)出高可靠性的系統(tǒng)產(chǎn)品也是業(yè)界研究和探討的熱點(diǎn)。目前，基于模型驅(qū)動(dòng)的軟件開發(fā)方法因?yàn)榭梢蕴嵘痛_保軟件系統(tǒng)最終的質(zhì)量，所以在業(yè)界得到了廣泛的應(yīng)用，同時(shí)業(yè)界也在探尋其他數(shù)學(xué)方式如形式化方法等來持續(xù)提升系統(tǒng)的可靠性、安全性等非功能屬性。B方法是一種面向模型的形式化需求方法，用偽代碼描述系統(tǒng)需求模型，對(duì)系統(tǒng)原始需進(jìn)行形式化描述。結(jié)構(gòu)分析與設(shè)計(jì)語言（Architecture Analysis & Desing Language，AADL）被認(rèn)為是基于模型驅(qū)動(dòng)的嵌入式實(shí)時(shí)系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn)的基礎(chǔ)，可以對(duì)任務(wù)關(guān)鍵系統(tǒng)進(jìn)行設(shè)計(jì)建模。為了確保任務(wù)關(guān)鍵系統(tǒng)的模型滿足系統(tǒng)的原始需求， 本文提出了一種基于形式化B方法生成AADL模型的方法，在需求階段采用形式化的B方法描述系統(tǒng)的需求，通過構(gòu)建B方法與AADL的語法映射規(guī)則，由B方法形式化需求描述生成相應(yīng)的AADL模型，從而確保AADL設(shè)計(jì)模型的正確性。后續(xù)可以使用模型驅(qū)動(dòng)的測(cè)試方法，基于AADL模型生成測(cè)試用例對(duì)系統(tǒng)直接開展驗(yàn)證，從而基于模型保證需求描述到測(cè)試用例的自動(dòng)轉(zhuǎn)換，減小對(duì)需求理解的偏差，提升和保證測(cè)試用例對(duì)需求覆蓋的精確性、全面性。

1 相關(guān)技術(shù)

1.1 B方法

形式化方法是指建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上的軟件開發(fā)方法。在軟件開發(fā)過程中，從需求分析、規(guī)格說明、設(shè)計(jì)、編程、系統(tǒng)集成、測(cè)試、文檔生成直至維護(hù)的各階段，凡是采用嚴(yán)格的數(shù)學(xué)語言、具有精確的數(shù)學(xué)語義的方法都稱為形式化方法［1］ 。

B方法是一種基于模型的軟件構(gòu)造方法，類似于VDM（Vienna Development Method）和Z（一種基于一階謂詞邏輯和集合論的形式規(guī)格說明語言）［2］。B 語言支持規(guī)格說明，并且支持繼規(guī)格說明之后所有的精化和設(shè)計(jì)步驟［3］。

抽象機(jī)（Abstract Machine AM）是B方法的一個(gè)基本機(jī)制，其概念非常接近模塊、類或抽象類型 ［3-5］，其封裝了系統(tǒng)的靜態(tài)行為和動(dòng)態(tài)行為2個(gè)部分的內(nèi)容，即狀態(tài)和操作。其中，變量和集合及數(shù)學(xué)項(xiàng)等構(gòu)成狀態(tài)，這些狀態(tài)要符合一定的規(guī)則（即不變式），它是一個(gè)邏輯語句，利用集合論及謂詞演算進(jìn)行描述。操作關(guān)鍵字描述系統(tǒng)的動(dòng)態(tài)行為，每一個(gè)操作可以改變抽象機(jī)的當(dāng)前狀態(tài)，但這些狀態(tài)的改變不能超過不變式的范圍。

一個(gè)簡(jiǎn)單的B方法抽象機(jī)包含幾個(gè)子句，MACHINE子句表示抽象機(jī)的名稱為 M。SETS子句主要用來描述抽象機(jī)中的數(shù)據(jù)類型，列出抽象機(jī)中需要使用的數(shù)據(jù)集合，表達(dá)形式為S1，S2，…，Sn。集合通常分為2種形式，一種是延期集合，另一種是枚舉集合，它們可以表示獨(dú)立的數(shù)據(jù)類型。CONSTANTS主要表示抽象機(jī)中所有的常量，形式為C1，C2，…，Cn。PROPERTIES子句描述了涉及常量和給定集合的謂詞，主要用來描述它們的邏輯特征，通常表示為一個(gè)合取公式。變量子句 VARIABLES定義了該抽象機(jī)所使用的狀態(tài)變量，其形式為v1，v2，…，vn。這些變量的值的改變，只能由抽象機(jī)中的操作關(guān)鍵字實(shí)現(xiàn)。不變式 INVARIANT子句描述了抽象機(jī)的靜態(tài)規(guī)則，即抽象機(jī)狀態(tài)的不變式性質(zhì)，通常是由若干個(gè)謂詞組成的邏輯語句，語句中包括變量、常量和機(jī)器參數(shù)。抽象機(jī)的所有操作均要嚴(yán)格遵守定義的不變式。INITIALIZATION子句是對(duì)抽象機(jī)的初始狀態(tài)進(jìn)行描述，即對(duì)機(jī)器的變量賦初始值。通常采用代換的形式進(jìn)行初始化操作。初始化操作同樣不能違反不變式的規(guī)定。系統(tǒng)的操作OPERATIONS子句用來描述系統(tǒng)的動(dòng)態(tài)行為，通常用由不包括順序或循環(huán)的偽代碼表示，而這段偽代碼是不能被執(zhí)行的。每條操作由2個(gè)元素組成，包括1個(gè)前置條件、1個(gè)原子動(dòng)作，前置條件指出在什么條件下激活操作，原子操作通過形式化的廣義代換表示。

1.2 AADL

體系結(jié)構(gòu)分析與設(shè)計(jì)語言AADL（Architecture Analysis & Desing Language）是一種字符化和圖形化的語言，是由SAE（Society for Automotive Engineers）提出，主要用于設(shè)計(jì)和分析對(duì)性能有極高要求的實(shí)時(shí)系統(tǒng)的軟、硬件體系結(jié)構(gòu)。AADL模型主要由各種類型的組件構(gòu)成，可以表示AADL模型的硬件、軟件等各類型的實(shí)體。AADL中的組件可以劃分為軟件組件、執(zhí)行平臺(tái)組件和系統(tǒng)組件3種類型。軟件組件主要包含數(shù)據(jù)、進(jìn)程、線程、子程序等；執(zhí)行平臺(tái)組件由存儲(chǔ)器、總線、外設(shè)、處理器等組件組成；系統(tǒng)組件主要表示系統(tǒng)。Object-Oriented Language中的類、對(duì)象的定義與AADL中的組件類型（Component Type）和組件實(shí)現(xiàn)（Component Implementation）的概念有相似之處。組件類型是指組件的作用分類，用來描述組件的用途如對(duì)外接口（網(wǎng)口、端口等）。組件類型可以通過標(biāo)識(shí)符、特征、流和屬性進(jìn)行描述，這與Object-Oriented Language中類的標(biāo)識(shí)符、屬性、方法等概念類似。組件用來描述和細(xì)化組件的內(nèi)部結(jié)構(gòu)，包括子組件、組件之間的關(guān)系等。

AADL模型主要應(yīng)用于高可靠性的關(guān)鍵系統(tǒng)進(jìn)行建模，可以直接定義軟件和硬件間的對(duì)應(yīng)關(guān)系，描述系統(tǒng)的功能屬性和非功能屬性。

2 B方法到AADL模型的轉(zhuǎn)換

本節(jié)在總結(jié)和分析形式化B方法語法、AADL模型語言語法的基礎(chǔ)上，提出了一種基于B方法的需求描述，最終用于生成AADL設(shè)計(jì)模型的方法，該方法的主題思想如下：首先，對(duì)系統(tǒng)需求進(jìn)行自然語言描述，然后依據(jù)B方法的語法規(guī)則，通過構(gòu)造抽象機(jī)及抽象機(jī)之間的關(guān)系，使用B方法將非形式化的需求描述進(jìn)行形式化描述，再通過建立B語言和AADL之間的映射規(guī)則，由形式化的B方法需求描述直接生成AADL設(shè)計(jì)模型。該方法的開發(fā)流程圖如圖1所示。

2.1 B方法描述系統(tǒng)需求

B方法的語法基礎(chǔ)是各種各樣的抽象機(jī)。任務(wù)關(guān)鍵系統(tǒng)包含一些軟件系統(tǒng)和若干硬件設(shè)備，為了使用B方法的抽象機(jī)描述整個(gè)系統(tǒng)需求，研究人員需要定義若干不同的抽象機(jī)。每一個(gè)抽象機(jī)代表一個(gè)實(shí)際存在的系統(tǒng)、軟件或硬件，也稱為實(shí)體抽象機(jī)，對(duì)應(yīng)的抽象機(jī)名稱即實(shí)體的名稱。此外，可以定義一個(gè)延期集合（Defer Set）ENTIY，用于表示系統(tǒng)、軟件和硬件等實(shí)體所有可能的（現(xiàn)在和未來）實(shí)例。同時(shí)，定義一個(gè)變量entiy，表示該實(shí)體現(xiàn)有的實(shí)例。兩者的關(guān)系在抽象機(jī)的不變式子句INVARIANT中約束為entiy∈ENTIY。

為了區(qū)分各抽象機(jī)所描述的實(shí)體對(duì)象，研究人員將實(shí)體抽象機(jī)按照邏輯分為以下3種類型：系統(tǒng)類抽象機(jī)（System Machine）、軟件類抽象機(jī)（Software Machine）、硬件類抽象機(jī) （Hardware Mchine）。在需求階段，對(duì)系統(tǒng)中包含的軟件系統(tǒng)，研究人員只關(guān)注這個(gè)軟件系統(tǒng)所提供的功能和非功能需求，不需要描述需求的設(shè)計(jì)和實(shí)現(xiàn)過程，將這個(gè)軟件具體設(shè)計(jì)為一個(gè)子系統(tǒng)或進(jìn)程等，所以將需求中的所有軟件系統(tǒng)全都抽象為軟件類抽象機(jī)。對(duì)于硬件設(shè)備，抽象機(jī)直接描述某一種特定的硬件設(shè)備，同時(shí)可以在數(shù)據(jù)類型抽象機(jī)中定義一些常用的硬件設(shè)備類型。對(duì)于需求描述中所需的數(shù)據(jù)類型，除了B方法提供的簡(jiǎn)單數(shù)據(jù)類型（包括INT、CHAR、BOOL），其他復(fù)雜數(shù)據(jù)類型或者其他自定義數(shù)據(jù)類型可定義在一個(gè)特殊的抽象機(jī)，即數(shù)據(jù)類型抽象機(jī)（DateType Machine）。實(shí)體抽象機(jī)通過“USES”關(guān)鍵字引用數(shù)據(jù)類型抽象機(jī)，可以使用數(shù)據(jù)類型抽象機(jī)定義數(shù)據(jù)類型。

Includs關(guān)鍵字用來表示系統(tǒng)實(shí)體、軟件實(shí)體、硬件實(shí)體之間的包含關(guān)系。同時(shí)，對(duì)于需求中的系統(tǒng)、軟件和硬件非功能屬性需求，在實(shí)體抽象機(jī)定義相關(guān)的變量，并使用需求中所要求的值對(duì)這個(gè)變量進(jìn)行初始化。對(duì)于原始需求中每個(gè)實(shí)體各種狀態(tài)之間的轉(zhuǎn)換，使用抽象機(jī)中的操作表示，操作的前提條件為引起狀態(tài)發(fā)生變化的事件或動(dòng)作。

一個(gè)B方法描述的系統(tǒng)需求由系統(tǒng)類抽象機(jī)（System Machine）、軟件類抽象機(jī)（Software Machine）、硬件類抽象機(jī) （Hardware Mchine）、數(shù)據(jù)類型抽象機(jī)4類抽象機(jī)組成，數(shù)據(jù)類型抽象機(jī)主要定義數(shù)據(jù)類型的集合及函數(shù)之間的映射關(guān)系。數(shù)據(jù)類型抽象機(jī)會(huì)被其他實(shí)體抽象機(jī)調(diào)用，然后一起對(duì)系統(tǒng)的原始需求進(jìn)行描述。

2.2 B方法到AADL的映射規(guī)則

為了使B方法需求描述映射生成基本的AADL設(shè)計(jì)模型，研究人員定義了B方法語法和AADL模型語法之間的4條映射規(guī)則。

規(guī)則1：一個(gè)B方法中的實(shí)體抽象機(jī)可以對(duì)應(yīng)AADL模型中的一個(gè)組件。使用B方法描述系統(tǒng)需求，每個(gè)實(shí)體抽象機(jī)即對(duì)應(yīng)現(xiàn)實(shí)場(chǎng)景中的一個(gè)系統(tǒng)、軟件或硬件。AADL中的組件類型分為系統(tǒng)、軟件和硬件3種組件。可以規(guī)定每一個(gè)實(shí)體抽象機(jī)即對(duì)應(yīng)一個(gè)AADL組件，而且要求組件名稱與抽象機(jī)名稱相同，組件類型與抽象機(jī)名的同名變量的類型相同。

規(guī)則2：B方法中的實(shí)體抽象機(jī)之間的Includes關(guān)系可以映射到AADL模型中的Subcomponent。B方法中的抽象機(jī)之間的Includes關(guān)系用來表示在特定的抽象機(jī)中包含其他抽象機(jī)，而AADL模型中的Subcomponent也表示當(dāng)前組件包含了其他組件。所以，抽象機(jī)包含的子抽象機(jī)可以映射到AADL的Subcomponent。

規(guī)則3：B方法中實(shí)體抽象機(jī)中定義的變量可以映射到AADL組件類型中的Properties。 AADL中的組件類型用來描述一個(gè)組件的整體屬性，而B方法中每個(gè)實(shí)體抽象機(jī)中所定義的變量也用來描述相關(guān)實(shí)體的屬性要求。所以，可以將抽象機(jī)中用于描述實(shí)體屬性的變量映射到AADL的properties。

規(guī)則4：B方法中實(shí)體抽象機(jī)中的操作可以映射到AADL組件的特征、流和模式等。具體的映射方法是B抽象機(jī)的帶輸出和輸入?yún)?shù)的操作映射到AADL組件中向外和向內(nèi)的接口。這里的操作可以只有操作名而沒有操作細(xì)節(jié)，因?yàn)樵谛枨竺枋鲭A段只關(guān)注需求描述這個(gè)實(shí)體所提供的接口，只有接口定義，不需要真正關(guān)注接口如何實(shí)現(xiàn)，但映射到AADL模型時(shí)，就需要人工進(jìn)行決策，確定這個(gè)接口具體的類型。B方法中的while代換和順序代換分別映射到AADL組件中的模式變換和流。

3 應(yīng)用舉例

首先使用B方法進(jìn)行需求描述，然后應(yīng)用本文中定義的B方法到AADL的模型轉(zhuǎn)換規(guī)則進(jìn)行需求描述的轉(zhuǎn)換。以一個(gè)簡(jiǎn)單的速度控制器系統(tǒng)需求為例，速度控制器由速度傳感器、油門執(zhí)行器及速度控制軟件系統(tǒng)組成。在實(shí)際應(yīng)用場(chǎng)景中，首先速度控制器處于初始（initial）狀態(tài)，速度控制器啟動(dòng)之后，切換為運(yùn)行狀態(tài)，然后通過速度傳感器采集當(dāng)前的速度數(shù)據(jù)，將數(shù)據(jù)傳給速度控制系統(tǒng)進(jìn)行分析，同時(shí)速度控制系統(tǒng)可以向油門控制器發(fā)出控制指命。整個(gè)系統(tǒng)的命令的最大執(zhí)行時(shí)間為10 ms。

針對(duì)上述對(duì)速度控制器的需求，可以使用B方法對(duì)其進(jìn)行描述。其中，整個(gè)抽象機(jī)名可以定為sSpeedControlSystem，然后通過INCLUDE關(guān)鍵字包含Sensor、Controller、Throttle表示系統(tǒng)包括2個(gè)硬件設(shè)備和1個(gè)軟件系統(tǒng)。同時(shí)，速度控制器系統(tǒng)中用到的變量包含系統(tǒng)狀態(tài)、命令執(zhí)行最大時(shí)間等，可以使用VARIABLES關(guān)鍵字定義pP、dDeadline表示，并可以通過INITIALIZATION關(guān)鍵字對(duì)這2個(gè)變量進(jìn)行初始化，因?yàn)橄到y(tǒng)最初是關(guān)閉的狀態(tài)，而且整個(gè)系統(tǒng)命令的最大執(zhí)行時(shí)間為10 ms，根據(jù)上述需求可以描述為pP：=sShut，dDeadline：=10。針對(duì)系統(tǒng)的狀態(tài)變化，可以通過OPERTIONS關(guān)鍵字描述IF pP=oOpen，THEN? mMode（sSpeedControlSystem）：=eExecute表示當(dāng)速度控制器啟動(dòng)之后，切換為運(yùn)行狀態(tài)。

通過第2.2章節(jié)中定義的B方法到AADL的轉(zhuǎn)換規(guī)則，可以將上述使用B方法定義的速度控制器系統(tǒng)需求轉(zhuǎn)換為AADL模型。其中，AADL中的systemSystem關(guān)鍵字直接繼承MACHINE的名稱值，然后系統(tǒng)的組成關(guān)系在AADL模型中可以通過sSubcomponent關(guān)鍵字繼承B方法中的INCLOUD關(guān)系，則3個(gè)subcomponentSubcomponent分別為 sensorSensor：device Device Sensor.imp、throttleThrottle：device Shrottle.imp、controllerController：system System Sontroller.imp。針對(duì)系統(tǒng)中涉及的變量即系統(tǒng)狀態(tài)、命令執(zhí)行最大時(shí)間，直接使用propertiesProperties關(guān)鍵字進(jìn)行描述，同時(shí)參考B方法的INITIALIZATION獲取這些變量的初始值，即可以直接描述為spdeadlineSpdeadline=>10 ms。針對(duì)系統(tǒng)狀態(tài)的變化，可以通過AADL中的modesModes關(guān)鍵字進(jìn)行描述，因?yàn)锽方法中描述的狀態(tài)包括初始化狀態(tài)和執(zhí)行狀態(tài)，那么在AADL中也可定義2個(gè)狀態(tài)（initInit：init Init modeMode; executeExecute：modeMode），同時(shí)直接使用initInit-->executeExecute表示狀態(tài)之間的轉(zhuǎn)換。

4 結(jié)論

本文通過對(duì)形式化B方法及AADL模型探索和研究，分析二者的語法規(guī)則，提出了B方法與AADL模型之間的轉(zhuǎn)化規(guī)則，實(shí)現(xiàn)將B方法描述的系統(tǒng)需求轉(zhuǎn)化為對(duì)應(yīng)的AADL模型，從而可以支持后續(xù)基于AADL模型的自動(dòng)化驗(yàn)證以及開發(fā)等工作，從而實(shí)現(xiàn)高質(zhì)量、高可靠性的系統(tǒng)。但是，本文的轉(zhuǎn)換規(guī)則只有4條，目前還無法支撐一個(gè)完整系統(tǒng)的需求描述轉(zhuǎn)為AADL模型，所以需要對(duì)B方法和AADL模型進(jìn)行持續(xù)的研究和學(xué)習(xí)，從而建立更多的轉(zhuǎn)換規(guī)則，更好地滿足二者之間的轉(zhuǎn)換需求，而且因?yàn)锽語言是形式化語言，需要一定的形式化數(shù)據(jù)知識(shí)基礎(chǔ)，學(xué)習(xí)難度較高，所以如何確保設(shè)計(jì)人員能更好、更方便地使用形式化B語言對(duì)系統(tǒng)需求進(jìn)行全面、準(zhǔn)確的描述，也是后續(xù)工作的重點(diǎn)。

5 參考文獻(xiàn)

［1］塔維娜， 何積豐. 基于形式化方法的需求分析［J］.計(jì)算機(jī)工程，2003，29（18）：107-108.

［2］Brookes S D，Hoare C A R，Roscoe A W. A theory of communicating processes［J］.Journal of the ACM，2009，31（3）：560-599.

［3］J-RAbrial.B方法［M］.裘宗燕，譯.北京：電子工業(yè)出版社，2004：15-16.