基于有限謂詞追蹤的民機系統(tǒng)需求一致性檢查方法

王 鵬, 岳舒婷, 張 帆,*, 董 磊

(1. 中國民航大學(xué)民航航空器適航審定技術(shù)重點實驗室, 天津 300300;2. 中國民航大學(xué)安全科學(xué)與工程學(xué)院, 天津 300300)

0 引 言

隨著整機設(shè)計要求的不斷提升與相關(guān)技術(shù)的發(fā)展,以平視顯示(head-up display, HUD)系統(tǒng)為代表涉及多領(lǐng)域的高復(fù)雜性安全關(guān)鍵系統(tǒng),呈現(xiàn)綜合集成度高、研發(fā)周期長、管理復(fù)雜等特點[1]。為保證安全關(guān)鍵系統(tǒng)基于需求的正向研發(fā)水平,在設(shè)計早期確認(rèn)功能需求的正確性具有重要意義。在國產(chǎn)安全關(guān)鍵系統(tǒng)研發(fā)工程中,系統(tǒng)功能需求確認(rèn)主要通過人工評審來實現(xiàn),效率低且難以排除需求文檔中所有沖突與不一致,無法滿足機載系統(tǒng)功能需求的嚴(yán)格確認(rèn)要求[2-3]。同時,此類安全關(guān)鍵系統(tǒng)通常由多部門、多專業(yè)協(xié)同研發(fā),而不同的開發(fā)人員、設(shè)計階段使得整體項目的需求細(xì)節(jié)無法被全面、準(zhǔn)確地理解[4],從而導(dǎo)致需求沖突與不一致的問題通常在系統(tǒng)設(shè)計后期的集成測試階段涌現(xiàn),而引入錯誤和發(fā)現(xiàn)錯誤之間的間隔越長,會造成系統(tǒng)研發(fā)迭代成本越高[5-6]。解決上述問題,亟需研究形式化的需求一致性檢查方法,以嚴(yán)格的數(shù)學(xué)邏輯進行規(guī)約,在系統(tǒng)研發(fā)初期能夠捕獲需求沖突與需求不一致,從而迅速進行需求迭代,在降低系統(tǒng)設(shè)計返工或性能不足風(fēng)險的同時減少系統(tǒng)研發(fā)成本。

采用形式化方法開展需求一致性檢查,主要包含兩部分內(nèi)容:需求形式化規(guī)約與需求沖突檢測。近年來,已有多位學(xué)者開展相關(guān)研究,研究成果涉及系統(tǒng)需求形式化規(guī)范、軟件需求沖突檢查等領(lǐng)域。

在早期的需求形式化規(guī)約研究中,文獻[7]開發(fā)了簡單需求語法模板(easy approach to requirement syntax, EARS),包括5類模板規(guī)范自然語言需求。隨后多項研究基于架構(gòu)模型建立需求規(guī)約,包括系統(tǒng)建模語言(system modeling language, SysML)[8-9]的建模語言提供了易于理解、使用的圖形語法,但缺乏正式的語義。基于描述邏輯的Web本體語言[10]為需求語言提供精確的語義,文獻[11-12]開發(fā)了多種本體構(gòu)建方法以及工程設(shè)計領(lǐng)域需求的本體,但其表達(dá)性具有一定局限。文獻[13]基于一階邏輯(first-order logic, FOL)謂詞的形式化規(guī)約則通過增加謂詞、量詞等進一步分析語句成分,成為更具表達(dá)力的基于邏輯的語言。文獻[14]提出了直觀表示FOL的顯式方法,利用此方法構(gòu)造了智能計算機輔助診斷/計算機輔助制造系統(tǒng)邏輯架構(gòu)。由于FOL表達(dá)能力廣泛,對特定復(fù)雜領(lǐng)域知識的描述需要對其進行一定的約束或擴展,使其適用于特定的形式化規(guī)約。文獻[15]提出了基于派生特征約束FOL的特定領(lǐng)域語言形式化規(guī)約方法。文獻[16]結(jié)合Petri網(wǎng)使用FOL對智能制造系統(tǒng)進行形式化建模,并推導(dǎo)出用于表示工藝方案的有限一階謂詞。

基于上述需求形式化規(guī)約的研究,需求沖突檢測技術(shù)相應(yīng)發(fā)展。基于EARS的EARS-CTRL (control)工具[17]可進行需求沖突檢查,但檢查效率較低且只針對簡單類型的沖突。SysML、架構(gòu)描述語言[18-19]多用于需求沖突檢測,但缺乏形式語義。文獻[20]提出了將邏輯嵌入SysML并將驗證問題轉(zhuǎn)化為邏輯問題的方法。文獻[21]使用FOL構(gòu)建需求模型,并進行跟蹤關(guān)系的語義一致性檢驗,但其范圍僅限于確認(rèn)通用需求關(guān)系一致性,并未針對特定對象檢查內(nèi)容一致性,因此,后續(xù)研究更多針對需求內(nèi)容進行推理規(guī)則的處理。文獻[22]提出了一種基于獨立FOL規(guī)則的方法,檢測領(lǐng)域工程過程中的不一致特征,以提高軟件產(chǎn)品的質(zhì)量。文獻[23-24]基于FOL的規(guī)范表示和一致性推理進行自動化合規(guī)性檢查,但其推理規(guī)則較為復(fù)雜。文獻[25]利用擴展謂詞邏輯進行形式化規(guī)約并推導(dǎo)出用于驗證的語義、語法和推理規(guī)則的定理。文獻[26]利用基于有限謂詞規(guī)則的軟件特征模型分析其模型中的不一致性,但并未針對軟件需求進行一致性分析。

對以上研究工作進行總結(jié),上述方法存在以下兩點問題:① 在需求形式化規(guī)約方面,未形成緊密貼合民機系統(tǒng)研發(fā)流程的系統(tǒng)級功能需求形式化規(guī)約方案,導(dǎo)致形式化方法和實際系統(tǒng)研發(fā)有一定偏差;② 在需求沖突方面,結(jié)合需求內(nèi)容正確性、關(guān)系一致性的沖突檢測技術(shù)在民機系統(tǒng)級需求領(lǐng)域尚無應(yīng)用。

針對上述問題,提出基于有限謂詞追蹤的系統(tǒng)功能需求一致性檢查方法體系,開展包含屬性分配、變量分配的系統(tǒng)級功能需求形式化規(guī)約分析,在此基礎(chǔ)上運用定理證明器ACL2(a computational logic for application common lisp)[27]實現(xiàn)需求自沖突、集沖突與需求關(guān)系一致性檢查,基于可解釋的檢查反例進行需求迭代。最后通過實例分析,驗證該方法的合理性與適用性。

1 基于有限謂詞追蹤的需求一致性檢查結(jié)構(gòu)框架

1.1 基于有限謂詞追蹤的需求一致性檢查方法概述

文獻[28]中需求確認(rèn)為確定產(chǎn)品需求的正確性與完整性。一致性為已確定的相對于標(biāo)準(zhǔn)、技術(shù)規(guī)范或圖紙的(產(chǎn)品)正確性,屬于正確性檢查的重要組成部分。功能需求指在具體條件下為了獲得系統(tǒng)預(yù)期性能所需的需求,是系統(tǒng)功能架構(gòu)研制的基礎(chǔ)[29],包括系統(tǒng)級功能自頂向下的功能需求分配,并針對系統(tǒng)級、子系統(tǒng)級進行確認(rèn),以此支持系統(tǒng)功能需求的更新與迭代,過程如圖1所示。

圖1 基于4754A的需求分配及其確認(rèn)流程圖Fig.1 Requirement allocation and verification flow based on 4754A

系統(tǒng)自頂向下的功能需求分配基于系統(tǒng)實現(xiàn),其系統(tǒng)過程與子系統(tǒng)過程之間的信息流形成系統(tǒng)功能需求,以此向下分配至:① 子系統(tǒng)設(shè)計階段,形成內(nèi)部功能需求;② 子系統(tǒng)綜合階段,形成交互功能需求。系統(tǒng)需求的規(guī)范化描述為需求規(guī)約,針對目前未形成緊密貼合民機系統(tǒng)研發(fā)流程的系統(tǒng)級功能需求形式化規(guī)約方案的問題,結(jié)合上述分配過程提出基于變量分配、屬性分配的形式化需求及其分配規(guī)約,共同輸入至系統(tǒng)級功能需求文檔。

系統(tǒng)級功能需求一致性檢查過程基于4754A中建議的正確性檢查指南,從3個檢查緯度評估需求的正確性,包括:① 需求包含事實的錯誤嗎?——需求自沖突檢查;② 需求與其他需求沖突嗎?——需求集沖突檢查;③ 需求追蹤具有一致性嗎?——需求關(guān)系一致性檢查。由于目前在需求沖突方面,結(jié)合需求內(nèi)容正確性、關(guān)系一致性的沖突檢測技術(shù)在民機系統(tǒng)級需求領(lǐng)域尚無應(yīng)用,提出系統(tǒng)單條需求的自沖突、多條需求的集沖突以及需求關(guān)系一致性的檢查方法,建立基于有限謂詞追蹤的系統(tǒng)功能需求一致性檢查體系,總體框架如圖2所示。

圖2 基于有限謂詞追蹤的需求一致性檢查方法Fig.2 Requirement consistency checking method based on finite predicate tracing

(1) 需求形式化規(guī)約

傳統(tǒng)的需求文檔為基于工程經(jīng)驗、利益攸關(guān)者意愿、運行限制、規(guī)章約束以及設(shè)計實現(xiàn)等編寫的自然語言文本,易于表達(dá)但缺乏精準(zhǔn),因此結(jié)合圖1系統(tǒng)研發(fā)流程將功能需求分為內(nèi)部功能需求與交互功能需求。將上述兩類功能需求進一步細(xì)分,提出功能需求形式化分配方法:① 完成頂層期望功能的需求——完全/部分屬性分配,例如,HUD系統(tǒng)具備姿態(tài)信息顯示功能;② 完成設(shè)計實現(xiàn)所需功能的需求——監(jiān)控/受控變量分配,例如,如果機體俯仰角大于35°,則HUD系統(tǒng)進入異常姿態(tài)模式。采用形式化規(guī)約描述需求以進行自動化定理證明或推理,從而檢查需求沖突或不一致。

(2) 需求一致性檢查

① 單條需求檢查:單條需求沖突常為數(shù)值、范圍、語義等類型沖突。因此,基于形式化需求提取可變類型及其變量,采用自沖突屬性進行單條需求內(nèi)容確認(rèn)。② 多條需求內(nèi)容檢查:多條需求沖突常存在于擁有相同可變類型及變量的多個需求之間。因此,基于形式化需求提取涉及同一變量的所有需求,采用集沖突屬性進行多條需求內(nèi)容確認(rèn)。③ 多條需求關(guān)系一致性檢查:系統(tǒng)需求間的不一致關(guān)系常存在于系統(tǒng)向下分配需求時多個分配關(guān)系的矛盾。因此,基于形式化需求分配鏈提取需求關(guān)系并映射至屬性關(guān)系,采用一致性推理公理進行需求關(guān)系一致性檢查。

1.2 基本概念定義

需求、屬性和變量是系統(tǒng)需求規(guī)約的3個基本概念:需求是功能規(guī)范的可識別要素;屬性是描述系統(tǒng)擁有的靜態(tài)特性;變量是系統(tǒng)輸入/輸出的事件和數(shù)據(jù)。后續(xù)使用FOL將需求及需求關(guān)系形式化為精準(zhǔn)語義描述,其遵循以下基本定義。

定義 1需求R。需求R定義為一個元組〈P,S〉,其中P為包含兩個參數(shù)的屬性,P可以用由謂詞組成的合取范式(conjunctive normal form, CNF)表示如下:

定義 2屬性P。屬性P是由條件與結(jié)論組成的陳述句。其中,條件為系統(tǒng)展現(xiàn)出規(guī)定特性的假設(shè);結(jié)論為陳述系統(tǒng)在假設(shè)成立時真實存在的特征。

定義 3監(jiān)控變量C。屬性P的條件中使用的變量是系統(tǒng)輸入的事件和數(shù)據(jù)。

定義 4受控變量H。屬性P滿足C條件下的結(jié)論中設(shè)置的變量,是系統(tǒng)輸出的事件和數(shù)據(jù)。

例如,R1:如果動機轉(zhuǎn)速百分比小于30%(條件),那么系統(tǒng)應(yīng)將通道Px設(shè)置為開啟(結(jié)論)。

此條功能需求語句中,條件中的“轉(zhuǎn)速百分比”為監(jiān)控變量,結(jié)論中的“通道Px”為受控變量。

將屬性P定義為一個元組〈C,H〉,即?h∈H:C(h)。根據(jù)FOL的語義模型理論,將C形式化表達(dá)為

需求自沖突、集沖突、關(guān)系不一致是系統(tǒng)需求檢查的基本概念。

定義 5需求沖突。如果需求R1的實現(xiàn)排除了需求R2的實現(xiàn),那么需求R1和需求R2就會沖突,反之亦然。

定義 6需求自沖突。如果監(jiān)控變量的某個輸入值不能滿足需求,即使存在受控變量滿足,該需求為自沖突。

定義 7需求集沖突。任一受控變量的輸入值,都有一個或幾個監(jiān)控變量的輸入值不能滿足需求集,則該需求為集沖突。

定義 8需求關(guān)系不一致。指需求之間某些關(guān)系的共存導(dǎo)致了已定義語義上下文中的矛盾。

定義 9ACL2邏輯。ACL2邏輯中用宏defun來定義函數(shù),用添加定理defthm的方法來證明系統(tǒng)的屬性。函數(shù)定義包括函數(shù)名、參數(shù)名以及函數(shù)體,示例如下:

① (defun (xy)

② (if (conspx)

③ (cons (carx) (app (cdrx)y))y))

④ (defthmtest-app (equal (app (appab)c)

(appa(appbc)))

第①行定義了“連接x和y”的函數(shù);第②行通過謂詞函數(shù)檢查參數(shù)類型;第③行以可終止的遞歸形式定義,表示如果x不為空,則復(fù)制x的第一個節(jié)點并重復(fù)到下一個節(jié)點,直到x為空則回到y(tǒng);第④行為驗證app函數(shù)的ACL定理,證明過程中,ACL2包含大量的決策制定程序和強大的簡化機制。

基于FOL精準(zhǔn)語義形式化系統(tǒng)功能需求,進行需求一致性檢查需要用到相應(yīng)的定理證明推理規(guī)范[30],因此做出如下假設(shè)。

假設(shè) 1使用規(guī)范語言L

① 多類別一階邏輯

② 可擴展

③ 可執(zhí)行

假設(shè) 2屬性P定義形式為

① 無嵌套量詞

② 隱式普遍量化

假設(shè) 3一個交互定理證明器(interactive theorem prover assistant, ITP),可以對L中的規(guī)范進行推理。

① 分解:將一個目標(biāo)(一個用L寫的公式)作為輸入,并返回一個相等有效的子目標(biāo)列表。

② 簡化:將使用語言L編寫的公式和組公式作為輸入,并返回一個與語言L編寫公式等價的簡化公式(假設(shè)組公式為真)。

2 系統(tǒng)需求形式化描述規(guī)約

2.1 系統(tǒng)內(nèi)部功能需求形式化方法

基于需求捕獲環(huán)境必須允許需求工程師在高層級需求描述中不給出低層級需求的全部細(xì)節(jié)[4],系統(tǒng)需求形式化描述規(guī)約通過謂詞追蹤完成分配。分配允許識別未完全描述的某些組件具體行為,形式上可以理解為未解釋的函數(shù)。因此,可以將頂層需求直接向下分配,不進行分配的需求也可直接形式化屬性及變量,進行需求一致性檢查。

系統(tǒng)內(nèi)部功能需求向下形式化分配包含屬性分配與變量分配兩種方式,分配過程如圖3所示。

圖3 內(nèi)部功能需求的形式化Fig.3 Formalization of internal functional requirements

2.1.1 屬性分配

(1) 屬性完全分配

設(shè)R1=〈P1,S1〉,R2=〈P2,S2〉是需求。P1和P2為由CNF組成的需求屬性,P2的CNF為

?s∈S2:s?S1

結(jié)論:如果P1對于給定的系統(tǒng)s成立,那么P2對于s也成立(?s∈S1:s∈S2)。在?s∈S2:s?S1和?s∈S1:s∈S2的基礎(chǔ)之上,即可得S1?S2。Refines關(guān)系具有非自反性、非對稱性和傳遞性。

例:需求R1向下完全分配了需求R2

P1=FMA_pattern_1(x)

P2=CMD_msg(x)

x∈{CMD,NO_CMD,SINGE_CH,和NO_SINGE_CH}

設(shè):FMA_pattern_1Mdef{CMD,NO_CMD,SINGE_CH,NO_SINGE_CH}

則CMD_msgMdef{CMD,NO_CMD}

屬性完全分配后形式化為

R2refinesR1:[CMD_msg(x)→FMA_pattern_1(x),S2?S1]

即HUD系統(tǒng)顯示飛行模式通告(FMA_pattern_1)功能向下完全分配至自動監(jiān)視儀(CMD_msg)啟動功能。

(2) 屬性部分分配

設(shè)R1=〈P1,S1〉,R2=〈P2,S2〉是需求,P1和P2為公式,P2的CNF為

例:需求R1向下部分分配了需求R2

P1=interface(x,y)

P2=datainterface(x,y,z)

式中:x是功能需求的變量;y是接口需求的變量;z是數(shù)據(jù)接口的變量;P2細(xì)化了P1接口部分,并增加了數(shù)據(jù)接口的具體內(nèi)容。因此,屬性部分分配后形式化為表示為

R2partially_refinesR1:[datainterface(x,y,z)→

interface(x,y),?s∈S1:s?S2,?s∈S2:s?S1]

即HUD系統(tǒng)符號顯示功能中的功能接口需求部分分配至數(shù)據(jù)接口,但分配后的數(shù)據(jù)接口功能并不完全服務(wù)于符號顯示功能。

2.1.2 變量分配

(1) 受控變量分配

設(shè)P1=〈C1,H1〉P2=〈C2,H2〉是需求。

該定義可得出結(jié)論H1?H2。集合H1和H2之間的子集關(guān)系將control_refines關(guān)系定義為非自反、非對稱和傳遞的,也可以稱作R2為R1的先決條件,且R1與R2不允許相等。

例:需求R1受控變量向下分配了需求R2

H1=FMA_pattern∈{CMD,NO_CMD,SINGE_CH,NO_SINGE_CH}

H2=SINGE_CH_msg

受控變量向下分配后形式化表示為

R2control_refinesR1:[C(x),H2?H1]

(2) 監(jiān)控變量分配

設(shè)R1=〈C1,H1〉,R2=〈C2,H2〉,…,Rk=〈Ck,Hk〉是需求,其中k≥2,C2,C3,…,Ck為公式,其CNF為

式中:C′表示為C2,C3,…,Ck未捕獲的需求。此定義對于分解的完整性不做假設(shè)。從定義可以得出結(jié)論,如果C1成立,那么C2…Ck也保持,如果C2…Ck成立則C1不一定成立。因此,H1?H2,H1?H3,…,H1?Hk。其中,monitor_refines關(guān)系是非自反的,非對稱的,傳遞的。

例:需求R1監(jiān)控變量向下分配了需求R2

C1=provide (FMA_FD_ONf)

監(jiān)控變量向下分配后形式化為表示為

ON_flash),H2?H1]

即HUD系統(tǒng)自動駕駛儀未接通符號閃爍顯示的條件分配為3個監(jiān)控變量。

2.2 系統(tǒng)交互功能需求形式化方法

與前述內(nèi)部需求類似,交互功能需求的形式化需要考慮多個系統(tǒng)的交互關(guān)系下屬性分配與多系統(tǒng)子集關(guān)系,形式化過程如圖4所示。

圖4 交互功能需求的形式化Fig.4 Formalization of interactive functional requirements

(1) 屬性完全分配

交互需求屬性完全分配后形式化表示為

(2) 屬性部分分配

?s∈S1-S2:s?S1-S2,?s∈(S1-S2∩S1-S2)

P2=datainterface(x,y,z)

R2partially_refinesR1:[datainterface(x,y,z)→

(3) 變量分配

交互功能需求的變量分配與內(nèi)部功能需求相同,即:

3 基于有限謂詞追蹤的一致性檢查

3.1 系統(tǒng)功能需求自沖突檢查

本文通過提取關(guān)鍵沖突屬性并采用ACL2定理證明器對需求一致性進行驗證。基于第2節(jié)系統(tǒng)功能需求形式化描述規(guī)約,由需求自沖突的定義可得自沖突的檢查形式[31]為

(1)

式中:c1,c2,…,cn為需求的n個監(jiān)控變量(monitor_variable);T1,T2,…,Tn為監(jiān)控變量的n個類型(monitor_type);h1,h2,…,hk為需求的k個受控變量(control_variable);Z1,Z2,…,Zk為受控變量的k個類型(control_type);fr為需求主體。

式(1)表明,對于監(jiān)控變量的任何可行賦值(監(jiān)控變量的類型對應(yīng)其可行值),受控變量至少有一個可行賦值,使得需求R成立。基于式(1)的檢查形式構(gòu)建顯示自沖突的確認(rèn):

(2)

式(2)則表明需求自沖突的類型,如果提取變量及其可行值與自沖突類型相同,則需求R顯示為自沖突,即存在監(jiān)控變量的可行賦值不滿足需求R。因此,自沖突檢查過程如圖5所示。

圖5 需求自沖突檢查Fig.5 Requirements self-conflict checking

待檢查的單條形式化需求Ri作為輸入,提取屬性以及變量進行沖突識別,判斷其是否屬于需求自沖突類型,若屬于自沖突類型則檢查結(jié)果為需求自沖突,并輸出反例;否則進入下一條需求的檢查。其中,自沖突類型:① 存在監(jiān)控變量及其可行值,但不存在相應(yīng)受控變量;② 存在監(jiān)控變量及其可行值、相應(yīng)受控變量,但該受控變量不存在可行值;③ 存在監(jiān)控變量但不存在該監(jiān)控變量可行值。

例,R1:如果機體俯仰角超過35°,則HUD系統(tǒng)進入異常姿態(tài)模式;R2:姿態(tài)數(shù)據(jù)傳感器可識別角度范圍[-30,33]。此案例中的自沖突類型為第③種,即R1監(jiān)控變量的賦值大于33時無可行賦值,R1發(fā)生自沖突。

自沖突屬性系統(tǒng)功能需求檢查為自沖突,ACL2實現(xiàn)策略如下:

DEFUN self-conflict

(AND (?monitor_variable∈monitor_type)

(eqlfr(Monitor_variable, control_variable)T))

#監(jiān)控變量存在可行賦值且輸出受控變量與監(jiān)控變量的關(guān)系

DEFTHM self-conflict-test

(OR (?control_variable∈control_type)

(eqlfr(Monitor_variable, control_variable)T))

#受控變量存在可行賦值

3.2 系統(tǒng)功能需求集沖突檢查

根據(jù)需求集沖突的定義,將式(1)與式(2)中的R替換為需求R的集合,作為集沖突的檢查形式,集沖突的檢查過程如圖6所示。

由于多數(shù)存在集沖突的需求集往往共享一個受控變量,因此待檢查的多條形式化需求Ri作為輸入,需要提取相關(guān)屬性及其相同受控變量進行沖突識別,判斷其是否屬于需求集沖突類型,若屬于集沖突類型則檢查結(jié)果為需求集沖突,并輸出反例;否則進入下一條需求的檢查。其中,集沖突類型:① 存在一個監(jiān)控變量及其可行值對應(yīng)多個監(jiān)控變量及可行值;② 存在多個監(jiān)控變量及其可行值同時成立時無相應(yīng)受控變量及可行值。

例,R1:如果TO/GA狀態(tài)數(shù)據(jù)指令開啟,則自動油門模式通告顯示為“GA”;R2:如果自動油門模式N1數(shù)據(jù)指令開啟時,則自動油門模式通告顯示為“N1”。此案例中的沖突類型為第②種,即如果TO/GA狀態(tài)數(shù)據(jù)指令開啟且自動油門模式N1數(shù)據(jù)指令開啟兩個條件同時成立時,受控變量——“自動油門模式通告”不存在可行賦值,即兩個需求發(fā)生集沖突。

集沖突屬性系統(tǒng)功能需求檢查為集沖突,ACL2實現(xiàn)策略如下:

DEFUN set-conflict

(COND (c1∈T1(AND (eqlfr(c1,h1)T)h1∈Z1))

(c2∈T2(AND (eqlfr(c2,h2)T)h2∈Z2))

?

(cn∈Tn(AND (eqlfr(cn,hk)T)hk∈Zk)))

#如果c1/c2/…/cn成立則對應(yīng)輸出h1/h2/…/hk

DEFTHM set-conflict-test

(IMPLIES (AND (eqlfr(c,h)T)(?cn∈Tn))

(AND (eqlfr(c1,h)T)(eqlfr(c2,h)T)))

#監(jiān)控變量找不到可行值或多個同時滿足輸出一個受控變量。

3.3 系統(tǒng)功能需求關(guān)系一致性檢查

基于第2節(jié)需求分配關(guān)系定義,需求分配f(R1,R2)共存在4種關(guān)系:① 屬性完全分配WR;② 屬性部分分配PR;③ 監(jiān)控變量分配MR;④ 受控變量分配CR。需求關(guān)系的一致性通過將需求關(guān)系進一步細(xì)分為屬性關(guān)系g(P1,P2)進行檢查,根據(jù)文獻[21]給定的需求屬性,存在的5種關(guān)系分別為:① 整體-整體——all-in-whole(P1,P2);② 整體-局部——all-in-part(P1,P2);③ 局部蘊含——some-implies-in(P1,P2);④ 整體蘊含——all-implies-in(P1,P2);⑤ 全等——all-equals-in(P1,P2),基于以上5種關(guān)系分別定義需求的屬性分配與變量分配關(guān)系:

具體映射如下:

對于上述公式之間的關(guān)系,具有以下一致性公理,如果推導(dǎo)出的新關(guān)系包含以下矛盾關(guān)系,則被判定為不一致。具體檢查過程如圖7所示。

圖7 需求一致性檢查Fig.7 Requirement consistency checking

(1) 全等與蘊含矛盾

例:all-equals-in∩all-implies-in=?

(2) 整體與局部矛盾

例:all-in-whole∩all-in-part=?

需求R進行屬性/變量分配過程得到分配后的需求R′,即將R與R′之間的關(guān)系fn(R1,R2)作為輸入,存在多種關(guān)系的兩條需求,使其需求關(guān)系映射至屬性關(guān)系gn(P1,P2),判斷細(xì)化后的屬性關(guān)系是否存在矛盾關(guān)系,如果存在則判定為不一致關(guān)系;否則進入下一對需求關(guān)系檢查。

例:①R1可以通過屬性完全分配得到R2;②R1可以通過受控變量分配得到R2。此案例中的不一致類型為第①種,即兩個需求的屬性關(guān)系all-equals-in, some-implies-in矛盾即R1與R2存在不一致。

關(guān)系沖突屬性系統(tǒng)功能需求關(guān)系檢查為不一致,ACL2實現(xiàn)策略如下:

DEFUN consistency

(COND (ralation1(P1,P2)(OR{00}{11}{01}{10}))

(ralation2(P1,P2)(OR{00}{11}{01}{10}))

?

(ralation5(P1,P2)(OR{00}{11}{01}{10})))

#如果ralation1/…/ralation5成立則輸出對應(yīng)的{00}/{11}/{01}/{10}

DEFTHM consistency-test

(IF (output(consistency)∈(OR{0011}{1100}{0110}{1001}))′(non-consistency)′(consistency))

#如果給定的兩需求關(guān)系代碼組合屬于不一致組合,則該兩需求關(guān)系之間存在不一致。

4 實例分析

4.1 HUD系統(tǒng)飛行信息符號生成與顯示功能概述

HUD系統(tǒng)能夠?qū)C上傳感器信息處理計算后,利用光學(xué)反射和成像設(shè)備將必要飛行狀態(tài)信息,以及提示、告警、故障等方式投射至飛行員前方的成像板上,實現(xiàn)飛行關(guān)鍵信息符號生成與顯示[32]。HUD系統(tǒng)的基本架構(gòu)由HUD計算機(HUD computer, HUDC)、HUD投影裝置(HUD projector unit, HPU)、HUD組合儀(HUD combiner unit, HCU)組成。以典型功能“飛行信息符號生成與顯示”為例,系統(tǒng)功能架構(gòu)如圖8所示。 HUDC接收并解析機載傳感器數(shù)據(jù),將其轉(zhuǎn)換為內(nèi)部應(yīng)用程序編程接口;符號生成軟件根據(jù)傳感器數(shù)據(jù)計算符號邏輯,生成繪制指令。HUDC根據(jù)繪制指令生成飛行信息符號畫面發(fā)送給HPU,HPU對顯示畫面進行畸變校正,并經(jīng)過光學(xué)結(jié)構(gòu)進行投影。HCU接收投射的顯示畫面并顯示規(guī)定的符號信息。

圖8 HUD系統(tǒng)飛行信息符號生成與顯示功能架構(gòu)Fig.8 HUD system flight information symbol generation and display function architecture

4.2 基于形式化規(guī)約的系統(tǒng)功能需求描述

4.2.1 功能需求分類

飛行信息符號生成與顯示功能需求(部分)分類如表1所示。

表1 “飛行信息符號生成與顯示”功能需求(部分)Table 1 Functional requirements of “flight information symbol generation and display” (partial)

4.2.2 功能需求形式化描述

基于第2節(jié)形式化需求分配,HUD系統(tǒng)內(nèi)部、交互功能需求的分配關(guān)系如圖9所示,其中WR為屬性完全分配,PR為屬性部分分配,CR為受控變量分配,MR為監(jiān)控變量分配。

圖9 功能需求分配關(guān)系圖Fig.9 Functional requirement allocation relationship diagram

(1) 內(nèi)部功能需求形式化

分配①:R02partially_refinesR01:[FMA(x,y)→Display(x),?s∈S01:s?S02,?s∈S02:s?S01]

∥R02部分細(xì)化了R01的飛行模式通告具體內(nèi)容。

分配②:R03refinesR02:[FDM(y)→ FMA(x),S03?S02]

∥R03在R02原有內(nèi)容的基礎(chǔ)上細(xì)化了飛行指引儀模式通告信息具體內(nèi)容。

分配③:R04control_refinesR03:[AFM(x),H04?H03]

∥R04細(xì)化了R03結(jié)論中自動飛行模式通告改變時系統(tǒng)模式的改變。

分配④:R07partially_refinesR04:[MODE_Change _body→AFM-MODE(x),?s∈S04:s?S07,?s∈S07:s?S04]

∥R07部分細(xì)化了R04兩個模式之間的關(guān)系。

分配⑤:R05monitor_refinesR04:[C04=C05∧C′,H05?H04]

∥R05細(xì)化了R04條件中自動飛行模式通告符號信息可顯示的3個模式通告。

分配⑥:R06control_refinesR04:[AFM(x),H06?H04]

∥R06細(xì)化了R04結(jié)論中兩個模式的類型。

(2) 交互功能需求形式化

∥R09細(xì)化了R08中符號定義的具體管理內(nèi)容

R10control_refinesR09:[Defined(x),H10?H09]

∥R10細(xì)化了R09結(jié)論中符號定義的條件。

∥R14、R15、R16細(xì)化了R13條件中的受控變量及其可行值,以及相應(yīng)的結(jié)論。

4.3 需求一致性檢查

(1) 需求自沖突檢查

自沖突適用于單條需求的類型檢查、賦值檢查以及范圍檢查,以R06和R07作為典型案例,使用ACL2定理證明器開展系統(tǒng)自沖突檢查。

基于自沖突屬性進行HUD功能需求自沖突檢查,ACL2實現(xiàn)如下:

DEFUN self-conflict1 (xy)

(declare (type integerxy))

(if (AND (INTEGERPx)

(<=1x)(<=x5)

(INTEGERPy)

(<=1y)(<=y5))

(+x1) 0)

DEFTHM self-conflict-test

(and (INTEGERP (self-conflict1xy))

(<=0 (self-conflict1xy))

(<=(self-conflict1xy) 5))

上述代碼首先定義monitor_variable存在的可行賦值,并構(gòu)建control_variable與monitor_variable在屬性中的映射關(guān)系,通過ACL2定理證明器,驗證該control_variable不存在滿足需求的可行賦值,檢查結(jié)果為自沖突。代碼中第二行要對需求變量的可行值類型進行約束,且需要給出監(jiān)控變量及其賦值的可行范圍,證明過程如下:

Cgen/test

圖10 自沖突檢查結(jié)果及反例Fig.10 Self-conflict examination results and counterexamples

因此,檢查結(jié)果表明R07存在自沖突,即如果自動飛行系統(tǒng)模式通告FMA_FD閃爍顯示,那么DesiredMODE應(yīng)該根據(jù)CurrentMODE設(shè)置為CurrentMODE+1的值,此時CurrentMODE為監(jiān)控變量,DesiredMODE為受控變量。但是CurrentMODE和DesiredMODE是相同的類型,是[1,5]范圍內(nèi)的整數(shù),如果CurrentMODE=5,那么就沒有辦法為受控變量DesiredMODE賦值以滿足需求,所以存在需求自沖突。

(2) 需求集沖突檢查

集沖突適用于具有相同受控變量的需求集,以R15和R16作為典型案例,使用ACL2定理證明器開展HUD系統(tǒng)功能需求集沖突檢查。

基于集沖突屬性進行HUD功能需求集沖突檢查,ACL2實現(xiàn)如下:

DEFUN set-conflict1(coma comb)

(declare (type integer coma comb))

(if (>=(-coma comb) 5) 1 0)

DEFUN set-conflict2(coma comb)

(declare (type integer coma comb))

(if (<=(-coma comb) 5) 0 1)

DEFTHM set-conflict-test

(=((-(set-conflict coma comb) (set-conflict coma comb))0)

上述代碼表示根據(jù)需求屬性定義當(dāng)monitor_variable存在可行值T1時,可使對應(yīng)的control_variable成立且輸出可行值Z1,或?qū)?c1,h1)的映射關(guān)系傳遞至(cn,hk)成立,及其對應(yīng)輸出可行賦值(Tn,Zk);驗證monitor_variable找不到可行值,或多個monitor_variable同時滿足輸出一個control_variable,則檢查結(jié)果為集沖突。代碼中第7行用到的函數(shù)必須存在多個需求使用同一受控變量及其可行值的條件限制,證明過程如下:

#將字符串與正則表達(dá)式進行匹配,正則表達(dá)式在宏擴展時進行分析。

#獲取和設(shè)置Cgen中各種參數(shù)的默認(rèn)值

#存儲簡化的定義主體

#簡化規(guī)則

Cgen/test

若存在反例,則ACL2輸出如圖11(a)所示,反例給出需求顯示自沖突時監(jiān)控變量賦值為5時受控變量存在兩相異可行值,即集沖突類型①如圖11(b)所示。

圖11 集沖突檢查結(jié)果及反例Fig.11 Set-conflict examination results and counterexamples

因此,檢查結(jié)果表示R15和R16存在集沖突,即|id_ComA-id_ComB|需要嚴(yán)格大于5還是大于或等于5存在沖突。ACL2給出的反例捕獲了兩個數(shù)據(jù)的差值正好為5的系統(tǒng)狀態(tài),在這種情況下,兩個需求都適用,并將FMA_pattern置為不同的值,所以存在需求集沖突。

(3) 需求關(guān)系一致性檢查

一致性沖突適用于分配過程的關(guān)系一致性,以R09和R10作為典型案例,使用ACL2定理證明器開展HUD系統(tǒng)功能需求關(guān)系一致性檢查。

基于關(guān)系沖突屬性進行HUD功能需求關(guān)系一致性檢查,ACL2實現(xiàn)如下:

DEFUN refines (all-in-whole some-implies-in)

(declare (type integer all-in-whole some-implies-in))

(cond((=all-in-whole some-implies-in)(print′(0 0)))

((

(endp))

DEFUN control-refines (all-in-part all-equals-in)

(declare (type integer all-in-part all-equals-in))

(cond((

((=all-in-part (fx all-in-part)) (print′(1 0)))

(endp))

DEFUN consistency-check (xy)

(declare (type integerxy))

(cond((or (=(concatenate′list′(refinesxy)′(control-refinesxy))′(0 0 1 0))

(=(concatenate′list′(refinesxy)′(control-refinesxy))′(0 1 1 1)))x)

((or (=(concatenate′list′(refinesxy)′(control-refinesxy))′(0 0 1 1))

(=(concatenate′list′(refinesxy)′(control-refinesxy))′(0 1 1 0)))y)(x))

DEFTHM consistency-test

(equal (consistency-checkxy)

(consistency-checkyy))

上述代碼表示根據(jù)屬性之間的關(guān)系對應(yīng)輸出集合{00}/{11}/{01}/{10},再將需求之間的關(guān)系以屬性關(guān)系的對應(yīng)數(shù)組按順序相連,形成相應(yīng)的需求關(guān)系代碼組合屬于規(guī)定的不一致組合{0011}{1100}{0110}{1001},則檢查結(jié)果為需求關(guān)系不一致。代碼中DEFTHM定義函數(shù)必須為可終止函數(shù),ACL2證明過程如下:

Cgen/test

若存在不一致則ACL2輸出如圖12(a)所示,反例給出需求關(guān)系顯示不一致時同時存在的屬性關(guān)系交集為空,即不一致類型①和②如圖12(b)所示。

圖12 一致性檢查結(jié)果及反例Fig.12 Consistency check results and counterexamples

因此,檢查結(jié)果為R10refinesR09與R10control _refinesR09關(guān)系存在不一致,ACL2給出的反例表示不存在有相應(yīng)關(guān)系的兩條需求,即WR(R10,R09)=all-in-whole(P10,P09)∧some-implies-in(P10,P09),CR(R10,R09)=all-in-part(P10,P09)∧ all-equals-in(P10,P09),整體(all-in-whole)與局部關(guān)系(all-in-part)相矛盾、全等關(guān)系(all-equals-in)與蘊含關(guān)系(some-implies-in)相矛盾。因此WR(R10,R09)和CR(R10,R09)存在不一致。

檢查結(jié)果匯總?cè)绫?所示。基于第4.2節(jié)中的形式化需求,開展HUD系統(tǒng)16條功能需求自沖突檢查、16條功能需求集沖突檢查、14種分配關(guān)系進行一致性檢查,共完成46次一致性檢查共遍歷13 026次,生成15條反例對結(jié)果進行評審,確認(rèn)結(jié)果正確,從而證明了方法的有效性。

表2 “飛行信息符號顯示與生成功能”需求一致性檢查結(jié)果Table 2 Results of “flight information symbol display and generation function” requirement consistency check

本文提出的基于有限謂詞追蹤的HUD系統(tǒng)功能需求一致性檢查方法與EARS-CTRL、根系統(tǒng)標(biāo)記語言(root system markup language, RSML)、規(guī)范工具和需求方法(specification toolsand requirements methodology, SpecTRM),統(tǒng)一建模語言(unified modeling language, UML)、 SysML、美國國防部架構(gòu)框架(Department of Defense Architecture Framework, DoDAF),TRIC/FOL的對比結(jié)果如表3所示。通過對比,本文方法主要具有以下3個方面的優(yōu)勢:① 綜合需求內(nèi)容正確性與需求關(guān)系一致性的體系化檢查方案;② 生成可解釋沖突反例,實現(xiàn)部分隱性需求顯性化,有助于安全關(guān)鍵系統(tǒng)研發(fā)需求的更新迭代;③ 基于4754A系統(tǒng)功能需求形式化分配完成邏輯事實推理,將需求沖突檢查轉(zhuǎn)化為基于一階邏輯的精準(zhǔn)語義推理,優(yōu)化以往形式化方法語義推理不足。

表3 方法對比Table 3 Methods comparison

5 結(jié) 論

本文提出基于有限謂詞追蹤的民機系統(tǒng)需求一致性檢查方法,能夠在系統(tǒng)研發(fā)初期捕獲功能需求沖突與不一致,并綜合考慮了需求內(nèi)容正確性與需求關(guān)系一致性的體系化檢查方案。① 針對系統(tǒng)功能需求包含的內(nèi)部功能需求、交互功能需求構(gòu)建基于謂詞追蹤的形式化規(guī)約,形成屬性追蹤、變量追蹤的系統(tǒng)級功能需求分配機制;② 基于需求形式化規(guī)約,在有限謂詞追蹤路徑內(nèi)定義需求沖突屬性,開展需求自沖突、集沖突的單、多條需求內(nèi)容的一致性檢查;③ 基于需求追蹤關(guān)系制定關(guān)系沖突屬性,通過ACL2完成需求關(guān)系一致性檢查。同時,檢查結(jié)果為沖突時即可生成可解釋反例實現(xiàn)隱性需求顯性化,助于需求迭代,以HUD系統(tǒng)飛行信息符號生成與顯示功能為例驗證該方法的正確性與有效性。

基于有限謂詞追蹤的民機系統(tǒng)需求一致性檢查方法是一階邏輯形式化與定理證明推理的綜合,應(yīng)用謂詞追蹤形式化需求分配過程,通過ACL2實現(xiàn)檢查策略從而識別沖突與不一致。在需求形式化規(guī)約方面,形成緊密貼合民機系統(tǒng)研發(fā)流程的系統(tǒng)級功能需求形式化規(guī)約方案,優(yōu)化形式化方法使用效果;在需求沖突方面,實現(xiàn)結(jié)合需求內(nèi)容正確性、關(guān)系一致性的沖突檢測技術(shù)在民機系統(tǒng)級需求領(lǐng)域的應(yīng)用,降低系統(tǒng)研發(fā)成本。