面向限定自然語言需求的AADL自動(dòng)生成工具

劉承威,楊志斌,2,周 勇,袁勝浩,許金淼,薛 壘

1(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,南京 211106)2(軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心,南京 210093)3(上海航天電子技術(shù)研究所,上海 201109)

1 引 言

安全關(guān)鍵軟件(Safety-Critical Software)[1]是指應(yīng)用于航空、航天、交通、能源等領(lǐng)域的安全關(guān)鍵系統(tǒng)中的一類軟件,其運(yùn)行情況可能引起系統(tǒng)處于危險(xiǎn)狀態(tài),從而導(dǎo)致財(cái)產(chǎn)損失、環(huán)境破壞或者人員傷害.如2016年,日本宇航局JAXA宣布耗資310億日元的X射線天文探測(cè)衛(wèi)星Hitomi由于姿控軟件故障,導(dǎo)致異常翻滾,最終徹底失控.安全關(guān)鍵軟件一般為安全關(guān)鍵系統(tǒng)的一部分,它可能引起或者助長不安全的條件,這樣的軟件被認(rèn)為是安全關(guān)鍵的[2].如何保障這類軟件的可靠性和安全性一直是學(xué)術(shù)界和工業(yè)界共同面臨的難題.

近年來,模型驅(qū)動(dòng)(Model-Driven)尤其是采用形式化模型驅(qū)動(dòng)的安全關(guān)鍵軟件設(shè)計(jì)與開發(fā)方法逐漸受到重視,并被工業(yè)界認(rèn)為是保障軟件安全性與可靠性切實(shí)可行的重要手段.例如,國際民航領(lǐng)域使用的機(jī)載系統(tǒng)適航審定中的軟件開發(fā)標(biāo)準(zhǔn)DO-178C[3]就將模型驅(qū)動(dòng)和形式化方法(即DO-331[4]和DO-333[5])作為其核心標(biāo)準(zhǔn)的重要技術(shù)補(bǔ)充.模型驅(qū)動(dòng)開發(fā)方法以模型為整個(gè)軟件開發(fā)過程的核心,通過在設(shè)計(jì)階段建立軟件的體系結(jié)構(gòu)模型,實(shí)現(xiàn)模型的盡早驗(yàn)證和分析.同時(shí),模型的重用以及基于模型轉(zhuǎn)換的求精過程,都有助于降低軟件開發(fā)的時(shí)間和成本.

然而,模型驅(qū)動(dòng)開發(fā)生命周期一般較難涉及需求階段[6],而是從軟件的分析或設(shè)計(jì)開始,其主要原因是當(dāng)前工業(yè)界的軟件需求主要通過自然語言文本描述.但是,已有研究表明,安全關(guān)鍵軟件引起嚴(yán)重事故的問題鏈的最上端原因往往又是軟件需求尤其是安全性需求的問題[7].如著名的歐洲阿里安娜5火箭爆炸事件,事后分析其主要原因是阿里安娜5火箭是在阿里安娜4的基礎(chǔ)上開發(fā)的,它的初始加速度比后者高了很多,這導(dǎo)致阿里安娜5火箭的水平速度是阿里安娜4的6倍.但這一部分軟件恰恰是重用了阿里安娜4的模塊,開發(fā)者沒有意識(shí)到有關(guān)的需求已經(jīng)發(fā)生了變化,而沒有根據(jù)新的需求對(duì)重用的軟件進(jìn)行必要的修改[8].因此,如何將自然語言需求和模型驅(qū)動(dòng)開發(fā)方法進(jìn)行有效鏈接,即實(shí)現(xiàn)自然語言需求到形式化設(shè)計(jì)模型的自動(dòng)或半自動(dòng)轉(zhuǎn)換是模型驅(qū)動(dòng)開發(fā)方法在安全關(guān)鍵軟件設(shè)計(jì)與開發(fā)中實(shí)際應(yīng)用的一個(gè)主要挑戰(zhàn)[6,9,10].

目前,安全關(guān)鍵軟件的需求表達(dá)方式主要包括自然語言自由文本或限定自然語言文本(模板、表格等),用例圖以及少量直接使用形式化的需求描述方式等.而常用于模型驅(qū)動(dòng)開發(fā)的建模語言主要包括UML、SysML、AADL、EAST-ADL等,其中AADL(Architecture Analysis & Design Language)[11]是由美國汽車工程師協(xié)會(huì)SAE(Society of Automotive Engineers)提出的面向安全關(guān)鍵嵌入式系統(tǒng)的一種建模語言,并發(fā)布為SAE AS5506標(biāo)準(zhǔn).AADL采用單一模型支持多種分析的方式,支持對(duì)安全關(guān)鍵嵌入式系統(tǒng)的軟硬件混合建模,將系統(tǒng)設(shè)計(jì)、分析、驗(yàn)證、自動(dòng)代碼生成等關(guān)鍵環(huán)節(jié)融合于統(tǒng)一框架之下[30],是一種非常適用于安全關(guān)鍵系統(tǒng)的體系結(jié)構(gòu)建模與分析語言.

我們將已有需求表達(dá)到設(shè)計(jì)模型的轉(zhuǎn)換分為以下三類:

1)針對(duì)自由文本描述的軟件需求,通過自然語言處理(Natural Language Processing,NLP)的方式解析自由文本,并對(duì)解析結(jié)果進(jìn)行分析處理,最后轉(zhuǎn)換到設(shè)計(jì)模型.例如Keletso J.Letsholo等提出的TRAM(Tool for Transforming Textual Requirements into Analysis Models)方法[12],主要考慮自然語言需求到UML類圖的轉(zhuǎn)換,而Imran Sarwar Bajwa等則提出自然語言需求到的UML類圖的文本說明即OCL(Object Constraint Language)的轉(zhuǎn)換[13];

2)給出結(jié)構(gòu)化的限定自然語言需求表達(dá)方式,然后轉(zhuǎn)換到設(shè)計(jì)模型.挪威Simula實(shí)驗(yàn)室Tao Yue等提出的RUCM(Restriced Use Case Modeling)[14,15]方法是通過對(duì)UML用例圖的文本說明進(jìn)行自然語言限定,以此降低自然語言帶來的二義性與不精確性,并基于RUCM給出了aToucan工具[16],支持RUCM到UML活動(dòng)圖、順序圖等的自動(dòng)化生成;正在制定的SysML V2.0也將會(huì)為SysML需求圖中的文本說明設(shè)計(jì)自然語言約束規(guī)則,從而減少SysML建模過程中由自然語言帶來的二義性等問題;由Rolls Royce 公司提出的EARS (Easy Approach to Requirements Syntax)[17,18]方法則是提出了一些簡單需求結(jié)構(gòu)來捕獲和表達(dá)用戶需求,從而降低自然語言需求的二義性;

3)針對(duì)半形式化或形式化需求模型,抽取相關(guān)信息轉(zhuǎn)換到設(shè)計(jì)模型,如Jonathan Lasalle等提出的SysML到UML的轉(zhuǎn)換[19]、Van der Gaag等提出的SysML到SLIM的轉(zhuǎn)換[20]等.

限定自然語言是一種重要的需求表達(dá)方式,它既能夠減少自然語言帶來的二義性,又能夠較少改變工程師已有的需求撰寫習(xí)慣.但是已有工作較少面向安全關(guān)鍵軟件需求,同時(shí),還沒有考慮到AADL設(shè)計(jì)模型的自動(dòng)轉(zhuǎn)換.另外,在AADL模型驗(yàn)證與分析方面,驗(yàn)證性質(zhì)一般包括功能正確性、時(shí)間正確性和資源利用正確性等多個(gè)方面,目前主要是將AADL模型轉(zhuǎn)換到另外一種已有的形式化工具并通過模型檢測(cè)的方式進(jìn)行形式化驗(yàn)證,例如:AADL2Fiacre[21]AADL2BIP[22],AADL2IF[23],AADL2ACSR[24],AADL2RT-Maude[25],AADL2Lustre[26],AADL2Signal[27],AADL2TASM/UPPAAL[28]等.但是模型檢測(cè)方法容易存在狀態(tài)空間爆炸問題,基于Contract理論的組合驗(yàn)證方法成為AADL模型驗(yàn)證的一個(gè)新的研究熱點(diǎn).

因此,本文提出一種基于限定自然語言的安全關(guān)鍵軟件需求建模及其到AADL模型的自動(dòng)轉(zhuǎn)換方法.主要包括:首先,在綜合分析RUCM[14]、EARS[17]等需求表達(dá)方式的基礎(chǔ)上,提出基于限定自然語言需求模板的需求規(guī)約方法RNLreq,該規(guī)約方法能夠在盡量不改變工程師的需求撰寫習(xí)慣的前提下,降低自然語言需求存在的二義性與模糊性.其次,給出基于元模型的RNLreq到AADL模型的自動(dòng)轉(zhuǎn)換方法RNL2AADL.為了支持AADL模型的形式化驗(yàn)證,我們提出一種結(jié)構(gòu)化的驗(yàn)證性質(zhì)描述模板,并自動(dòng)轉(zhuǎn)換到AADL組合驗(yàn)證附件AGREE(Assume Guarantee REasoning Environment)Annex,以支持對(duì)AADL模型進(jìn)行組合驗(yàn)證[29].此外,我們?cè)贏ADL開源建模工具OSATE[18]中實(shí)現(xiàn)工具原型,并給出案例分析.

論文第二節(jié)介紹AADL語言的基本建模概念及其組合驗(yàn)證擴(kuò)展附件AGREE Annex.第三節(jié)給出限定自然語言需求建模方法RNLreq;第四節(jié)給出基于元模型的RNL2AADL模型轉(zhuǎn)換方法;第五節(jié)給出工具實(shí)現(xiàn)與案例分析;第六節(jié)對(duì)相關(guān)工作進(jìn)行分析;第七節(jié)是本文的總結(jié)和展望.

2 體系結(jié)構(gòu)分析與設(shè)計(jì)語言AADL

體系結(jié)構(gòu)分析與設(shè)計(jì)語言AADL是一種面向安全關(guān)鍵嵌入式系統(tǒng)的軟硬件建模語言,本節(jié)主要介紹AADL基本建模概念及基于Contract理論的AADL組合驗(yàn)證擴(kuò)展附件AGREE Annex.

2.1 AADL基本建模概念

2004 年,美國汽車工程師協(xié)會(huì)SAE(society of automotive engineers)在MetaH、UML等建模語言的基礎(chǔ)上,提出了嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)分析與設(shè)計(jì)語言AADL[11],目的是提供一種標(biāo)準(zhǔn)而又足夠精確的方式,設(shè)計(jì)與分析嵌入式實(shí)時(shí)系統(tǒng)的軟、硬件體系結(jié)構(gòu)及功能與非功能性質(zhì),采用單一模型支持多種分析的方式,將系統(tǒng)設(shè)計(jì)、分析、驗(yàn)證、自動(dòng)代碼生成等關(guān)鍵環(huán)節(jié)融合于統(tǒng)一框架之下[30].AADL的這些特性使其具有廣闊的應(yīng)用前景,得到了以航空航天領(lǐng)域(如空客、波音、霍尼韋爾等)為首的歐美工業(yè)界的支持,此外學(xué)術(shù)界也對(duì)AADL也展開了深入的研究和擴(kuò)展,其中,美國卡耐基梅隆大學(xué)為AADL開發(fā)的開源集成開發(fā)環(huán)境OSATE已被廣泛使用.

安全關(guān)鍵系統(tǒng)是應(yīng)用軟件、運(yùn)行時(shí)環(huán)境以及硬件平臺(tái)深度融合的復(fù)雜系統(tǒng),AADL語言與之對(duì)應(yīng)地提供了軟件體系結(jié)構(gòu)、運(yùn)行時(shí)環(huán)境以及硬件體系結(jié)構(gòu)的建模概念[30].

AADL是一種基于構(gòu)件(Component)的軟硬件建模語言,其軟件構(gòu)件主要用于描述系統(tǒng)的軟件體系結(jié)構(gòu),主要包括線程(Thread)、線程組(ThreadGroup)、進(jìn)程(Process)、數(shù)據(jù)(Data)、子程序(Subprogram)等;硬件構(gòu)件主要用于描述系統(tǒng)的硬件體系結(jié)構(gòu),主要包括處理器(Processor)、虛擬處理器(VirtualProcessor)、存儲(chǔ)器(Memory)、外設(shè)(Device)、總線(Bus)、虛擬總線(VirtualBus)等;此外,AADL還提供了系統(tǒng)構(gòu)件(System),整合分發(fā)協(xié)議(Dispatch)、通信協(xié)議(Communication)、調(diào)度策略(Scheduling)、模式變換協(xié)議(ModeChange)以及分區(qū)機(jī)制(Partition)等屬性來描述系統(tǒng)的運(yùn)行時(shí)環(huán)境,從而層次化地建立系統(tǒng)的體系結(jié)構(gòu)模型.

在每個(gè)構(gòu)件中,AADL通過特征features(port、dataaccess)表示構(gòu)件的事件、數(shù)據(jù)交互端口,通過連接connection描述構(gòu)件間的交互行為,通過流flow描述系統(tǒng)中信息傳輸?shù)倪壿嬄窂?通過屬性property描述體系結(jié)構(gòu)中的約束條件,通過模式mode描述運(yùn)行時(shí)體系結(jié)構(gòu)的動(dòng)態(tài)演化等.

此外,AADL定義了屬性集擴(kuò)展和附件擴(kuò)展兩種方式,進(jìn)一步豐富了AADL語言的表達(dá)能力.其中,屬性集擴(kuò)展豐富了AADL在系統(tǒng)非功能約束方面的描述能力;而附件擴(kuò)展則增強(qiáng)了了AADL對(duì)構(gòu)件實(shí)際功能行為的詳細(xì)描述能力.

已有的擴(kuò)展附件主要有:Graphical AADL Notation Annex、Error Model Annex、Behavior Annex、Data Modeling Annex、ARINC653 Annex以及AGREE Annex等.

2.2 AADL AGREE Annex

一個(gè)嵌入式系統(tǒng)通常都會(huì)包含由不同領(lǐng)域計(jì)算模型組成的獨(dú)立部分,每個(gè)獨(dú)立部分都按照一定標(biāo)準(zhǔn)封裝成構(gòu)件(Component).隨著嵌入式系統(tǒng)功能不斷加強(qiáng),軟件規(guī)模和復(fù)雜性迅速提高,系統(tǒng)構(gòu)件化特征顯著,由此產(chǎn)生的狀態(tài)空間爆炸問題使得傳統(tǒng)的單構(gòu)件/單模塊形式化驗(yàn)證技術(shù)已經(jīng)無法滿足實(shí)際需求.因此,組合驗(yàn)證理論被引入系統(tǒng)體系結(jié)構(gòu)的驗(yàn)證過程中.組合驗(yàn)證技術(shù)在傳統(tǒng)單構(gòu)件驗(yàn)證的基礎(chǔ)上,以下層構(gòu)件所滿足的性質(zhì)作為上層構(gòu)件驗(yàn)證的基礎(chǔ),將系統(tǒng)驗(yàn)證分解成底層構(gòu)件的形式化驗(yàn)證及不同體系結(jié)構(gòu)層次的邏輯推理與組合,降低了系統(tǒng)形式化驗(yàn)證的實(shí)現(xiàn)難度.

基于契約(Contract)的組合驗(yàn)證方法是一種常見的組合驗(yàn)證方法,一個(gè)基本的構(gòu)件契約具有如下描述:Contract=(Assume,Guarantee),其中Assume為假設(shè)部分,描述構(gòu)件對(duì)運(yùn)行環(huán)境的需求;Guarantee為保證部分,描述當(dāng)運(yùn)行環(huán)境被滿足時(shí),構(gòu)件可保證的外部行為特性,及構(gòu)件承擔(dān)的責(zé)任[38].對(duì)于一個(gè)軟件構(gòu)件而言,假設(shè)為功能正常執(zhí)行的要求,保證為在要求滿足時(shí)的產(chǎn)出結(jié)果.

AADL作為一種面向構(gòu)件化、層次化的嵌入式軟硬件體系結(jié)構(gòu)描述語言,對(duì)組合驗(yàn)證也提供支持.2012年Rockwell Collins公司基于AADL開源工具環(huán)境OSATE提出了假設(shè)保證推理環(huán)境AGREE[29],并發(fā)布為AADL組合驗(yàn)證附件AGREE Annex,旨在構(gòu)建一套基于AADL的組合驗(yàn)證平臺(tái)工具,用于支持在AADL設(shè)計(jì)模型的基礎(chǔ)上對(duì)嵌入式軟硬件體系結(jié)構(gòu)進(jìn)行組合驗(yàn)證.AGREE Annex以附件的形式,增強(qiáng)了AADL對(duì)驗(yàn)證性質(zhì)、邏輯推理公式等的表達(dá)能力.以下給出AGREE的EBNF語法:

AgreeSubclause::=(SpecStatement)+;

SpecStatement::=

′assume′STRING′:′Expr′;′

| ′guarantee′STRING′:′Expr′;′

|EqStatement

|PropertyStatement

|ConstStatement

|FunDefExpr

|NodeDefExpr

| ′assert′Expr′;′

| ′lift′NestedDotId′;′

|LemmaStatement;

LemmaStatement::=′lemma′STRING′:′Expr′;′;

PropertyStatement::=′property′ID′=′Expr′;′;

ConstStatement::=′const′ID′:′Type′=′Expr′;′;

EqStatement::=′eq′Arg(′,′Arg)* ′=′Expr′;′;

FunDefExpr::=′fun′ID′(′Arg(′,′Arg)* ′:′Type′=′Expr′;′;

NodeDefExpr::=′node′ID′(′Arg(′,′Arg)* ′)′ ′:′ ′returns′′(′Arg(′,′Arg)* ′)′ ′;′NodeBodyExpr;

Arg::=ID′:′Type;

NodeBodyExpr::=(′var′ (Arg′;′)+)?

′let′ (NodeStmt)+′tel′ ′;′;

NodeStmt::=

Arg(′,′Arg)* ′=′Expr′;′

|LemmaStatement

在AGREE Annex中,assume和guarantee分別表示對(duì)應(yīng)構(gòu)件對(duì)環(huán)境的需求,以及需求滿足條件下所能保證的輸出.此外,AGREE還定義了等式(Eq)、性質(zhì)語句(Property)、常量(Const)、函數(shù)(Fun)、節(jié)點(diǎn)(Node)、斷言(Assert)、提升(Lift)、引理(Lemma)等,用以描述組件的執(zhí)行過程.

AGREE在OSATE的基礎(chǔ)上,通過插件的形式提供了AGREE解析器,將AGREE Annex解析成AGREE抽象語法樹,并提供AGREE分析器,將AGREE抽象語法樹轉(zhuǎn)換成同步語言Lustre程序,最后通過JKind模型檢測(cè)工具對(duì)生成的Lustre程序進(jìn)行驗(yàn)證,最終反饋出AGREE Annex中可能存在的缺陷或錯(cuò)誤.

3 限定自然語言需求規(guī)約方法

本文在RUCM、SPARDL和EARS等基礎(chǔ)上,提出限定自然語言需求規(guī)約方法RNLreq,主要包括四部分,數(shù)據(jù)字典、領(lǐng)域詞庫、需求模板以及限定句式.

3.1 領(lǐng)域詞庫和數(shù)據(jù)字典

1)領(lǐng)域詞庫,主要針對(duì)具體的領(lǐng)域需求,將需求中所涉及的各種對(duì)象名詞集中起來,形成一份參照列表,如專有的系統(tǒng)名、軟件模塊名、硬件設(shè)備、模式變遷狀態(tài)等.

領(lǐng)域詞庫中的名詞可以定義為一個(gè)三元組,Noun::=,包括名詞中文名稱,英文名稱以及類型,其中類型可以是系統(tǒng)、子系統(tǒng)、任務(wù)、子任務(wù)、共享功能模塊、外設(shè)、總線、存儲(chǔ)器、處理器、模式等類型.

證法2 不妨設(shè)a>0,b>0,c<0.如圖2，在平面直角坐標(biāo)系中，確定兩個(gè)固定點(diǎn)以點(diǎn)A為圓心，線段AB為半徑作⊙A，⊙A與x軸相交于點(diǎn)C和點(diǎn)D，與y軸相交于點(diǎn)E.

2)數(shù)據(jù)字典,將需求文檔中的各種數(shù)據(jù)都集中起來,并采用比較規(guī)范的方式對(duì)它們的屬性進(jìn)行描述,主要包括軟件系統(tǒng)中的各種輸入數(shù)據(jù)、輸出數(shù)據(jù)、靜態(tài)數(shù)據(jù)等.

數(shù)據(jù)字典中每條數(shù)據(jù)可以定義為一個(gè)七元組,Data::=,包括中文名稱、英文名、數(shù)據(jù)組成/類型、數(shù)據(jù)單位、數(shù)據(jù)值域、數(shù)據(jù)精度、數(shù)據(jù)描述等屬性.其中DataType可以是基本數(shù)據(jù)類型(Integer,Boolean,String等),也可以是由多個(gè)數(shù)據(jù)組成的復(fù)雜數(shù)據(jù)類型(類似C語言中的結(jié)構(gòu)體).

3.2 需求模板

嵌入式系統(tǒng)常常使用系統(tǒng)、子系統(tǒng)、功能、子功能的概念來對(duì)軟件進(jìn)行分層組織,并通過共享模塊調(diào)用來實(shí)現(xiàn)跨系統(tǒng)或跨功能之間的模塊共享.在RNLreq 中,系統(tǒng)、子系統(tǒng)、功能、子功能以及共享模塊都采用需求模板的方式表達(dá)需求,需求模板之間的層次關(guān)系則顯式地表達(dá)軟件系統(tǒng)的體系結(jié)構(gòu).其中,系統(tǒng)(System)需求模板可以分解為若干個(gè)子系統(tǒng)(Subsystem)需求模板,而子系統(tǒng)可以繼續(xù)劃分為多個(gè)子系統(tǒng)或功能(Function),功能也可劃分為若干個(gè)子功能(SubFunction).此外,共享功能模塊(ShareFuctionBlock)作為獨(dú)立的模塊掛靠在系統(tǒng)中,可以被功能或子功能調(diào)用,共享功能模塊可以用于描述一些經(jīng)常被調(diào)用到的算法(如傅里葉變換)或與外設(shè)交互(如從RS422總線讀寫數(shù)據(jù)).

限定自然語言需求模板是對(duì)需求的一種規(guī)范描述.根據(jù)文獻(xiàn)[18]的建議,本文根據(jù)系統(tǒng)分解的思想,分別從系統(tǒng)、子系統(tǒng)、功能、子功能4個(gè)層次進(jìn)行需求描述.基本的需求模板如表1所示.

需求模板由標(biāo)識(shí)符ID(Component_ID)、名稱(Component_Name)、輸入(Input)、輸出(Output)、子模塊成組成(Component_Composition)以及需求約束(Requirement_Constraint)等項(xiàng)組成.其中ID是每個(gè)模板即軟件模塊的唯一標(biāo)識(shí);名稱是從領(lǐng)域詞庫中選擇獲得,實(shí)現(xiàn)中英文對(duì)照,這樣可以減少手工輸入帶來的不一致性;輸入輸出描述了軟件模塊與外界的交互,一般分為數(shù)據(jù)和事件兩種類型.

表1 限定自然語言需求模板
Table 1 Restricted natural language requirement template

ID唯一標(biāo)識(shí)符構(gòu)件名稱限定為名詞,或者多個(gè)名字的組合或簡寫,用于描述系統(tǒng)/子系統(tǒng)/功能/子功能的名稱輸入系統(tǒng)/子系統(tǒng)/功能/子功能的輸入事件/數(shù)據(jù),沒有寫NONE輸出系統(tǒng)/子系統(tǒng)/功能/子功能的輸出事件/數(shù)據(jù),沒有寫NONE組成子系統(tǒng)一個(gè)復(fù)雜系統(tǒng)可以分解為若干子系統(tǒng)功 能每個(gè)系統(tǒng)將實(shí)現(xiàn)若干功能子功能每個(gè)功能可以分解為若干原子功能功能需求每個(gè)功能單元在功能方面的描述模式變換每個(gè)功能單元在模式變換方面的描述性能需求規(guī)定每個(gè)功能單元在性能方面的約束接口需求各層組件數(shù)據(jù)流、控制流的協(xié)議描述設(shè)計(jì)約束軟硬件設(shè)計(jì)約束,安全性可靠性的約束描述

需求約束包括功能處理(Functional_Process)、模式變換(Mode_Transition)、性能需求(Performance_Requirement)、接口需求(Interface_Requirements)及設(shè)計(jì)約束(Design_Restraints)等.其中功能處理通過事件流來表達(dá)正常功能處理流程,其中的具體功能需求可以標(biāo)定為安全關(guān)鍵功能;模式與模式變換用來描述當(dāng)前模塊在上一層系統(tǒng)中所處的工作模式(即源模式),以及當(dāng)前模塊的模式變換的觸發(fā)條件和目標(biāo)模式;性能需求則是對(duì)軟件完成任務(wù)的能力做出的一些定量要求,如:實(shí)時(shí)性、精度、功耗、最大處理能力等;接口需求描述各模塊與外界交互接口的要求,如接口數(shù)據(jù)傳輸協(xié)議等;設(shè)計(jì)約束描述功能模塊在軟硬件、安全性、可靠性等方面的約束.

由此,本文給出限定自然語言需求模板的EBNF語法如下:

RNLreq::=GlossaryDictionaryTemplateSetSentencePatterns

Glossary::=Noun+;

Noun=(NounZhNameNounEnNameNounType)+;

DataDictionary::=Data+;

Data=(DataNameDataEnNameDataTypeDataUnitDataRangeDataAccuracyDataDescription)+;

TemplateSet::=(RNLreq_Template)+;

RNLreq_Template::=Component_IDComponent_NameInputOutputComponent_CompositionRequirement_Constraints

Requirement_Constraint::=Functional_Process[Performance_requirements][Mode_Transitions][Interface_requirements][Design_constraints];

Noun_Category::=Software_Category

|HardWare_Category

Template_Category::=′System′ |′Subsystem′|′Function′ |′SubFunction′|′Shared_Function_Block′;

HardWare_Category::=′Device′|′Bus′

|′Processor′|′Memory′;

Component_Name::=Noun_zh;

Component_Composition::=(RNL_Req_Template)+

Functional_Requirements::=(Sentence_Pattern)+

Performance_requirements::=(Sentence_Pattern)+

Mode_Transitions::=(Sentence_Pattern)+

Interface_requirements::=(Sentence_Pattern)+

Design_constraints::=(Sentence_Pattern)+

Input::={VarName_zh[Assume_Specification]}+;

Output::={VarName_zh[Guarantee_Specification]}+;

其中,Noun表示領(lǐng)域?qū)Ｓ忻~,Data表示需求中的數(shù)據(jù),對(duì)應(yīng)Component_Name必須是領(lǐng)域詞庫中已“注冊(cè)”的名詞,Input、Output必須是“數(shù)據(jù)字典”中已注冊(cè)的數(shù)據(jù),Component_Composition描述需求模板間的層次關(guān)系,Functional、Performance、ModeTransitions、Interface、Designconstraints分別描述功能、性能、模式變換、接口、設(shè)計(jì)約束等不同類型的需求.

3.3 限定句式

基于限定自然語言的需求規(guī)約方法不僅包括在需求組織結(jié)構(gòu)上的約束,還包括對(duì)每一條需求描述的約束.在已有工作[31]中我們已經(jīng)給出了限定自然語言需求模板的通用約束規(guī)則,用于限定自然語言的表述方式,以此減少在需求規(guī)約過程中人為引入的二義性和不確定性,通用約束規(guī)則如表2所示.

表2 通用自然語言約束規(guī)則
Table 2 General restriction rules for natural language

約束規(guī)則描述R1句子的主語必須是模塊名稱或“該模塊”R2只使用陳述句R3只使用現(xiàn)在時(shí)R4用主動(dòng)語態(tài)而不用被動(dòng)語態(tài)R5不使用情態(tài)動(dòng)詞(如大概)、代詞以及表示否定含義的副詞/形容詞R6只使用簡單句R7準(zhǔn)確的描述模塊間的交互,主語和賓語都不能丟失R8不要使用分詞短語作狀語修飾詞R9以一致的方式使用詞語,使用固定的名詞來描述某個(gè)事物

本文在已有工作的基礎(chǔ)上,分別為各類需求約束制定了一系列的需求描述限定句式,本文以功能處理為例進(jìn)行說明.

針對(duì)功能處理,本文指定了5種限定句式,涵蓋在功能處理中常用的時(shí)間約束、判斷選擇等關(guān)系,具體如表3所示.

其中,Behavior表示一個(gè)或一組順序執(zhí)行的簡單操作,操作可以是數(shù)據(jù)發(fā)收、數(shù)據(jù)賦值、功能模塊調(diào)用等;Condition表示功能執(zhí)行的條件,可以分為觸發(fā)條件(當(dāng)接收到觸發(fā)事件時(shí)執(zhí)行)和判斷條件(當(dāng)值滿足一定條件時(shí)執(zhí)行)兩種;TimeRestrain表示Behavior執(zhí)行的時(shí)間約束.

基于上述的約束規(guī)則及限定句式,本文給出一個(gè)導(dǎo)航、制導(dǎo)與控制系統(tǒng)中的實(shí)際模塊作為RNLreq的示例如表4所示.

表3 功能需求描述句型
Table 3 Sentence patterns for functional requirements

NOID唯一標(biāo)識(shí)符SP1Behavior表示一個(gè)簡單句,單純執(zhí)行一條功能;SP2Condition+Behavior表示在某種條件下完成一個(gè)功能行為的執(zhí)行SP3TimeRestrain+Behavior表示在一定時(shí)間范圍內(nèi)完成一個(gè)功能行為;SP4Condition+Behavior+else+Behavior表示在一定條件下完成一個(gè)功能行為,若不滿足條件則執(zhí)行另一個(gè)功能行為SP5TimeRestrain+ Condition+Behavior表示在連續(xù)時(shí)間范圍內(nèi)一直滿足某些條件,執(zhí)行一個(gè)功能行為

表4 GNCC控制數(shù)據(jù)轉(zhuǎn)發(fā)模塊
Table 4 GNCC data retransmission module

名稱GNCC控制數(shù)據(jù)轉(zhuǎn)發(fā)模塊IDTX_GNCC是否安全關(guān)鍵是輸入數(shù)據(jù)GNCC數(shù)據(jù)轉(zhuǎn)發(fā)控制指令GNCC控制數(shù)據(jù)輸出數(shù)據(jù)GNCC控制數(shù)據(jù)MF標(biāo)志功能處理1.在10ms內(nèi),該模塊向GNCC發(fā)送握手信息.2.如果功能處理1失敗,那么執(zhí)行3次功能處理1;如果3次功能處理1失敗,那么執(zhí)行賦值MF標(biāo)志位為1,該模塊向日志模塊發(fā)送錯(cuò)誤信息.3.該模塊向GNCC發(fā)送GNCC控制數(shù)據(jù).4.該模塊向GNCC發(fā)送結(jié)束信息.性能需求1.該模塊的周期=50ms.

4 RNL2AADL自動(dòng)轉(zhuǎn)換方法

在RNLreq的基礎(chǔ)上,本文通過模型轉(zhuǎn)換技術(shù)實(shí)現(xiàn)RNLreq到AADL初始模型的自動(dòng)轉(zhuǎn)換.

從限定自然語言需求模板到AADL模型自動(dòng)轉(zhuǎn)換的主要包括兩部分:

1)數(shù)據(jù)字典與領(lǐng)域詞庫的轉(zhuǎn)換:數(shù)據(jù)字典轉(zhuǎn)換到AADL數(shù)據(jù)構(gòu)件(DataComponent)及數(shù)據(jù)構(gòu)件的屬性(Properties),例如第二章示例中的GNCC控制數(shù)據(jù)需在數(shù)據(jù)字典中定義,并將被轉(zhuǎn)換到AADL的數(shù)據(jù)構(gòu)件,其數(shù)據(jù)組成將轉(zhuǎn)換到數(shù)據(jù)構(gòu)件的子構(gòu)件(subcomponent).由于領(lǐng)域詞庫主要用于領(lǐng)域?qū)Ｓ性~匯的“注冊(cè)”與中英文映射,因此無需轉(zhuǎn)換到特定的AADL模型元素.

2)限定自然語言需求模板的轉(zhuǎn)換:在RNL2AADL自動(dòng)轉(zhuǎn)換的實(shí)現(xiàn)過程中,文本提出中間轉(zhuǎn)換模型RAInterM(RNL2AADL Intermediate Model),將需求到AADL模型的轉(zhuǎn)換(多對(duì)多關(guān)系)拆分成限定自然語言需求到RAInterM(多對(duì)一關(guān)系)以及RAInterM到AADL(一對(duì)多關(guān)系)的轉(zhuǎn)換關(guān)系,從而簡化了轉(zhuǎn)換的實(shí)現(xiàn)并保證了轉(zhuǎn)換的可擴(kuò)展性.

4.1 RNLreq元模型

基于第二章給出的RNLreq的EBNF語法規(guī)則,本文給出了RNLreq的元模型如圖1所示.

RNLreq元模型主要分為三個(gè)部分:DataDictionary&Glossary,Template,以及Sentence.DataDictionary&Glossary表示表示數(shù)據(jù)字典及領(lǐng)域詞庫,其中DataWord和Term分別表示數(shù)據(jù)和領(lǐng)域詞匯.Template表示各層模板,每一類模板都繼承自AbstractTemplate,且低層模板可以是高層模板的父模板.各層模板中每一類需求都是由一組限制句式描述的,每一類限制句式繼承于Sentence,而Sentence中的gen()方法中定義了該句式的轉(zhuǎn)換規(guī)則.

圖1 RNLreq元模型Fig.1 Meta-Model of RNLreq

4.2 RAInterM元模型

為了簡化RNL2AADL的轉(zhuǎn)換,并保證轉(zhuǎn)換的可擴(kuò)展性,本文提出RAInterM中間模型,并給出其元模型如圖2所示:

其中Model是頂層概念,表示整個(gè)系統(tǒng);Component表示系統(tǒng)中的實(shí)體;StateMachine可以分為MTStateMachine和BHVStateMachine兩種,分別對(duì)應(yīng)RNLreq中的模式變換和功能處理,以及AADL中的modetransition和BehaviorAnnex;Connection和Port對(duì)應(yīng)RNLreq中的輸入輸出,表示系統(tǒng)中構(gòu)件間的通信通道,其中Port中定義了端口的數(shù)據(jù)類型,Property定義了Component等元素的約束性質(zhì).

圖2 RAInterM元模型Fig.2 Meta-Model of RAInterM

4.3 RNLreq到RAInterM的轉(zhuǎn)換

基于RNLreq及RAInterM元模型,本文給出RNLreq到RAInterM的轉(zhuǎn)換算法如算法1所示:

算法1.

Transformation from RNL2AADL to RAInterM

Input:RNL2AADL

Output:RAInterM

1:foreachTemplatetinRNL2AADL.getTemplatesdo

2:Componentc=newComponent(t.getType);

3:foreachPortpinRAInterM.getPortsdo

4:p.gen(RAInterM,c,p.PortType);

5:endfor

6:endfor

7:foreachPortpinRAInterM.getPortsdo

8:ifp.NoSameNamePortthen

9:p:type=DATAACCESS;

10:RAInterM.add(data=newComponent(DATA));

11:RAInterM.addDataAccessConnections(p,data);

12:else

13:RAInterM.addConnections(p,p.getSameNamePort);

14:endif

15:endfor

16:foreachSentencesint.getRequirementsdo

17:s.gen(RAInterM,c);

18: // Each type of requirements transformed into different parts in RAInterM

19:endfor

大致思路如下:

1)系統(tǒng)框架的轉(zhuǎn)換:首先將整個(gè)系統(tǒng)的框架轉(zhuǎn)換到中間模型RAInterM,其中模板轉(zhuǎn)換到的Component組件,輸入輸出轉(zhuǎn)換到Port,其中端口上添加的約束性質(zhì)對(duì)應(yīng)轉(zhuǎn)換到端口所關(guān)聯(lián)Connection的Property中.

2)Connection 生成:在需求模板中,聯(lián)通的輸入輸出端口在定義時(shí)數(shù)據(jù)類型是相同的.因此,相同數(shù)據(jù)類型的Port通過Connection連接起來,而單獨(dú)的Port通過共享數(shù)據(jù)組件以共享數(shù)據(jù)訪問的方式建立Connection,其中輸入輸出端口上的約束性質(zhì)轉(zhuǎn)換到Port的properties.

3)需求的轉(zhuǎn)換:針對(duì)RNLreq 中定義的多種需求,如功能處理、性能需求、接口需求、安全性設(shè)計(jì)約束、模式變換等,通過在各需求描述句式的gen()方法中定義各種需求描述句式到中間模型的轉(zhuǎn)換方法,實(shí)現(xiàn)需求描述到中間模型的轉(zhuǎn)換,如模板A發(fā)送數(shù)據(jù)D到模板B,可以轉(zhuǎn)換成RAInterM模型中,componentA的outportD與componentB的inportD相連,并在componentA與B的最近公共父組件的BHVStateMachine中描述對(duì)應(yīng)子組件發(fā)送數(shù)據(jù)這一行為.

4.4 RAInterM到AADL的轉(zhuǎn)換

在從RNLreq到RAInterM的轉(zhuǎn)換完成之后,我們?cè)俳o出從RAInterM到AADL的轉(zhuǎn)換規(guī)則,其中AADL的元模型可以在開源AADL工具環(huán)境(OSATE)中直接獲得.本文給出的RNLreq到AADL的轉(zhuǎn)換算法,如算法2所示:

算法2.

Transformation from RAInterM to AADL

Input:RAInterM

Output:AADL

1:foreachComponentcin

RAInterM.getComponentsdo

2:ifc.isSystemthen

3:AADL:add(newSystemn);

4:elseifc.isProcessthen

5:AADL:add(newProcessn);

6:elseifc.isThreadthen

7:AADL:add(newThreadn);

8:elseifc.isSubprogramthen

9:AADL:add(newSubprogramn);

10:else

11:AADL.add(newAbstractn);

12:endif

13:AADL.addInstance(n.newInstance);

14:c.getPorts->n.features;

15:c.SubComponents->n.instance.subcomponents;

16:c.Connections->n.instance.connections;

17:c.MTStateMachine.getStates->n.instance.modes;

18:c.MTStateMachine.getTransitions->n.instance.transitions;

19:c.Properties->n.instance.properties;

20:c.BHVStateMachine->n.instance.BA;

21:endfor

RAInterM到AADL的轉(zhuǎn)換主要包括兩部分:

1)AADL組件類型的轉(zhuǎn)換,主要是對(duì)AADL組件類型和端口聲明的生成,其中RAInterM中component轉(zhuǎn)換到AADL中的軟硬件構(gòu)件,如system、process、thread、bus、processor、device等,而port則轉(zhuǎn)換到AADL聲明中的features,port上對(duì)應(yīng)的約束規(guī)則轉(zhuǎn)換到AGREE Annex的assume與guarantee.

2)AADL組件實(shí)例化的轉(zhuǎn)換,主要包括AADL模型的主體信息,其中,RAInterM中的component間關(guān)系轉(zhuǎn)換到AADL的軟硬件組件關(guān)系,connection、property、statemachine等轉(zhuǎn)換到AADL中的連接(Connection)、性質(zhì)(Property)、模式變化(modetransition)、行為附件(behaviorannex)等.

完成初始AADL模型的自動(dòng)轉(zhuǎn)換之后,還需要通過精化的方式進(jìn)一步完善AADL設(shè)計(jì)模型,使其能夠更加完整地表達(dá)安全關(guān)鍵軟件設(shè)計(jì).

4.5 AGREE Annex自動(dòng)生成

通過RNLreq到AADL的轉(zhuǎn)換,生成初始AADL設(shè)計(jì)模型.為了增強(qiáng)AADL設(shè)計(jì)模型對(duì)組合驗(yàn)證的支持,需在AADL設(shè)計(jì)模型中添加組合驗(yàn)證所需的約束信息.因此,本文面向AGREE假設(shè)保證附件,提出一個(gè)面向組合驗(yàn)證的性質(zhì)描述模板,用以輔助用戶增加組合驗(yàn)證所需的相關(guān)信息,其結(jié)構(gòu)如表5所示.

表5 組合驗(yàn)證性質(zhì)描述模板
Table 5 Compositional verification specification template

需求模板名稱對(duì)應(yīng)AADL設(shè)計(jì)模型中的一個(gè)組件假設(shè)該組件所需的外界條件,如輸入值的范圍等保證該組件在外界條件滿足的前提下所能保證的性質(zhì)約束性質(zhì)該組件中涉及的數(shù)據(jù)的約束條件,可以是端口數(shù)據(jù)或臨時(shí)變量的約束不等式臨時(shí)變量中間計(jì)算過程的臨時(shí)變量等式中間數(shù)據(jù)計(jì)算過程

其中,需求模板名稱對(duì)應(yīng)AADL組件的名稱,假設(shè)和保證分別表示對(duì)應(yīng)AADL組件正常工作所需的外界條件及在該外界條件的前提下該組件所能保證的性質(zhì),約束性質(zhì)、臨時(shí)變量、等式等為驗(yàn)證求精過程中增加的中間過程.其中,約束性質(zhì)可以是從需求模板中性能需求、接口需求中抽取出來的約束條件;臨時(shí)變量和等式可以是需求模板中的功能需求、模式變換中抽取的組件內(nèi)功能執(zhí)行邏輯.

在工程師通過組合驗(yàn)證求精模板以自然語言的方式增加相關(guān)描述之后,可以自動(dòng)轉(zhuǎn)換成AADL AGREE Annex并插入到RNL2AADL生成的初始AADL模型中.

本文給出組合驗(yàn)證性質(zhì)描述模板到AADL AGREE Annex的轉(zhuǎn)換算法,如算法3所示:

算法3.

Transformation from VRT to AGREE

Input:VRT,AADL

Output:AGREE

1:foreachComponentcinAADL.getComponentsdo

2:VRTTemplatev=VRT.getVRTTemplate(c);

3:foreachAssumeStmtasinv.getAssumeStmtsdo

4:AGREE.getComponent(c).addAssumeStmt(cs);

5:endfor

3:foreachGuaranteeStmtasinv.getGuaranteeStmtsdo

4:AGREE.getComponent(c).addGuaranteeStmt(cs);

5:endfor

6:foreachConstStatementcsinv.getConstStatementsdo

7:AGREE.getComponent(c).addConstStatement(cs);

8:endfor

9:foreachPropertypinv.getPropertiesdo

10:AGREE.getComponent(c).addProperty(p);

11:endfor

12:foreachEqStatementesinv.getEqStatementsdo

13:AGREE.getComponent(c).addEqStatement(es);

14:endfor

15:endfor

在此基礎(chǔ)上,用戶可基于OSATE中集成的AGREE假設(shè)保證插件對(duì)AADL AGREE Annex進(jìn)行組合驗(yàn)證.

5 工具實(shí)現(xiàn)和案例分析

5.1 工具實(shí)現(xiàn)

基于限定自然語言的需求模型到AADL設(shè)計(jì)模型的轉(zhuǎn)換工具是基于AADL開源環(huán)境OSATE開發(fā)的,按照MVC的設(shè)計(jì)思想,將工具拆分為前端(模板、領(lǐng)域詞庫、數(shù)據(jù)字典的限定自然語言輸入方式等)、中間模型(RAInterM,數(shù)據(jù)字典、領(lǐng)域詞庫的數(shù)據(jù)模型等)和(后端)中間模型到AADL的代碼生成三個(gè)部分.其中,增加的組合驗(yàn)證性質(zhì)分別定義在模板、數(shù)據(jù)字典、Req2AADL和代碼生成等部分中,工具程序框架如圖3所示.

5.2 案例分析

導(dǎo)航、制導(dǎo)與控制系統(tǒng),即GNC系統(tǒng),是航天器在軌運(yùn)行的核心保障系統(tǒng),承擔(dān)著航天器姿態(tài)和軌道確定與控制的重要任務(wù),一般由導(dǎo)航傳感器、控制計(jì)算機(jī)和執(zhí)行機(jī)構(gòu)組成.其中,導(dǎo)航傳感器包括導(dǎo)航相機(jī)、星敏感器、陀螺、加速度計(jì)等,主要用于采集各種數(shù)據(jù);控制計(jì)算機(jī),也稱為姿態(tài)與軌道控制系統(tǒng)(Attitude and Orbit Control System,AOCS),通過收集和處理各種傳感器的測(cè)量數(shù)據(jù)來完成制導(dǎo)和控制任務(wù),主要執(zhí)行軌道確定、軌道控制、姿態(tài)確定、姿態(tài)控制等功能.

圖3 原型工具實(shí)現(xiàn)框架Fig.3 Framework of prototype tool

5.2.1 需求建模及AADL模型生成

GNC案例對(duì)應(yīng)的數(shù)據(jù)字典、領(lǐng)域詞庫如圖4所示:

圖4 GNC案例數(shù)據(jù)字典及領(lǐng)域詞庫Fig.4 GNC DataDictionary & Glossary

建立數(shù)據(jù)字典和領(lǐng)域詞庫后,通過需求模板進(jìn)行GNC需求規(guī)約,并對(duì)需求進(jìn)行精化,此處以GNC中姿態(tài)控制子系統(tǒng)為例,需求結(jié)構(gòu)如圖5所示,同時(shí)以圖6中的消初偏模塊(即消除星箭分離所產(chǎn)生的偏差)為例,給出其功能需求描述.

通過工具生成的AADL模型如圖7所示.

5.2.2 模型驗(yàn)證

在生成GNC案例的AADL模型之后,我們考慮對(duì)生成的AADL模型進(jìn)行形式化驗(yàn)證.在已有工作[31]中,我們已實(shí)現(xiàn)了單構(gòu)件驗(yàn)證工具AADL2TASM/UPPAAL.本文在對(duì)生成AADL模型進(jìn)行單構(gòu)件驗(yàn)證的基礎(chǔ)上,通過AGREE插件工具對(duì)AADL模型進(jìn)行組合驗(yàn)證.

首先,在RNL2AADL的基礎(chǔ)上,生成了AADL初始設(shè)計(jì)模型,以其中attitude_filter_init模塊為例,一個(gè)簡化的初始設(shè)計(jì)模型的代碼如圖5所示.

圖5 RNLreq描述GNC需求結(jié)構(gòu)Fig.5 Requirement structure of GNC in RNLreq

threadattitude_filter_init

features

Attitude_Measure:indataport

Base_Types::Integer;

Attitude_Angular_Belocity:indataport

Base_Types::Integer;

Attitude_Estimation:outdataport

Base_Types::Integer;

endattitude_filter_init;

在此基礎(chǔ)上,通過AGREE驗(yàn)證精化模板,對(duì)attitude_filter_init模塊進(jìn)行精化,添加假設(shè)、保證、約束性質(zhì)等組合驗(yàn)證信息.精化后Attitude_filter_init模塊對(duì)應(yīng)轉(zhuǎn)換出的AGREE Annex如下所示:

annexagree {**

constAttitude_Rate:real=1.2;

eqCompute_Attitude:real=Atti-

tude_Angular_Belocity * Attitude_Rate;

assume"Attitude_Filter input range ":Attitude_Measure<5;

assume"Attitude_Filter input range ":Attitude_Angular_Belocity>9;

guarantee"Attitude_Filter output range ":Atttude_Estimation < Attitude_Measure+Compute_Attitude;

**};

圖6 GNC案例消初偏模塊功能需求Fig.6 Functional requirement of initial offset elimination module in GNC

圖7 AADL模型圖形化表示Fig.7 AADL model expressed in graphics

最后,通過Osate的AADL AGREE 插件工具運(yùn)行執(zhí)行對(duì)AGREE附件的組合驗(yàn)證.

本文分別對(duì)GNC中的6項(xiàng)非功能性質(zhì)進(jìn)行驗(yàn)證,包括基于測(cè)速儀和節(jié)流閥的速度驗(yàn)證、基于導(dǎo)航相機(jī)和加速度計(jì)的加速度驗(yàn)證、對(duì)AOCS子系統(tǒng)執(zhí)行周期的驗(yàn)證、對(duì)AOCS外設(shè)電源分配的驗(yàn)證、對(duì)各執(zhí)行機(jī)構(gòu)并行工作情況的驗(yàn)證、對(duì)陀螺儀是否正常工作的驗(yàn)證.

以速度驗(yàn)證為例,驗(yàn)證性質(zhì)為當(dāng)輸入的速度值為0到150范圍內(nèi)時(shí),保證每個(gè)邏輯時(shí)間的速度差的絕對(duì)值小于2.基于此,通過本文提出的方法生成了相應(yīng)構(gòu)件中的assume和guarantee,并通過需求精化模板增加了中間計(jì)算過程,得到的父組件Terminal中的AGREE Annex代碼如下:

annexagree {**

constmax_accel:real=2.0;

assume"target speed is positive":

Targer_speed_Input.val >=0.0;

assume"reasonable target speed":

Targer_speed_Input.val < 150.0;

propertyconst_tar_speed=Agree_Nodes.H

(Targer_speed_Input.val=prev(Targer_speed_Input.val,0.0));

guarantee"actual speed is less than constant target speed":const_tar_speed => (Actual_Out.val <=Targer_speed_Input.val);

guarantee"acceleration is limited":Agree_Nodes.abs(Actual_Out.val-prev(Actual_Out.val,0.0)) < max_accel;

**};

測(cè)速儀中AGREE代碼如下:

annexagree {**

constP:real=0.2;

constD:real=0.1;

constI:real=0.1;

eqe:real=Targer_speed.val-Actual.val;

eqe_int:real=prev(e,0.0)+e;

eqe_dot:real=prev(e,0.0)-e;

equ:real=P*e+D*e_dot+I*e_int;

guarantee"Actuator":Actuator_Input=u;

guarantee"Differ Speed":Differ_speed.val=e;

**};

節(jié)流閥中AGREE代碼如下:

annexagree {**

guarantee"Throttle_Behavior":Actual.val=prev(Actual.val,0.0)+0.1*Actuator_Input;

**};

在此基礎(chǔ)上,可以通過AGREE組合驗(yàn)證插件對(duì)生成的AGREE代碼進(jìn)行驗(yàn)證,驗(yàn)證結(jié)果如圖8所示.

圖8 使用AGREE工具驗(yàn)證速度Fig.8 Verifying speed properties with AGREE

圖中可以看出,在給定的assume滿足,及給出的中間計(jì)算過程的情況下,檢測(cè)出性質(zhì)"accelerationislimited"無法滿足,從而可以說明模型中關(guān)于速度控制的功能構(gòu)件存在問題,進(jìn)而說明需求中存在不合理的設(shè)計(jì).

6 相關(guān)工作

本文的相關(guān)工作主要包括3部分:

1) 限定自然語言需求建模;

2) 自然語言需求到設(shè)計(jì)模型的自動(dòng)轉(zhuǎn)換;

3) 基于契約的組合驗(yàn)證.

6.1 限定自然語言需求建模

自然語言具有很好的表達(dá)能力,但是存在著二義性、模糊性以及難以自動(dòng)化分析處理等缺點(diǎn).Rolls Royce公司的Alistair Mavin等人針對(duì)用戶需求難以描述和表達(dá)的問題,在大量工程經(jīng)驗(yàn)的基礎(chǔ)上,提出了一種EARS(Easy Approach to Requirements Syntax)[17,18]方法進(jìn)行需求規(guī)約.該方法通過將需求分為6種類型,有效簡化了需求的描述與表達(dá)難度,同時(shí)有效降低自然語言的二義性.德國帕德博恩大學(xué)的J?rg Holtmann 教授等人針對(duì)汽車工程領(lǐng)域的軟件系統(tǒng)的需求規(guī)約展開研究,提出了一種受控自然語言(Controlled Natural Language,CNL)用于汽車領(lǐng)域嵌入式軟件需求描述.CNL還可以實(shí)現(xiàn)需求的自動(dòng)化驗(yàn)證,以及對(duì)需求的不一致性和不完整性進(jìn)行檢測(cè)[32].

挪威Simula實(shí)驗(yàn)室的Yue Tao教授提出了一種改進(jìn)的受限用例建模方法RUCM(Restricted Use Case Modeling)[14-16],RUCM包含一個(gè)相對(duì)完善的用例文本說明模板和一系列自然語言限定規(guī)則(Restricted Rules),使得用例描述更加易于理解和精確,減少歧義,并且可以自動(dòng)化產(chǎn)生分析模型.目前,已有相應(yīng)的研究方法和工具支持將RUCM的用例模型自動(dòng)轉(zhuǎn)換為初步的UML分析模型(類圖、活動(dòng)圖、順序圖等).此外,針對(duì)RUCM較難描述機(jī)載嵌入式軟件的安全性需求的不足,北航的吳際等人對(duì)RUCM進(jìn)行了擴(kuò)展,添加相應(yīng)的模板與限定規(guī)則,提出Safety RUCM,使其支持安全性需求的規(guī)范化描述[33].另外,面向?qū)ο蠊芾斫M織OMG (Object Management Group)在正在制定的SysML 2.0版本[18]中也提出了限定自然語言需求建模的思想,旨在提高需求描述的精確性和有效性.

6.2 自然語言需求到設(shè)計(jì)模型的自動(dòng)轉(zhuǎn)換

如何將基于自由文本、受限的自然語言或半形式化的設(shè)計(jì)模型轉(zhuǎn)換到形式化模型是一個(gè)熱點(diǎn)問題.

英國曼徹斯特大學(xué)Keletso J.Letsholop[12]等為了實(shí)現(xiàn)自由文本需求到設(shè)計(jì)模型的自動(dòng)化轉(zhuǎn)換,提出了TRAM(Tool for Transforming Textual Requirements into Analysis Models)工具,實(shí)現(xiàn)了從自由文本描述的需求到設(shè)計(jì)模型的自動(dòng)化轉(zhuǎn)換.在轉(zhuǎn)換過程中,采用了Stanford分詞器將自然語言文本進(jìn)行切分,并通過SOM(Semantic Object Models)構(gòu)造器建立中間SOMi模型,模型生成器(Model Generator)將SOMi模型通過模板匹配的方式映射到目標(biāo)模型,最后通過模型驗(yàn)證器(Model Validator)對(duì)生成的設(shè)計(jì)模型進(jìn)行分析驗(yàn)證并反饋給領(lǐng)域?qū)＜?然后進(jìn)行下一輪需求迭代.

意大利Insubria大學(xué)的Pietro Colombo 和Ferhat Khendek[34]等針對(duì)需求與設(shè)計(jì)之間存在鴻溝的問題提出了一種從需求文檔自動(dòng)抽取生成早期設(shè)計(jì)模型的方法,該方法是以通過抽取經(jīng)分析后產(chǎn)生的問題表(Problem Frames)中的信息,采用ATL(ATLAS Transformation Language)模型轉(zhuǎn)換語言制定轉(zhuǎn)換規(guī)則,分四個(gè)步驟分別抽取Blackboard和Knowledge Source信息并不斷精化,最后生成SysML模塊定義圖、活動(dòng)圖等設(shè)計(jì)模型.

代爾夫特理工大學(xué)的Van der Gaag等[35]提出了一種將SysML轉(zhuǎn)換到SLIM的方法SSTM(SysML to SLIM Transformation Methodology),支持SysML模型到SLIM模型的自動(dòng)化轉(zhuǎn)換,使得缺乏軟件工程相關(guān)知識(shí)的系統(tǒng)工程師可以直接進(jìn)行SysML系統(tǒng)建模,通過自動(dòng)轉(zhuǎn)換后使用COMPASS工具集直接分析系統(tǒng)的動(dòng)態(tài)功能行為并發(fā)現(xiàn)開發(fā)過程中可能出現(xiàn)的約束和錯(cuò)誤,有助于減少系統(tǒng)開發(fā)的時(shí)間和成本.

6.3 基于契約的組合驗(yàn)證

契約理論最早是由Reussner 等[36]首次引入到基于構(gòu)件的軟件設(shè)計(jì)與開發(fā)過程中的,通過將契約從傳統(tǒng)C/S 架構(gòu)的設(shè)計(jì)方法推廣到基于組合理論的組合契約,從而使其在組合設(shè)計(jì)與開發(fā)過程中得到應(yīng)用.

Atkinson 等[37]提出了一種組合時(shí)動(dòng)態(tài)契約檢查方法.通過設(shè)計(jì)一種Built-in Test 構(gòu)件,實(shí)現(xiàn)了測(cè)試任務(wù)的內(nèi)建.該方法主要包括兩個(gè)部分,Tester構(gòu)件和Testing構(gòu)件,其中Tester 構(gòu)件負(fù)責(zé)測(cè)試構(gòu)件是否實(shí)現(xiàn)了其外部行為特性,Testing 構(gòu)件負(fù)責(zé)測(cè)試外部環(huán)境提供的服務(wù)是否滿足構(gòu)件的需求,通過在軟件中植入檢測(cè)構(gòu)件,提取相關(guān)運(yùn)行時(shí)信息進(jìn)行分析,以確定構(gòu)件可組合性[38].

John D.Backes等[37]在研究使用規(guī)約模式把自然語言需求簡化成形式化規(guī)約的結(jié)構(gòu)的過程中,通過增加需求規(guī)約語言RSL(Requirements Specification Language)模式和calendar automata的方式,支持實(shí)時(shí)系統(tǒng)的分析并證明了AGREE中隱藏的性質(zhì):所有子組件的契約滿足,保證系統(tǒng)的契約滿足.

7 結(jié)束語

本文提出了一種基于限定自然語言的需求規(guī)約方法RNLreq,通過結(jié)構(gòu)化的數(shù)據(jù)字典、領(lǐng)域詞庫、需求模板及限定句式,約束需求的描述方式以減少其二義性;其次給出了RNLreq到AADL模型的自動(dòng)轉(zhuǎn)換,包括RNLreq到中間模型RAInterM及RAInterM到AADL的轉(zhuǎn)換規(guī)則,簡化了限定自然語言需求到AADL模型的自動(dòng)轉(zhuǎn)換;此外,提出了AADL模型組合驗(yàn)證性質(zhì)描述模板,并自動(dòng)生成AADL的組合驗(yàn)證附件AGREE Annex,以支持對(duì) AADL模型進(jìn)行組合驗(yàn)證;最后,在AADL開源建模環(huán)境OSATE實(shí)現(xiàn)了原型工具,并基于實(shí)際工業(yè)案例GNC系統(tǒng)進(jìn)行了案例分析.

在未來的工作中,在需求建模方面,將進(jìn)一步考慮對(duì)限定自然語言需求RNLreq的擴(kuò)展,增強(qiáng)RNLreq對(duì)安全性、可靠性、實(shí)時(shí)性等非功能屬性的表達(dá)能力;在模型驗(yàn)證方面,將研究從限定自然語言需求模型中自動(dòng)生成驗(yàn)證性質(zhì),包括線性時(shí)序邏輯公式和分支時(shí)序邏輯公式,形成完整的模型驗(yàn)證方法.