德國 AbsInt 公司是全球領(lǐng)先的安全苛求軟件研發(fā)、確認、驗證和認證工具鏈供應商。能夠為客戶提供完整的確保代碼安全的性能分析工具套件以及軟件分析、驗證、確認和編譯器技術(shù)相關(guān)咨詢服務。AbsInt產(chǎn)品廣泛地應用于、汽車、軌交、通信和能源等行業(yè)的安全苛求軟件研發(fā)過程中。

　　產(chǎn)品介紹

　　AbsInt 代碼安全性能分析套件主要包括以下幾種產(chǎn)品：

　　♦ aiT WCET Analyzer/ 差情況執(zhí)行時間分析工具

　　♦ StackAnalyzer / 差情況堆棧使用量分析工具

　　♦ TimingProfiler/ 代碼執(zhí)行時間分析工具

　　♦ Astrée /C 代碼運行時錯誤和數(shù)據(jù)競爭檢查工具

　　♦ RuleChecker/C 代碼規(guī)則檢查工具

　　♦ CompCert/ 形式化方法驗證的優(yōu)化 C 語言編譯器

　　●二進制代碼分析工具

　　♦ aiT、StackAnalyzer 和TimingProfile

　　▼ aiT針對特定的處理器和編譯器，能夠分析出接近實際運行情況的差執(zhí)行時間，真實反映系統(tǒng)性能。在分析過程中充分考慮了高速緩存和流水線（pipeline）的影響，從而避免了過于保守的WCET值，亦即避免了硬件資源的浪費

　　▼ StackAnalyzer 針對特定的處理器族和編譯器，能夠自動分析出任務的差堆棧使用量，即避免了人為低估造成的堆棧溢出，又避免了人為高估而造成的資源浪費

　　▼ TimingProfiler 針對特定的處理器族和編譯器，能夠從初期開始對代碼執(zhí)行時間進行持續(xù)分析和評估

　　● 特點

　　▼ 代碼靜態(tài)分析工具，可直接導入編譯后的 .elf/*.out 等二進制可執(zhí)行文件進行自動分析，不會對現(xiàn)有的工具鏈造成影響

　　▼ 圖形化顯示程序的調(diào)用和控制流及不同程序點的機器狀態(tài)，為優(yōu)化提供依據(jù)

　　▼ 遍歷所有程序執(zhí)行路徑，對所有場景有效，無需提供測試用例

　　▼ 支持批量測試，支持 Jenkins，可實現(xiàn)軟件持續(xù)集成測試

　　▼ aiT 和 StackAnalyzer 有認證支持包，能夠提供認證支持服務（ DO-178B, ISO-26262, IEC-61508, EN-50128 等）

　　● C 代碼分析工具

　　♦ Astrée

　　▼ Astrée能夠確保找出所有的代碼運行時錯誤(run-time error) 和數(shù)據(jù)競爭 (data race) 問題，控制流和數(shù)據(jù)流達到 的覆蓋度

　　▼ Astrée 分析方法，確保極低的誤報率

　　▼ Astrée在分析過程中能夠考慮ARINC653 OSEK AUTOSAR 等OS配置環(huán)境的影響，提高分析結(jié)果度

　　▼ Astrée的分析結(jié)果支持交互式瀏覽，能夠幫助用戶迅速定位問題，并進行備注及修改

　　▼ Astrée 可與 dSPACE TargetLink 實現(xiàn)無縫集成

　　▼ Astrée有認證支持包，能夠提供認證支持服務（DO-178B, ISO-26262, IEC-61508, EN-50128 等）

　　♦ RuleChecker

　　RuleChecker是C代碼規(guī)則檢查工具，支持以下代碼規(guī)則標準：

　　▼ MISRA 2004、2012、2012 Amendment 1

　　▼ ISO/IEC TS 17961:2013

　　▼ SEI CERT Secure C

　　▼ MITRE CWE

　　▼ 客戶訂制標準

　　恒潤科技

　　北京市海淀區(qū)知春路7號致真大廈D座6層

　　網(wǎng)址：www.hirain.com