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

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

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

0 引 言

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

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

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

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

對以上研究工作進行總結,上述方法存在以下兩點問題:① 在需求形式化規約方面,未形成緊密貼合民機系統研發流程的系統級功能需求形式化規約方案,導致形式化方法和實際系統研發有一定偏差;② 在需求沖突方面,結合需求內容正確性、關系一致性的沖突檢測技術在民機系統級需求領域尚無應用。

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

1 基于有限謂詞追蹤的需求一致性檢查結構框架

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

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

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

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

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

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

(1) 需求形式化規約

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

(2) 需求一致性檢查

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

1.2 基本概念定義

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

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

定義 2屬性P。屬性P是由條件與結論組成的陳述句。其中,條件為系統展現出規定特性的假設;結論為陳述系統在假設成立時真實存在的特征。

定義 3監控變量C。屬性P的條件中使用的變量是系統輸入的事件和數據。

定義 4受控變量H。屬性P滿足C條件下的結論中設置的變量,是系統輸出的事件和數據。

例如,R1:如果動機轉速百分比小于30%(條件),那么系統應將通道Px設置為開啟(結論)。

此條功能需求語句中,條件中的“轉速百分比”為監控變量,結論中的“通道Px”為受控變量。

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

需求自沖突、集沖突、關系不一致是系統需求檢查的基本概念。

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

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

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

定義 8需求關系不一致。指需求之間某些關系的共存導致了已定義語義上下文中的矛盾。

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

① (defun (xy)

② (if (conspx)

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

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

(appa(appbc)))

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

基于FOL精準語義形式化系統功能需求,進行需求一致性檢查需要用到相應的定理證明推理規范[30],因此做出如下假設。

假設 1使用規范語言L

① 多類別一階邏輯

② 可擴展

③ 可執行

假設 2屬性P定義形式為

① 無嵌套量詞

② 隱式普遍量化

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

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

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

2 系統需求形式化描述規約

2.1 系統內部功能需求形式化方法

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

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

圖3 內部功能需求的形式化Fig.3 Formalization of internal functional requirements

2.1.1 屬性分配

(1) 屬性完全分配

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

?s∈S2:s?S1

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

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

P1=FMA_pattern_1(x)

P2=CMD_msg(x)

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

設: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系統顯示飛行模式通告(FMA_pattern_1)功能向下完全分配至自動監視儀(CMD_msg)啟動功能。

(2) 屬性部分分配

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

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

P1=interface(x,y)

P2=datainterface(x,y,z)

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

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

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

即HUD系統符號顯示功能中的功能接口需求部分分配至數據接口,但分配后的數據接口功能并不完全服務于符號顯示功能。

2.1.2 變量分配

(1) 受控變量分配

設P1=〈C1,H1〉P2=〈C2,H2〉是需求。

該定義可得出結論H1?H2。集合H1和H2之間的子集關系將control_refines關系定義為非自反、非對稱和傳遞的,也可以稱作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) 監控變量分配

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

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

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

C1=provide (FMA_FD_ONf)

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

ON_flash),H2?H1]

即HUD系統自動駕駛儀未接通符號閃爍顯示的條件分配為3個監控變量。

2.2 系統交互功能需求形式化方法

與前述內部需求類似,交互功能需求的形式化需要考慮多個系統的交互關系下屬性分配與多系統子集關系,形式化過程如圖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) 變量分配

交互功能需求的變量分配與內部功能需求相同,即:

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

3.1 系統功能需求自沖突檢查

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

(1)

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

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

(2)

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

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

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

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

自沖突屬性系統功能需求檢查為自沖突,ACL2實現策略如下:

DEFUN self-conflict

(AND (?monitor_variable∈monitor_type)

(eqlfr(Monitor_variable, control_variable)T))

#監控變量存在可行賦值且輸出受控變量與監控變量的關系

DEFTHM self-conflict-test

(OR (?control_variable∈control_type)

(eqlfr(Monitor_variable, control_variable)T))

#受控變量存在可行賦值

3.2 系統功能需求集沖突檢查

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

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

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

集沖突屬性系統功能需求檢查為集沖突,ACL2實現策略如下:

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成立則對應輸出h1/h2/…/hk

DEFTHM set-conflict-test

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

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

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

3.3 系統功能需求關系一致性檢查

基于第2節需求分配關系定義,需求分配f(R1,R2)共存在4種關系:① 屬性完全分配WR;② 屬性部分分配PR;③ 監控變量分配MR;④ 受控變量分配CR。需求關系的一致性通過將需求關系進一步細分為屬性關系g(P1,P2)進行檢查,根據文獻[21]給定的需求屬性,存在的5種關系分別為:① 整體-整體——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種關系分別定義需求的屬性分配與變量分配關系:

具體映射如下:

對于上述公式之間的關系,具有以下一致性公理,如果推導出的新關系包含以下矛盾關系,則被判定為不一致。具體檢查過程如圖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′之間的關系fn(R1,R2)作為輸入,存在多種關系的兩條需求,使其需求關系映射至屬性關系gn(P1,P2),判斷細化后的屬性關系是否存在矛盾關系,如果存在則判定為不一致關系;否則進入下一對需求關系檢查。

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

關系沖突屬性系統功能需求關系檢查為不一致,ACL2實現策略如下:

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成立則輸出對應的{00}/{11}/{01}/{10}

DEFTHM consistency-test

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

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

4 實例分析

4.1 HUD系統飛行信息符號生成與顯示功能概述

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

圖8 HUD系統飛行信息符號生成與顯示功能架構Fig.8 HUD system flight information symbol generation and display function architecture

4.2 基于形式化規約的系統功能需求描述

4.2.1 功能需求分類

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

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

4.2.2 功能需求形式化描述

基于第2節形式化需求分配,HUD系統內部、交互功能需求的分配關系如圖9所示,其中WR為屬性完全分配,PR為屬性部分分配,CR為受控變量分配,MR為監控變量分配。

圖9 功能需求分配關系圖Fig.9 Functional requirement allocation relationship diagram

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

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

∥R02部分細化了R01的飛行模式通告具體內容。

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

∥R03在R02原有內容的基礎上細化了飛行指引儀模式通告信息具體內容。

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

∥R04細化了R03結論中自動飛行模式通告改變時系統模式的改變。

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

∥R07部分細化了R04兩個模式之間的關系。

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

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

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

∥R06細化了R04結論中兩個模式的類型。

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

∥R09細化了R08中符號定義的具體管理內容

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

∥R10細化了R09結論中符號定義的條件。

∥R14、R15、R16細化了R13條件中的受控變量及其可行值,以及相應的結論。

4.3 需求一致性檢查

(1) 需求自沖突檢查

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

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

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存在的可行賦值,并構建control_variable與monitor_variable在屬性中的映射關系,通過ACL2定理證明器,驗證該control_variable不存在滿足需求的可行賦值,檢查結果為自沖突。代碼中第二行要對需求變量的可行值類型進行約束,且需要給出監控變量及其賦值的可行范圍,證明過程如下:

Cgen/test

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

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

(2) 需求集沖突檢查

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

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

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)

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

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

#獲取和設置Cgen中各種參數的默認值

#存儲簡化的定義主體

#簡化規則

Cgen/test

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

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

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

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

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

基于關系沖突屬性進行HUD功能需求關系一致性檢查,ACL2實現如下:

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))

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

Cgen/test

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

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

因此,檢查結果為R10refinesR09與R10control _refinesR09關系存在不一致,ACL2給出的反例表示不存在有相應關系的兩條需求,即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)與局部關系(all-in-part)相矛盾、全等關系(all-equals-in)與蘊含關系(some-implies-in)相矛盾。因此WR(R10,R09)和CR(R10,R09)存在不一致。

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

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

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

表3 方法對比Table 3 Methods comparison

5 結 論

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

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