裝備電子系統的研發、測試、保障解決方案中心

符合DO-178B/C驗證要求的需求可追蹤工具VeroTrace

VeroTrace是一個需求和生命周期可追蹤管理的工具，允許產生、管理和發布用于支持DO-178B/C軟件認證/審核的所有數據。它可以追蹤系統需求、軟件需求，追蹤與需求相關的工件，例如：源代碼，設計組件，功能測試結果，覆蓋率測試結果。

 VeroTrace提供一個需求跟蹤數據庫，在數據庫中可以添加、修改、刪除、提問，追蹤驗證狀態，執行在線驗證，可以從配置管理中提取工件數據，創建驗證檢查列表，提供在工件和驗證證據之間基本的跟蹤XML文件。VeroTrace通過自動生成超鏈接的可追蹤性信息，可以組織需求、與需求相關的工件及所有評審文件，到一個鏈接所有生命周期中可追蹤性數據的CD-ROM，以便于驗證和審核。

●需求的導入、編輯和查詢

●定義完整的需求狀態（比如部件是否導入、評審狀態、聲明周期階段等）

●跟蹤每個需求和部件的評審狀態（評審狀態轉換時管理基線）

●在線評審需求和部件（可以集成配置管理系統，或使用桌面文件系統）

■需求評審和分析

■工作產品和評審

■測試和評審

將評審意見記錄到可追蹤性數據庫；自動生成評審檢查單（通過VeroStyle的幫助）以及檢入檢查單到配置管理中

●生成XML數據用于VeroStyle轉換到報告和度量中，管理需求和工作產品報告以及從VeroTrace中產生的文檔。  

●驗證追蹤（VoT）

VeroTrace 是一個生命周期追蹤管理工具，可以產生、管理和交付支持安全關鍵軟件確認和許可的數據。工具完成兩大任務：工作產品追蹤的驗證（AVoT）和超鏈接的追蹤驗證（HVoT）。

VeroTrace產生一個校驗數據包的CD-ROM 影像，內含超鏈接追蹤所有的需求和工作產品?？梢源_保：

■工作產品的名稱為RTD，匹配CD中實際相對應的文件，包含從配置管理系統中提取的基線工作產品。這就是工作產品追蹤的驗證（AVoT）

■所有的超鏈接是由VeroTrace自動生成，含有期望的目標文件。這就是超鏈接的追蹤驗證（HVoT）。

l運行平臺：Windows XP/7/10

符合DO-178B/C驗證要求的目標碼分析工具VerOCode

VerOCode是一個不需要特殊硬件的執行跟蹤分析工具。被測試的代碼不需要插裝（不添加記錄執行狀態的功能調用）。應用代碼在目標計算機（例如PowerPC，V8）上執行，執行的數據圖表搜集到一個宿主機上（PC/Windows或更高配置）。VerOCode使用搜集的執行數據圖表與鏈接器符號信息和編譯器產生的清單一起，可以顯示出哪些指令執行了，哪些指令沒有執行，以及條件指令執行過程中的條件代碼狀態。產生的VerOCode結果清單包含了DO-178B/C A級，最高級別的安全性要求所要求的覆蓋率分析的證明。

VerOCode記錄和顯示被測試程序中執行的指令。對于條件指令，VerOCode顯示每次指令執行時的條件代碼的狀態。覆蓋率在機器碼級獲得，結果通過一個包含源代碼和匯編語言擴展的程序清單來報告。 工作在交叉模式。監控和測試程序（測試控制和被測單元）在目標機上執行， 目標機通過通信口語宿主機連接。一個測試運行以后，搜集的覆蓋率數據上載到宿主機來分析。

VerOCode設計為三個模塊：

1) 第一個駐留在目標系統中（監控程序），搜集覆蓋率數據；

2) 第二個是基于宿主機的（分析工具），實現覆蓋率分析和報告；

3) 一旦覆蓋率分析完成，結果文件可以通過第三個Coverage Editor來注解。這個模塊幫助確認無用的代碼。

●顯示目標代碼級的覆蓋率；

●能夠結合多個測試的結果，以提供累計覆蓋率數據；

●通過單獨搜集每個條件的結果能夠獲得條件判斷的覆蓋率（MCDC） ；

●不插裝被測代碼；

●能夠記錄覆蓋率數據；

●能夠形成一部分可重復的、自動化的測試和覆蓋率分析腳本；

●作為認證證明數據，VerOCode 可以用作一個驗證工具，其覆蓋率結果可以作為認證信用。 VerOCode可以與認證材料一起提供，能夠用于A級認證系統；

支持的目標平臺：SPARC V8、PPC、Intel處理器。

符合DO-178B/C驗證要求的控制耦合目標的驗證工具VerOLink

基于需求的測試驗證了軟件行為是按照預期來實現的。使用結構覆蓋率分析，尤其在目標碼上的分析，能夠證明不期望的功能已經被去掉。那么剩下來的工作就是確定和給出目標證明，每個軟件函數是按照預期被調用的，由鏈接器產生的錯誤沒有被發現，符合DO-178B/C的控制聯合目標的要求。

VerOLink幫助滿足DO-178B/C的控制目標。VerOLink驗證了在鏈接器（linker）鏈接多個目標模塊時產生的可執行鏡像內的函數調用可以被正確分解。VerOLink檢查在可執行鏡像內的被調用函數的地址與函數調用時的地址是否一致，在本質上驗證系統鏈接器產生的鏈接，這些鏈接來自單獨的編譯單元內的函數調用。

●VerOLink是一個滿足DO-178B的控制聯合目標的驗證工具?？刂坡摵弦髾z測集成多個分別編譯的目標文件形成一個可執行映像的正確性。

●VerOLink用來完成這個最終的檢查。代碼集成的驗證再現鏈接器和相關工具分別執行的過程，交叉檢查集成的一致性。

●VerOLink驗證當鏈接器組合目標模塊時一個可執行映像中的函數調用已經被正確地解析了。

●VerOLink檢查執行映像中的函數地址是對應于被調用的函數的起始地址的。這樣就驗證了通過鏈接器產生的分別編譯的單元間函數的符號鏈接。

●VerOLink可以與認證材料一起提供，能夠用于直到A級認證的任何認證級別的系統。

●VerOLink在Windows主機平臺運行，支持PPC Target和GNU C。

符合DO-178B/C 驗證要求的BC級軟件覆蓋率分析工具VeroSource

 VeroSource可以計算在PPC目標環境下的代碼覆蓋率，用于得到源代碼級別的語句分支覆蓋率，可以滿足在適航項目中對代碼進行語句分支覆蓋分析的驗證要求。主要應用由C語言編寫的B/C類軟件驗證。提供DO-178B/C中B/C類軟件所需的證明。

VeroSource由四個模塊構成：

1) 插裝器（主機上）完成對C代碼的插裝；

2) 監控器（目標機上）從目標機捕獲并傳送數據到主機；

3) 分析器（主機上）使用覆蓋率信息注解列表；

4) 編輯器（主機上）是一個定制工具，可以在覆蓋率不完備時編輯和標記注解列表。

插裝器、分析器和編輯器組成的主機系統可以運行在一個PC電腦。插裝器完成對預處理過的源碼進行插裝，作為分析器的輸入源。 插樁后的被測程序和用來驅動被測程序的測試程序，經過一起編譯鏈接后，下載到目標機上執行。 測試運行后，由監控器捕獲的覆蓋率數據上載到PC主機，分析器使用覆蓋率信息注解C代碼列表。 編輯器根據分析器產生的帶有注解的源碼XML文件，在覆蓋率不完備時編輯和標記注解列表，并且產生HTML格式報告。

●支持源碼級別的語句分支覆蓋率分析；

●支持C代碼插裝；提供目標平臺的測試數據捕獲程序；

●支持覆蓋率結果標注到代碼；

●提供DO178B/C中B/C類軟件所需的證明。

●提供完整的Verocel工具質量文件（Tool Qualification Documents）。

●支持PPC目標平臺（PSC ARINC 653或者VxWorks 653），GNU C。

符合DO-178B/C 驗證要求的A級軟件覆蓋率分析工具VeroSource-A

VeroSource-A是覆蓋率分析工具VerOCode和VeroSource的補充，可以滿足DO-178B/C A級軟件指定的最嚴格的覆蓋分析要求，即修訂的條件/判定覆蓋率（MC/DC）。

VeroSource-A與VeroSource一樣也是由插裝器、監控器、分析器、編輯器四個模塊構成。

●插裝器的功能

 插裝器在預處理的源文件中插入以下實體：

■聲明覆蓋監視函數（VerOSource_D和VerOSource_C）；這些函數用于獲取判定和條件的覆蓋信息。

■定義覆蓋數據表（VerOSource_CT）；每個源碼的覆蓋信息保存在這張表中。

■在合適的地方調用覆蓋監控函數。

■被覆蓋監控函數使用的本地變量（VerOSource_S）的定義。

■附加工具-內置信息（作為一條注釋在文件的結尾）。

●監控器功能

監控器是駐目標機程序模塊監測插裝后測試程序的執行，在覆蓋率數據表格中獲取覆蓋率信息。每一個源文件都有一個覆蓋率表格。表格可以讀取目標機監控器的信息轉移到主機從而進行深入分析。用戶開發的測試工具用于啟動和停止監控器，轉移覆蓋率結果從目標機到主機。

●分析器的功能

分析器校對從目標機上帶有相應源碼列表的的Monitor中收集的覆蓋數據，并生成帶注釋列表的XML文件。分析器注釋信息列表，使分析的覆蓋信息容易理解。結果文件中的所有判定和條件，以特定的XML屬性標記并顯示覆蓋率。XML文件可在編輯器中打開。

分析器需要有預處理過的C源碼文件、插裝的或注釋的C源碼文件，以及覆蓋數據表文件。如果輸入文件已被注釋或相應的源碼文件有兩個或多個覆蓋數據表，該工具會合并覆蓋數據。

●編輯器的功能

編輯器接收分析器產生的XML文件，顯示帶有注釋的列表。用戶可以查看源代碼和覆蓋注釋。如果必要，可能在帶有覆蓋說明的列表文件中添加注釋。編輯器不會更改或不允許更改列表，源代碼和覆蓋數據。

●支持PPC目標平臺（PSC ARINC 653或者VxWorks 653），GNU C。

最差堆棧使用情況分析工具VeroStack

VeroStack可以計算代碼在最差條件下使用堆棧的情況，支持Ada、C、C++、以及匯編語言?？梢栽谥鳈C上運行，直接分析應用的執行鏡像?？梢苑治鱿到y和應用程序的堆棧使用，支持DO-178B/C中的A級軟件驗證。

在使用 VeroStack 編輯器標識出應用入口以及應用中代表任務和進程的程序，它們都有自己的堆棧， VeroStack 分析出程序的調用關系，通過這些信息， VeroStack 計算應用中每個堆棧在最差條件下的大小，并產生可以作為驗證數據的報告。

VeroStack由三部分構成：

1) Image Processor：分析被測軟件執行映像，定位所有符號和調用。

2) Editor：允許用戶完善缺少的堆棧分析數據（如間接調用，未知堆棧結構等）。

3) Calculator：總結和呈現堆棧分析結果。

●基于目標碼分析。

●支持C、C++、Ada和匯編語言的分析。

●VeroStack 編輯器是用來解析間接調用的。通過這些信息， VeroStack 計算應用中每個堆棧在最差條件下的大小，并產生可以作為驗證數據的報告。

■直接和間接的遞歸調用

■通過指針的調用

■間接調用（比如在C++中通過分配表dispatch tables進行的調用）

●在Windows主機平臺運行，支持PPC Target。