中斷驅動型航天嵌入式軟件原子性違反檢測方法

于婷婷 李 超 王博祥 陳 睿 江云松

1（北京軒宇信息技術有限公司 北京 100190）

2（北京控制工程研究所 北京 100190）

嵌入式軟件的可信性對航天任務成敗至關重要，即使一個微小的軟件缺陷也可能導致重要任務的失敗.航天嵌入式軟件廣泛采用中斷驅動的并發機制，與硬件頻繁地進行交互并實時地響應外界事件[1].當一個系統中的大量處理都由中斷發起時，我們稱這類系統為中斷驅動型系統[2].

中斷驅動型嵌入式軟件使用大量的共享數據來實現主任務和中斷，以及不同中斷之間的通信和數據交互.如圖1 所示，航天嵌入式軟件通常由主任務和多個中斷服務程序構成.主任務的結構是一個無限循環，等待中斷的觸發進行相應的操作.中斷由來自軟件或硬件（如定時器、外設和I/O 端口）的中斷信號觸發，例如由內部事件及“異常”，或由接收字節的串行端口控制器觸發.然后，處理器通過掛起其他當前活動、保存其狀態并執行中斷處理程序來響應當前事件.待中斷處理完成后，處理器恢復其正常活動.由于中斷可能在任意時刻發生并搶占正在執行的計算，因此，如果對共享數據的訪問沒有被恰當地同步，則不確定的中斷搶占可能會導致數據訪問沖突，引起嚴重的安全問題.據中國空間技術研究院軟件產品保證中心統計[3]，在航天器總裝集成測試（assembly，integration &test，AIT）階段發現的軟件質量問題中，約80%為中斷相關的并發缺陷.這些缺陷在經過各種嚴格的軟件測試后仍然被遺漏，是航天嵌入式軟件開發中最難以消除的缺陷類型之一.根據文獻[4]對航天嵌入式軟件并發缺陷的研究，原子性違反是中斷并發缺陷中最突出的一類缺陷模式.這種模式指的是程序員對共享數據連續多次訪問的原子性執行期望由于中斷搶占而遭到破壞，導致非預期的程序行為.

Fig.1 Interrupt-driven model in aerospace embedded software圖1 航天嵌入式軟件的中斷驅動模型

原子性違反檢測是國內外研究的熱點，已有方法大多面向多線程程序[5-14]，但這些方法不能直接應用于中斷驅動型航天嵌入式軟件，這是由于中斷驅動型航天嵌入式軟件與多線程程序在并發模型和編程范式方面存在顯著差異.例如，任務與中斷之間或中斷與中斷之間具有非對稱搶占關系，而線程之間可以互相搶占，異步并發事件及其優先級之間的隱式依賴關系，使用于檢測競爭的happens-before 關系復雜化，這導致適用于2 類程序的缺陷檢測方法存在差異；中斷驅動型航天嵌入式軟件一般缺乏底層并發編程框架，經常采用基于自定義標志變量的同步方式，而多線程程序多采用標準并發控制原語，自定義標志變量的存在極易導致檢測結果存在大量誤報；此外，中斷驅動型航天嵌入式軟件依賴大量的內存映射I/O 地址與外設進行交互，若不能恰當識別這些數據，將使檢測結果存在漏報.這些差異對檢測方法的有效性具有決定性作用，直接應用針對多線程程序的檢測方法面臨檢測結果不精確的問題.

目前，僅有少量工作針對中斷驅動型程序中的原子性違反[4,15].文獻[4]采用靜態分析的方法，可擴展到工業規模的嵌入式軟件，但存在較多誤報；文獻[15]采用程序模型檢驗方法，但僅能擴展到百行規模的程序.一方面，文獻[4,15]都無法同時實現高精度和高可擴展性；另一方面，中斷驅動型航天嵌入式軟件的硬件依賴性強且多采用裸機編程，其并發缺陷的表現形式具有領域相關特征，且已有方法的有效性都未經過真實航天嵌入式軟件的評估.

本文面向真實中斷驅動型嵌入式軟件中的原子性違反，研究精確且高效的靜態檢測方法.首先對2009—2022 年中國空間技術研究院第三方評測機構報告的82 個原子性違反缺陷進行特征研究，獲得該類缺陷在訪問交錯模式、共享數據訪問方式、訪問粒度等3 方面的表現特征.在此基礎上，提出了一個精確、高效的靜態缺陷檢測方法intAtom-S.該方法的核心思想是逐階段地采用更精確的技術消除不可行路徑導致的誤報，從而同時實現更少的誤報和更好的性能.intAtom-S 主要分為3 個階段：1）基于一個由數值不變式參數化的細粒度內存訪問模型，引入基于規則的方法剔除標志變量訪問，并采用抽象解釋進行精確的共享數據分析，以識別程序中的所有可能造成缺陷的共享訪問點.該分析能夠排除標志變量訪問，將共享數據訪問粒度精確至數組元素，并可識別共享內存映射I/O 地址.2）使用輕量級數據流分析技術匹配符合交錯模式的所有并發3 次訪問序作為潛在的原子性違反缺陷候選.3）采用基于路徑條件的約束求解對缺陷候選中的串行訪問對和并發3次訪問序進行路徑可行性分析，逐步消除誤報，得到最終的原子性違反結果.

本文實現了一個面向C 程序的中斷原子性違反靜態檢測工具intAtom-S，并在基準測試集Racebench 2.1[16]和8 個真實航天嵌入式軟件上進行了實驗評估.結果表明，與當前的研究工作相比，intAtom-S 的誤報率降低了72%，同時檢測速度提高了3 倍.此外，intAtom-S 可以非常快地完成對真實航天嵌入式軟件的分析，發現了23 個經開發人員確認的錯誤，且平均誤報率僅為8.9%.本文的部分內容已發表于文獻[17]和[18],相比已發表內容，intAtom-S 基于更精確、更細粒度的共享數據識別結果，可以處理數組元素訪問、標志變量訪問導致的誤報，顯著提高了缺陷檢測的精度.

本文的主要貢獻包括3 個方面：

1）對來自真實航天嵌入式軟件的82 個并發缺陷進行了全面、深入的實證研究，揭示了航天嵌入式軟件原子性違反的表現形式特征.

2）提出了一個精確、高效的中斷驅動型程序原子性違反靜態檢測方法intAtom-S.

3）在基準測試集和真實航天嵌入式軟件上進行實驗評估，驗證了本文方法的有效性.

1 原子性違反特征研究

本節首先介紹原子性違反模式并給出真實案例；然后，對本文缺陷特征的研究方法進行闡述；最后，給出特征研究結果及對應的方法.

1.1 原子性違反缺陷模式

原子性違反缺陷模式指的是程序員對共享數據的連續多次訪問具有原子性期望,而其他并發流的搶占執行打破了這種期望，導致非預期的程序行為.對于中斷驅動型程序，該類缺陷主要發生在對單個共享變量的并發訪問中.由于程序員通常以順序思維進行程序設計，往往會假設對同一變量的順序訪問是原子執行的，容易忽視中斷搶占及其干擾，但程序在實際執行時并不能確保這種原子性[4,19].

圖2 所示為一個典型的原子性違反案例，該案例來自某航天控制軟件.主任務循環執行mode_manage函數并周期性地更新變量v_error_max的值，使其表示fabsf(set_loop-tyro_L)的最大值.若中斷在S1之后、S3之前發生搶占，則S2在這2 次訪問之間執行，導致tyro_L的值將在S2中被改寫.若此時改寫之后的tyro_L不再使fabs f(set_loop?tyro_L)的值滿足S1的條件語句，就會造成v_error_max并不是真實的最大值.變量v_error_max用于重要的航天器控制任務，此缺陷將會引發嚴重的后果.

1.2 缺陷特征研究方法

Fig.2 An example of typical atomicity violation圖2 一個典型的原子性違反案例

中國空間技術研究院負責研制我國衛星、飛船和深空探測器等各類航天器，包括中國空間站、天問一號火星探測器、嫦娥五號月球探測器和北斗導航衛星等.本文以2009—2022 年中國空間技術研究院第三方評測機構軟件問題庫作為缺陷的數據來源.該問題庫包含超過28 000 個軟件缺陷，這些缺陷在經過各種開發方測試后依舊遺留，代表了航天嵌入式軟件研制過程中最具挑戰性的可信問題.

在案例分析過程中，本文首先通過“中斷”“原子性”“沖突”“競爭”等關鍵字進行檢索和挖掘，得到了424 個相關缺陷案例.然后，為了篩選出具有完整的、可供進一步分析的原子性違反缺陷案例，逐一地對424 個案例進行核查.核查的標準為：1）案例包含詳細的問題報告單、原始代碼和修復后版本的代碼；2）對源代碼進行分析和理解后，確認該缺陷案例屬于原子性違反.最終，獲得了82 個信息完整的缺陷案例.這個選擇過程保證了最終研究的缺陷案例集具有代表性.

這些缺陷來源于各種不同型號的航天嵌入式軟件，覆蓋了近十年我國研制和發射的各類空間飛行器中的關鍵嵌入式軟件，包括航天器控制軟件、航天器綜合電子軟件、航天器中央數據單元軟件以及各類遙測遙控軟件等；此外，這些軟件的硬件運行環境涉及各種不同類型的處理器，如80C32，TSC695F，BM3803 等，這保證了實證研究的公平性和多樣性.

進一步，本文對所有收集的案例逐個進行研究，總結了造成原子性違反的共享數據訪問交錯模式，并對發生缺陷的共享數據的訪問方式和訪問粒度進行了分析和統計.

1.3 缺陷表現特征

本節對實證研究獲得的共享數據訪問交錯模式、訪問方式和訪問粒度等原子性違反缺陷表現特征進行了說明.

1）共享數據訪問交錯模式.本文借用可序列化[20]的思想，總結形成了4 種造成原子性違反的訪問交錯模式，如表1 所示，這些模式刻畫了中斷驅動型程序中的原子性違反.每個訪問交錯(ep,er,ec)都可以通過一次執行中對同一個共享數據的3 次訪問描述.其中，ep和ec為來自主任務或低優先級中斷isrl的本地串行訪問對，而er為來自另一個高優先級中斷isrh的遠程交錯訪問.

Table 1 Access Interleaving Pattern of Atomicity Violation表1 原子性違反的訪問交錯模式

2）原子區范圍.發生缺陷的本地串行訪問對在源代碼上的距離范圍分布如圖3 所示，最小范圍為1 行（例如2 次訪問在同一行代碼中，如a++），最大范圍為31 行，平均范圍為5 行.其中，24 個訪問對位于同一行，17 個訪問對相鄰（范圍為2 行）.此外，有8 個訪問對位于循環結構中，6 個訪問對作為函數參數被訪問.特別的是，所有的訪問對都在同一個函數中，或作為同一主調函數內不同被調函數的參數.

Fig.3 Distribution of atomic region range圖3 原子區范圍分布

3）中斷嵌套層數.在中斷驅動型程序中，并發交錯的數量會隨著中斷的數量呈指數級增長，此外中斷嵌套的存在將加劇此增長速度.然而，本文研究的82 個缺陷案例中，觸發這些缺陷所涉及的中斷數量都不超過2 個.其中，69 個缺陷發生在主任務和中斷之間；9 個發生在中斷與中斷之間；4 個發生在主程序和嵌套的中斷之間.

4）共享數據訪問方式.如表2 所示，在發生缺陷的共享數據中，有60%是通過全局變量名進行直接訪問的.在全局變量訪問方式中，程序直接將變量所在內存單元的值取出并進行運算；有32%通過指針解引用進行間接的訪問.8%的缺陷發生于訪問內存映射I/O（memory mapped I/O，MMIO）時.在中斷驅動型嵌入式軟件中，MMIO 是一種典型的數據類型，廣泛用于表示硬件數據資源，例如0x40008000 代表某個外設寄存器的內存映射地址，程序可以通過*（（unsigned char*）0x40008000）對該寄存器進行讀寫.

Table 2 Access Modes and Access Granularities on Shared Data表2 共享數據訪問方式與訪問粒度

5）共享數據訪問粒度.即使是對同一塊內存單元，程序也可能通過不同的訪問粒度進行訪問[18].如表2 所示，在研究的案例中，嵌入式軟件對共享內存的訪問存在各種不同粒度.46%的共享內存為整體訪問，即通過變量名對變量指代的整個內存區域進行訪問；26%的共享內存為通過數組下標對元素進行訪問；17%的共享內存為通過結構體對成員進行訪問；11%的共享內存需要精確到位訪問.此外，在所有的內存訪問中，9%的共享內存訪問帶有非常量的偏移量，例如數組元素BRCS T_buf[i]，其偏移量需要通過計算變量i得到，使得這些內存地址難以靜態確定.

缺陷表現特征研究表明，航天嵌入式軟件中，程序員具有原子性意圖的串行訪問在源代碼上具有較近的距離，可以通過限定原子區范圍對原子區進行推斷，從而降低計算開銷并減少誤報.對原子性違反的檢測可以通過成對（主任務和中斷，或中斷與中斷）的方式進行，從而以損失較低精度的代價實現對絕大部分缺陷的高效檢測.對共享數據的訪問通常涉及訪問方式和粒度的復雜組合，這增加了共享數據分析的難度.若共享數據分析只關注數組對象而不能區分數組元素，將會導致大量誤報；若不能識別MMIO 類型的共享數據，則會導致漏報.因此，為了提高缺陷檢測的精度，檢測工具需要精確的共享數據分析.

2 intAtom-S

本文基于原子性違反特征研究的結果，提出intAtom-S.圖4 所示為intAtom-S 的框 架.該框架主要包括3 個階段：基于抽象解釋的共享分析（見2.1 節）、訪問交錯模式匹配（見2.2 節）、不可行路徑裁剪（見2.3 節）.

首先，intAtom-S 精確地分析程序中的共享數據.intAtom-S 構建了一個數值不變式參數化的細粒度內存訪問模型；采用區間抽象域和同余抽象域的約化積（reduced product of interval and congruence，RPIC）[21]進行基于抽象解釋的數值分析，以獲得采用內存訪問模型表示的共享數據地址中的數值不變式，從而達到精確識別的目的.在文獻[18]的基礎上，intAtom-S引入基于規則的方法剔除標志變量，僅識別那些會導致缺陷的共享數據，這對進一步精化缺陷檢測結果至關重要.

Fig.4 intAtom-S framework圖4 intAtom-S 框架

其次，intAtom-S 使用輕量級數據流分析技術匹配符合4 種交錯模式的所有并發3 次訪問序作為潛在的原子性違反候選.intAtom-S 使用過程間分析并采用“工作單元”的概念[22]識別isrl中的串行訪問對.在此基礎上，結合來自isrh的訪問進行模式匹配以識別出屬于訪問交錯模式（表1）的并發3次訪問序.這些3 次訪問序是輸入到后續步驟的原子性違反候選.

最后，對缺陷候選采用基于路徑條件的約束求解.通過對串行訪問對和并發3 次訪問序進行路徑可行性分析，逐步消除沒有違反程序員預期和實際不可能發生的2 類誤報，得到最終的原子性違反結果：1）依次檢查isrl中2 個串行訪問之間的路徑可行性，如果不可行，表明程序員對該串行訪問沒有一致性預期，并發3 次訪問序不會造成原子性違反，因此將該類候選排除.2）intAtom-S 通過一個模塊化、路徑敏感的分析，消除在實際執行中由于約束條件無法滿足而不可能真實發生的并發3 次訪問序.為了縮減交錯空間和提高分析效率，本文引入了2 個策略：1）intAtom-S 為每個中斷構建一個符號化的摘要，幫助進行模塊化的路徑裁剪，以消除不可行的交錯.2）intAtom-S 采用代表性搶占點策略，在不損失精度的情況下縮減交錯空間.

相比文獻[17]，intAtom-S 基于更精確、更細粒度且剔除標志變量訪問后的共享數據識別結果，可以處理數組元素訪問、標志變量訪問導致的誤報，將顯著提高精度.

2.1 基于抽象解釋的共享分析

根據缺陷特征，intAtom-S 提出一種精確的共享數據靜態分析方法.該方法主要包括：

1）參數化的內存訪問模型.為了應對航天嵌入式軟件中共享數據訪問通常涉及的訪問方式和粒度的復雜組合，本文通過參數化的內存訪問模型對不同粒度的共享數據訪問進行統一刻畫.

2）基于抽象解釋的數值分析.使用RPIC 對每一個并發流進行基于抽象解釋的數值分析，計算內存訪問模型中偏移量的數值不變式.

3）共享訪問點識別.采用基于規則的方法剔除標志變量訪問，進而通過對不同并發流（主任務、各個中斷）之間的數據訪問點的數值抽象域進行“與操作”，識別出會導致缺陷的共享數據訪問點.

2.1.1 參數化的內存訪問模型

本節建立了一個可對標量類型、聚合類型以及MMIO 類型的共享數據進行統一表示的參數化的內存訪問模型來描述被訪問的各種抽象內存區域.這一模型表示為一個五元組（Base，Offset，Size，Mode，ConstAccess）.

1）Base是抽象內存區域的起始地址（一般用變量名標識，若數據為MMIO 則以ADDR_ZERO 標識）.

2）Offset是抽象內存區域的偏移量，為處理在同一程序點訪問多個不同元素或成員的情況（例如循環訪問數組變量），可將Offset定義為一個集合.

3）Size是每一塊抽象內存區域的大小.

4）Mode是對抽象內存區域的訪問方式，包括讀和寫.

5）ConstAccess可判斷該抽象內存區域是否寫入常量或者Mode為讀，若是，則置為true；否則，置為false.

表3 為圖5 案例中標量類型、聚合類型、MMIO這3 種類型數據在該模型中的表示（針對每個數據類型，以一個具有代表性的訪問為例，給出其表現形式）.例如，在訪問點⑤和⑥處，對upload_data[0]、upload_data[1]的寫訪問可表示為(upload_data,{0,4},4,write,false)，描述了對地址為upload_data+0、大小為4B 以及地址為upload_data+4、大小為4B 的2 個內存單元的寫訪問.

本文通過指針分析確定內存訪問模型中的Base值，根據發生訪問的程序語句可得到Size值和Mode類型.因此，如何精確地描述抽象內存區域將取決于Offset值集的精確性.

2.1.2 基于抽象解釋的數值分析

本節采用RPIC 抽象域對每一個并發流進行獨立的基于抽象解釋的數值分析，計算內存訪問模型中Offset的數值不變式.除此之外，本節還擴展了現有的抽象解釋迭代算法，以實現對中斷干擾的上近似，保證分析無漏報.

Table 3 Representation of Different Data Types表3 不同數據類型表現形式

Fig.5 Example for shared data access圖5 共享數據訪問示例

2.1.2.1 RPIC 抽象域.

本文使用數值抽象域來刻畫內存訪問模型中的Offset值集.在缺陷特征研究中發現偏移量的使用會出現在3 種情況中：1）訪問數組元素；2）訪問結構體或聯合體的成員變量；3）通過增加偏移量訪問MMIO.因此在抽象解釋過程中需要選擇適合這3 種情況的抽象域.RPIC 抽象域是區間抽象域和同余抽象域的約化積（reduced product）[21]，它可以描述連續區域和步長信息，步長信息用于分析通過間接尋址來實現訪問操作，如結構體成員訪問和指針解引用等.在RPIC 中，區間抽象域提供變量值的上界和下界，而同余抽象域計算值之間的步長.因此抽象元素可以表示為[a,b]∩(cZ+d).例如，圖5 示例中的訪問點⑤，⑥處，對應的偏移量被近似表示為[0,4]∩(4Z)，它表示一個下界為0、上界為4、步長為4 的離散整數集，即Offset值集為{4Z|Z∈[0,1]}.

2.1.2.2 中斷干擾的上近似.

本文擴展了現有的抽象解釋迭代算法，以實現對中斷干擾的上近似分析.對于中斷驅動型程序，若在程序分析時不考慮中斷并發對程序狀態的影響，將導致主任務中的部分執行路徑被誤認為不可行，從而導致漏報.如圖6 所示，若不考慮中斷執行，僅考慮主任務執行，由于(Flag=false)∧(Flag==true)為互斥的約束，S1將不會被執行，則KZData不會被訪問.而事實上在中斷的作用下，Flag會被賦值為true，即S1是可以被執行的，因此主任務中對KZData的讀訪問也是一次共享訪問.為了保證分析結果的可靠性，本文采用了一種簡單的處理策略，即在迭代過程中認為所有分支路徑都可行，以收集到所有的數據訪問點，實現對中斷干擾的上近似分析.

Fig.6 A case of interrupt side effect圖6 中斷副作用示例

2.1.3 共享訪問點識別

共享訪問點識別的目的是識別被不同并發流（主任務、各個中斷）訪問的共享數據.特別是intAtom-S 引入基于規則的方法將不會導致缺陷的標志變量的訪問剔除，僅返回那些會導致缺陷的共享訪問點集合.在中斷驅動型嵌入式軟件中，自定義標志變量總是遵循的規則為：標志變量為char 類型，且在整個程序執行過程中僅被賦值為常量.而這些標志變量的并發訪問并不會導致缺陷.因此，本節首先識別出僅被寫入常量的char 類型共享數據.intAtom-S 通過對不同并發流之間的數據訪問點的ConstAccess進行合取操作，識別出標志變量.例如，圖5 示例中的訪問點③，④和⑩，其共享數據分別被表示為（func_run,[0,0]∩{1Z},0,read,true ），(func_run,[0,0]∩{1Z},0,write，true )，(func_run,[0,0]∩{1Z},0,write,true).③，④和⑩具有相同的Base，對它們的constAccess字段進行合取操作，即true∧true∧true得到true，且func_run是一個char 類型數據，因此其是一個標志變量.然后，intAtom-S 通過對不同并發流之間的數據訪問點的數值抽象域進行與操作，識別出共享數據訪問.例如，圖5 示例中的訪問點⑨，其共享數據可被表示為(upload_data,[4,4]∩{1Z},4,write,true).訪 問點⑤和⑥處的共享數據為(upload_data,[0,4]∩{4Z},4,write,false).⑤和⑥與⑨具有相同的Base，對[4,4]∩{1Z}和[0,4]∩{4Z}進行與操作得到[4,4]∩{1Z}，因此upload_data[1]是主任務（⑥）與中斷（⑨）之間的共享數據.在此過程中，會分析并發流的優先級以確定它們能否并發執行.比如，相同優先級的中斷之間不能發生搶占，相應的數據訪問并不會構成共享.最后，將兩個或多個并發流之間的數據訪問交集標記為共享數據.

intAtom-S 最終返回一個包含所有去掉標志變量訪問之后的共享訪問點和訪問點位置信息的集合，訪問點位置信息包括發生訪問的函數、程序入口、語句行號、列號、源文件等字段.

2.2 訪問交錯模式匹配

表1 中訪問交錯模式的3 次訪問序(ep,er,ec)由對同一共享數據的3 個訪問事件組成，其中ep和ec來自isrl（或主任務），er來自isrh.每一個訪問事件e由一個四元組e=(T,L,V,A)表示，其中T為任務或中斷的標識，L是事件發生的程序點，V是被訪問的共享數據，A是訪問類型（讀或寫）.

算法1 描述了基于過程間數據流分析框架[23]的訪問交錯模式匹配方法.本文將對同一個共享變量v的2 次串行訪問建模為一個數據流問題.如果對于一個變量的2 次訪問ep和ec之間有一條路徑，且在該路徑上v沒有其它訪問，則構成一個串行訪問對.dataFlowAnalysis對該數據流問題進行求解，以查找出所有的串行訪問對.此外，根據Vaziri 等人[22]的工作，程序員的原子意圖與程序結構相關，可以在特定的“工作單元”邊界內對原子性進行推斷.受此啟發，結合實證研究結果，本文根據共享變量所在位置，將原子性的邊界限制在同一函數或主調函數內，并過濾掉那些超出邊界的訪問對.然后，對于isrh中的每個共享內存訪問，intAtom-S 檢查它和isrl（或主任務）中的串行訪問對是否可以組合為表1 中的訪問交錯模式（行?～?）.如果可以，intAtom-S 將該3 次訪問序(ep,er,ec)添加至原子性違反候選集.

算法1.訪問交錯模式匹配算法.

輸入：源程序P；

輸出：原子性違反候選集合C={(ep,er,ec)}.

2.3 不可行路徑裁剪

本階段利用路徑約束求解進行串行訪問，對可行性分析和并發3 次訪問序進行可行性分析，逐步消除誤報，從而得到最終的原子性違反結果.

2.3.1 串行訪問對可行性分析

在這個階段，本文通過識別路徑不可行的串行訪問對(ep,ec)消除一類誤報.如果某串行訪問對不可行，說明程序員對它們并沒有進行原子性假設，此類原子性違反候選將被過濾掉.如圖7 所示，對共享數據YCData共有3 次訪問，S1、S2與S3顯然滿足(W,W,R)模式.在該案例中，中斷Timer0_ISR通過S2周期性地更新YCData，并將標志變量fgAh置為true.只有當中斷將YCData數據更新后，主任務才會通過S3讀取YCData的值，該程序有意設計語句if(fgAh==true)以判斷中斷是否已經發生.雖然S1和S3是2 個連續的串行訪問，但它們具有互斥的約束(fgAh=false)∧(fgAh==true)，因此，這2 個訪問組成的串行訪問對是不可行的，表明程序員對它們沒有進行原子性假設.所以，有必要排除這些不可行的連續訪問對.

Fig.7 A case of infeasible consecutive access pair圖7 不可行串行訪問對示例

為了提高分析效率，本文建立依賴圖[23]對程序進行稀疏的表示.并在此基礎上構建串行訪問對的路徑約束，然后利用SMT 求解器進行約束求解.若路徑中存在循環，為了防止過高的開銷，對循環展開2次后跳出.

對于一個給定的串行訪問對(ep,ec)，P1 和P2 分別是由入口到ep和ec的路徑.路徑條件PC(ep,ec)由P1 與P2 的有效路徑條件[24-25]合取得到.其中，有效路徑條件通過對該路徑相關的數據依賴和控制依賴合取得出.因此，給定一條從入口出發的路徑P，vi為P的路徑約束所依賴的變量，P的路徑條件計算公式為

一個路徑條件由3 個部分組成：

1）C D(vi)為控制依賴，表示到達vi的條件約束；

2）vi?1=vi描述vi中存儲的值流向vi?1；

3）DD(vi?1,vi)表示值從vi流向vi?1是可行的.

2.3.2 并發3 次訪問序可行性分析

在串行訪問對(ep,ec)可行的前提下，分析3 次訪問序(ep,er,ec)并發路徑的可行性，進一步消除誤報.由于中斷程序的副作用，仍然存在一些原子性違反候選在實際的并發執行中永遠不會發生，即不存在一條可行的并發路徑包含該3 次訪問序.如圖8 所示，當中斷在主任務中的S1后被搶占，則S2是不可能發生的.這是由于如果在該搶占點的狀態需滿足(ono f fn um>0)∧(fgExecute==1)，則從ONOFFManage入口到S2的路徑條件(fgExecute==0)將不能被滿足.因此，給定一個原子性違反候選(ep,er,ec)，若要檢查其可行性，需要對ep與ec之間的每個搶占點p分別檢查其子路徑（p→entryisr→…→er）與（exitisr→p→…→ec）的可行性.由于并發路徑的數量為指數級，這一步驟非常耗時.

Fig.8 A case of infeasible concurrent triple access interleaving圖8 不可行并發3 次訪問序示例

如算法2 所示，intAtom-S 采用了一種組合方法以降低不可行并發3 次訪問序裁剪的開銷.

1）模塊化地構建中斷摘要.intAtom-S 首先通過constructSummary對每個中斷構建符號化摘要，從而避免冗余路徑條件計算（行①～③）.摘要使用符號約束描述了er的路徑條件與exitisr的狀態.

2）選擇具有代表性的搶占點.對于每一個原子性違反候選，intAtom-S 通過函數selectPreemptPoint選擇具有代表性的搶占點，以縮減交錯空間（行④～⑤）.

3）利用約束求解驗證可行性.對于每一個選擇出的代表性搶占點p，分別檢查其子路徑（p→entryisr→…→er）與（exitisr→p→…→ec）的可行性.

intAtom-S 通過函數obtainState（行⑧）獲得代表性搶占點處的全局程序狀態，并將此信息作為上下文傳遞給中斷.然后，函數isFeasible提取摘要中的約束條件，并利用約束求解器來檢查以搶占點p為上下文時，路徑entryisr到er的可行性（行⑨）.如果這條路徑不可行，則意味該3 次訪問序為誤報，需要被裁剪掉；否則，intAtom-S 將繼續分析以exitisr為上下文時，搶占點p和ec之間路徑的可行性（行?）.constructPC使用與2.3.1 節相同的方法構建路徑條件.如果（p→entryisr→…→er）與（exitisr→p→…→ec）這2 條 路徑都可行，intAtom-S 將向用戶報告一個原子性違反.由于intAtom-S 區分了每個搶占點的上下文并檢查每條路徑的可行性，因此是上下文敏感和路徑敏感的.

intAtom-S 還在全局程序狀態中對中斷屏蔽的使用進行了建模.本文將中斷屏蔽寄存器作為全局變量，并在每個中斷的入口檢查是否被屏蔽.因此，本文的方法可以處理通用中斷屏蔽.

算法2.并發3 次訪問序可行性分析算法.

輸入：原子性違反候選集合C={(ep,er,ec)}、源程序P；

輸出：原子性違反.

接下來，將詳細介紹中斷摘要構建與代表性搶占點選取的細節.

1）中斷摘要構建.當檢查并發3 次訪問序可行性時，需要獲取2 個中斷信息：①了解entryisr到er的路徑條件，用于檢查路徑ep到er的可行性；②了解經過er的路徑在中斷出口處全局變量的狀態，以確定是否存在從中斷退出回到ec的可行路徑.因此，本文構建包含這2 個中斷信息的中斷摘要，當檢查路徑可行性時，在不同的搶占點處復用這些

摘要.給定一個中斷isr和一組變量集合Π={e0,e1，…}，該集合代表isr中所有可能的er，isr的摘要可由集合S ummisr表示，可以表示為三元組集合其中pcei代表從entryisr到ei的路徑條件，代表isr出口處的全局狀態.

本文單獨分析每個中斷來構建它的摘要，可在并發3 次訪問序可行性檢查時直接復用.對于isr中的訪問事件er，存在2 種情況可以重用中斷摘要.一是檢查涉及er的多個原子性違反候選的可行性；二是對同一個候選的多個搶占點進行檢查.

2）代表性搶占點選取.并發3 次訪問序(ep,er,ec)的可行性取決于2 條子路徑（p→entryisr→…→er）與（exitisr→p→…→ec）的可行性.然而，只有當程序語句直接修改了2 條并發子路徑的約束條件，或者修改了約束條件所依賴的變量時才會影響到并發3次訪問序的可行性.也就是說，某些程序語句的副作用可能對這2 條子路徑可行性檢查的結果沒有影響.因此，可以選擇性地檢查部分搶占點對應的并發路徑，而無需檢查所有的路徑，這些搶占點就被稱為代表性搶占點.

從ep到ec路徑上的所有程序語句可用集合S={S1,S2,…,Sn}表示，其中Si是Si+1的直接前序語句.用P={p1,p2,…,pn}表示搶占點集合，其中pi位于Si與Si+1之間，稱Si為搶占點pi對應的程序語句.本文代表性搶占點定義為：給定搶占點pi與pi+1，如果pi滿足2個條件之一，那么其為一個代表性搶占點.1）Si+1為一個賦值語句，且Si+1沒有改變任何路徑約束中包含的變量的取值；2）Si+1包含一個條件表達式，該條件表達式的控制變量與中包含的變量不重合.

因此，通過按順序遍歷P以選取所有ep到ec之間的代表性搶占點.對于每一個搶占點pi，如果其未滿足上述條件，那么pi+1將被選擇為代表性搶占點；否則，pi+1可以被當前選定的代表性搶占點代表.

圖9 顯示一個選擇代表性搶占點的例子.(ep,er,ec)為一個原子性違反候選.主任務與中斷中的語句記為Si，搶占點記為pi.S2對變量fgCurrentB進行了寫操作.由于路徑(p→entryisr→…→er)的路徑條件與變量fgCurrentB無關，且S2不是分支語句，因此p2可以被p1代表；同樣p3可以被p2代表.而S4對全局變量fgAh進行了寫操作，fgAh在路徑條件中，因此p4不能被p3代表.本文選擇p4為新的代表性搶占點.S5對變量fgCharge進行寫操作，然后fgCharge用于S6中條件表達式中.然而fgCharge不包含于中，因此p5與p6可以被p4代表.對于S7，fgPower是條件表達式的控制變量，且包含在中，因此p7不能被p4代表.最后，選擇3 個代表性搶占點p1，p4與p7.

3 實驗評估與應用

本文在一臺配備Intel(R) Xeon(R) E5-2 620 CPU、32GB RAM 和Ubuntu 20.04 操作系 統的計 算機上 進行了實驗.為了評估intAtom-S，考慮4 個研究問題：

問題1：intAtom-S 在檢測中斷驅動型程序的原子性違反方面有效性如何?

問題2：intAtom-S 在檢測中斷驅動型程序的原子性違反方面的效率如何?

問題3：intAtom-S 分析共享數據的有效性如何？

問題4：intAtom-S 路徑裁剪的有效性和效率如何?

3.1 實驗設置

為了評估intAtom-S 的缺陷檢測能力，本文將其與Rchecker[15]進行實驗對比，Rchecker 是與intAtom-S 最相近且最新提出的方法，它們針對的都是中斷驅動型程序中的原子性違反.然而Rchecker 不是開源工具，且只在基準測試集Racebench2.1 上進行過實驗，因此本文同樣在Racebench2.1 上對intAtom-S 進行實驗.為了進一步評估本文方法的實用性，還在8 個真實的中斷驅動型航天嵌入式軟件上進行了實驗.目前為止，intAtom-S 是唯一一個在工業嵌入式軟件上進行評估的并發缺陷檢測工具.此外，本文還將intAtom-S與static-TSA[26]進行實驗對比，以評估其分析共享數據的有效性.實驗中使用了2 個數據集.

Fig.9 An example of representative preemption points selection圖9 代表性搶占點選擇示例

1）數據1 是基準測試集.本文使用開源基準測試集Racebench 2.1 來評估intAtom-S 是否可以在各種場景中檢測原子性違反.Racebench2.1 最初被用于作為評估NASAC 2019 并發缺陷檢測工具競賽的參賽工具.后來，它也被用于Rchecker[15]的實驗分析.Racebench 2.1 由31 個中斷驅動型案例和54 個手動注入的原子性違反構成.這些案例都是基于真實航天嵌入式軟件的特點設計的，能夠反映現實世界中斷并發程序的語法和語義特點.這些案例涵蓋原子性違反的各種表現形式，如訪問交錯模式、共享數據類型、訪問方式、控制流場景等.Racebench 2.1 考慮了發生缺陷的不同場景，有助于對工具進行全面的評估.

2）數據2 是真實中斷驅動型航天嵌入式軟件.為了評估intAtom-S 是否能夠有效檢測真實中斷驅動型軟件中的原子性違反，從實證研究的缺陷案例中選取了8 個具有代表性的軟件，如表4 所示，所選案例的規模從970 行到5 099 行不等，是中斷驅動型航天嵌入式軟件最典型的代碼規模.首先，標記了這些軟件的CPU 類型、程序規模和中斷個數，這是反映真實嵌入式軟件多樣性的3 個重要屬性.然后，以涵蓋這3 個屬性的多種組合為目標，選取具有代表性的案例.盡管我們希望選用盡可能多的案例進行實驗，然而評估真實的航天嵌入式軟件需要消耗大量的時間和資源.主要原因為：①嵌入式軟件的編譯平臺多種多樣，不同的編譯器（如MCS-51，MSP430）采用不同的語言擴展，如數據類型、關鍵字等.由于原型工具只支持ANSI C，因此需要對源代碼進行大量修改才能將原始代碼轉換為等價的ANSI C 代碼.②原子性違反的確認需要應用程序（系統）相關的特定知識.所有原始報告中的警報都需要開發人員單獨分析確認.一般來說，每個項目需要一個多月的時間才能完成確認.因此，本文最終選擇了8 個具有代表性的案例作為實驗對象.

Table 4 Analyzed Real-world Aerospace Software Projects表4 被分析的真實航天軟件項目

3.2 檢測有效性（針對問題1）

1）基準測試集檢測結果.

在基準測試集Racebench 2.1 上的實驗結果如表5所示.intAtom-S 可以在基準測試集中檢測出所有的原子性違反，并顯著減少誤報.intAtom-S 在31 個基準測試集案例中只有6 個誤報，相比Rchecker 誤報率降低了72%.

我們發現，Rchecker 誤報的主要原因是因為忽視了對程序員的原子性意圖的推斷.因此，沒有原子性期望的3 次訪問序也被報告為缺陷.而intAtom-S則有效地解決了這一問題.進一步分析了intAtom-S的6 個誤報，誤報原因都是因為在循環中使用了簡化路徑條件計算.由于有一些在循環中被訪問的共享數據，是被循環計數變量相關的約束所保護的.為了避免循環展開，intAtom-S 簡單地忽略了該路徑約束.因此可能會錯誤地將條件訪問視為對同一變量的多次訪問.可以通過對循環使用路徑進行敏感分析以消除這些誤報.然而，這將不可避免地增加開銷.因為當循環計數非常龐大的時候，會產生巨額開銷.

Table 5 Results of Benchmark表5 基準測試集檢測結果

續表 5

2）真實中斷驅動型航天嵌入式軟件檢測結果.

表6 給出了在真實航天嵌入式軟件上的檢測結果.每個階段的結果分別由3 部分組成，“違反個數”表示進行當前階段的原子性違反候選個數；“減少比例”指與上一階段相比，原子性違反減少的比例；“時間占比”表示當前階段的時間開銷占總時間的百分比.每一個報告的原子性違反都經過開發人員檢查與確認，最終確定是否為一個真實缺陷.從表6 可以看出，intAtom-S 在8 個真實軟件中檢測出45 個原子性違反，平均誤報率為8.9%.實驗結果顯示，intAtom-S 可以有效地檢測真實工業嵌入式軟件中的原子性違反，且具有非常低的誤報率.

Table 6 Detection Results of Real-World Interrupt-Driven Aerospace Embedded Software表6 真實中斷驅動型航天嵌入式軟件檢測結果

進一步分析這些檢測結果，將其分為3 類：有害原子性違反、良性原子性違反和誤報.其中缺陷是否為良性也需要經過領域專家的檢查與確認.intAtom-S 檢測到23 個有害的原子性違反都已經得到開發人員的確認.檢測到的18 個良性原子性違反可分為2 類.1）雖然ep和er是2 個連續的本地訪問，但是開發人員對它們沒有原子性的期望.例如，開發人員預計ep之后會出現中斷，并使用ec進行容錯.2）原子性違反對結果沒有影響.例如，一個并發3 次訪問序(ep,er,ec)匹配模式(W,W,R)，如果ep和er將相同的值存儲到共享數據中，ec總是讀取期望值.值得注意的是，本文基于文獻[17] 中的intAtom 進行擴展，intAtom共檢測到3類良性原子性違反，除去這2 類，還有一類是由開發人員有意設計的.例如，在模式(R,W,W)中，ep對標志變量的讀訪問 處于循環條件語句中，等待特定的中斷搶占并執行er以改變此標志變量的值使條件滿足，從而執行循環體中的代碼段；執行完畢后通過ec重置此標志變量的值.然而，本文在共享數據識別階段去除了標志變量訪問，所以檢測階段不會再報告此類良性原子性違反，這表示intAtom-S 的檢測結果更加精確.

intAtom-S 結果中存在的4 個誤報都是由于在循環中使用了簡化的路徑條件計算所導致.相比intAtom，intAtom-S 的檢測結果更加精確，如表7 所示.intAtom 在這8 個真實程序的檢測結果中存在11個誤報，其中有6 個是由于當循環計數變量用作數組下標時，intAtom 不能區分這些數組元素所導致的；還有1 個是由于標志變量訪問造成的.而本文方法采用精確的共享數據分析，能夠識別標志變量訪問，且區分數組元素，因此可以避免這些誤報.

Table 7 Comparison of Effectiveness and Efficiency Between intAtom-S and intAtom表7 intAtom-S 與intAtom 有效性及效率對比

3.3 檢測效率（針對問題2）

表5 顯示了intAtom-S 和Rchecker 的在基準測試集Racebench 2.1 上的運行時間.為了公平地分析時間性能，本文只比較了2 個工具都能完成檢測的案例上所花費的時間.例如，由于Rchecker 無法分析案例24.因此，本文只關注其余30 個案例的實驗數據.從總體上看，相比Rchecker，intAtom-S 在大多數案例（26/30）上花費更短的檢測時間，intAtom-S 的平均檢測時間為0.196 s，而Rchecker 的平均 檢測時間為0.592 s.

由表5 可知，在所有的案例中，intAtom-S 的最長檢測時間為0.578 s.而Rchecker 在某些案例上的檢測時間則都多于1 s（如案例5、17、29），甚至最長檢測時間達到了5.2 s.檢查這些案例的代碼，發現它們都具有龐大而復雜的交錯空間，這導致Rchecker 的分析時間呈指數級增長.intAtom-S 使用函數摘要和代表性搶占點，可以有效緩解交錯空間爆炸，從而達到更高的檢測效率.

表7 顯示了intAtom-S 與intAtom 在真實中斷驅動型程序上的檢測時間對比.真實的中斷驅動型程序規模相對較大，包含數千行代碼.intAtom-S 可以在305 s 內分析5 000 行的真實航天嵌入式軟件，雖然比intAtom 時間開銷略高（額外開銷介于1.8%～50.4%），卻實現了更高的檢測精度，能夠滿足實際工業需求.

3.4 共享數據分析效果（針對問題3）

由于基準測試集中都是代碼規模較小的案例，對于不同數據類型的代表性不強，不具有統計學意義.本文在8 個真實的航天嵌入式軟件上進行了intAtom-S 與static-TSA 的共享數據分析對比實驗.在這8 個軟件中，存在3 種共享數據類型（標量類型、聚合類型、I/O 地址）.值得注意的是，static-TSA 利用調用圖和指向分析來識別共享數據訪問，然而與intAtom-S 相比，static-TSA 既不能處理I/O 地址訪問，也不能區分數組中的各個數組元素，這導致其實驗結果存在大量誤報與漏報.

表8 顯示了intAtom-S 與static-TSA 共享數據分析的結果.本文手動分析每個檢測到的共享數據并進行最終確認.由于intAtom-S 以原子性違反檢測為目標，進行共享數據分析時剔除了標志變量訪問，而static-TSA 并不進行此操作，為了保證對比實驗的公平性，本文將static-TSA 結果中的標志變量訪問手動剔除,進而對兩者進行對比.對于這8 個程序，intAtom-S 檢測所有共享數據都沒有誤報；而static-TSA 具有191 個誤報.這是由于static-TSA 不能區分數組索引，導致對不同數組元素的訪問被標識為同一數據的訪問.此外，static-TSA 遺漏了29 個共享的I/O 地址訪問；而intAtom-S 不僅可以區分數組索引，且能有效檢測共享的I/O 地址訪問，因此能夠精確檢測航天嵌入式軟件中各種類型的共享數據.

Table 8 Results of Shared Data Analysis表8 共享數據分析結果

3.5 路徑裁剪效果（針對問題4）

為了更好了解intAtom-S 路徑裁剪的有效性和效率，本文關注通過模式匹配檢測到的原子性違反候選的數量、經過路徑裁剪后剩余的候選數量，以及它們的時間開銷，分析結果如表6 和表9 所示.

實驗結果表明，路徑裁剪具有非常顯著的貢獻.在模式匹配階段，intAtom-S 檢測每個項目中潛在的原子性違反候選，平均每個項目有238 個候選.在路徑裁剪階段，intAtom-S 首先通過串行訪問對可行性分析裁剪了42.2%的候選，平均每個項目剩余100 個候選.然后intAtom-S 通過并發3 次訪問序可行性分析裁剪了97.6%的候選.每個階段的時間開銷如表6所示.在模式匹配和路徑裁剪階段，intAtom-S 花費的時間分別占總時間的37.8%和46.3%.

為了進一步評估所提出的符號化中斷摘要和代表性搶占點選擇方法的有效性，本文實現了2 個額外的intAtom-S 變體：Naive 和Naive+RPPS（使用代表性搶占點選擇）.Naive 可以被看作是一種基線方法，它在沒有中斷摘要的情況下，檢查并發3 次訪問序的可行性.Naive+RPPS 同樣不使用中斷摘要，但僅在每個代表性搶占點處進行路徑約束求解.本文在8 個真實航天嵌入式軟件上進行了實驗，比較了intAtom-S，Naive 和Naive+RPPS 進行并發3 次訪問序可行性分析時的時間開銷.如表9 所示，Naive+RPPS 的效率是Naive 的1.2～3.6 倍，平均1.8 倍；intAtom-S 的效率是Naive的2.6～8.5 倍，平均3.0 倍.結果表明，符號化摘要和代表性搶占點對提高方法可擴展性是至關重要的.

Table 9 Time Cost of Naive+RPPS and intAtom-S Compared with That of Naive表9 Naive+RPPS 和 intAtom-S 與Naive 的時間開銷對比

4 相關工作

近年來，學者們提出大量檢測多線程程序原子性違反的方法[5-10,20,27-29].Lu 等人[20]基于同一原子區中共享數據的訪問交錯定義了可串行化.在此基礎上，他們提出了訪問交錯不變量，并根據該不變量檢測原子性違反.在他們后續的工作中進一步提出CTrigger[27]，通過軌跡分析以識別不可串行交錯，并測試低概率交錯以暴露原子性違反.Lucia 等人[28]提出Atom-Aid，使用硬件簽名來檢測原子性違反，動態地調整塊邊界，在不需要任何程序注釋的情況下規避缺陷.Chew 等人[29]提出Kivati，通過結合靜態和動態分析以檢測和避免原子性違反.Wang 等人[10]提出了一種基于預測的檢測原子性違反的方法，通過監視執行交錯以記錄執行序列，并根據訪問交錯候選序列預測潛在的缺陷.Razavi 等人[8]提出一種基于人工智能的預測原子性缺陷的方法.Sorrentino 等人[9]提出一種算法挖掘一組導致原子性違反的執行序列，并使程序按這種序列執行以暴露缺陷.然而，中斷模型無論在調度、同步還是搶占關系上都與線程模型不同.而且，大多數方法所依賴的動態分析很難直接應用于中斷驅動型程序中.

目前有一些方法用于檢測中斷驅動型程序中的數據競爭[19,30-33].Wang 等人[19]提出SDRacer，將靜態分析與符號執行相結合，通過為中斷驅動型嵌入式軟件生成輸入數據來自動檢測數據競爭.Wu 等人[32-33]自動化地將中斷程序順序化為一個非確定的順序程序，分別采用限界模型檢測框架和抽象解釋的方法來分析程序中的數據競爭.Chopra 等人[30]為中斷程序定義了數據競爭與happens-before 的自然概念，他們還提出不相交塊的概念來定義同步以及高效的“sync-CFG”，從而展開靜態分析.然而中斷程序經常使用定制的同步機制，例如用戶定義的基于標志變量的同步.很多數據競爭是專門設計出來進行數據共享的，這些數據競爭都是良性的，若以數據競爭為檢測目標，會存在大量誤報.相比之下，本文的方法側重于最可能有害的原子性違反.

據我們所知，目前只有文獻[4,15,17]可用于檢測中斷驅動型程序中的原子性違反.文獻[4]采用基于抽象解釋的方法，可以有效地識別程序中潛在的原子性違反.然而，由于其分析對路徑不敏感，存在大量誤報.文獻[15]提出基于限界模型檢測的檢測方法，可以得到比較準確的結果，但可擴展性很差.文獻[17]采用了階段性的方法，可以同時實現更高的精度和分析.而本文在文獻[17]的基礎上增加了精確的共享數據分析，使結果進一步精確，能夠有效檢測工業規模的中斷驅動型嵌入式軟件.

5 總結

本文對航天嵌入式軟件中原子性違反缺陷的表現形式進行了系統的實證研究，獲得了原子區范圍、中斷嵌套層數、共享數據訪問交錯模式、訪問方式、訪問粒度等5 方面的表現特征.基于這些特征，提出了一個精確、高效的中斷驅動型程序原子性違反靜態檢測方法intAtom-S.該方法首先進行精確的共享數據分析，將共享數據訪問粒度精確至數組元素，并可識別標志變量訪問與共享的內存映射I/O 地址.然后，使用輕量級數據流分析技術匹配符合缺陷訪問交錯模式的所有并發3 次訪問序作為潛在的原子性違反缺陷候選.最后，采用基于路徑條件的約束求解對缺陷候選中的串行訪問對和并發3 次訪問序進行路徑可行性分析，逐步消除誤報，得到最終的原子性違反結果.本文分別在基準測試集與真實航天嵌入式軟件中對intAtom-S 進行了評估.結果表明，intAtom-S 顯著降低了誤報率，提高了檢測效率，并可滿足真實航天嵌入式軟件的檢測需求.

進一步的研究工作包括：

1）中斷驅動型軟件的設計中往往隱含了一些時序約束，而這種約束并不體現在代碼中，對于以源代碼為唯一分析對象的工具，該類誤報很難消除.未來可考慮對由用戶創建的系統時序模型進行精確檢測；

2）使用訪問交錯模式雖然很好地刻畫了原子性違反，但其中仍涵蓋了一些并不是缺陷的情況，未來可以進一步精化該模式.

作者貢獻聲明：于婷婷和李超為共同第一作者，提出了算法框架和實驗方案，完成實證研究并撰寫論文；王博祥負責完成工具開發和實驗；陳睿提出總體研究思路并撰寫論文；江云松提出指導意見并修改論文.