文献

J-GLOBAL ID：202102222607400217   整理番号：21A0153120

Recker:割込み駆動プログラムのためのCBMCベースのデータ競合検出器【JST・京大機械翻訳】

Rchecker: A CBMC-based Data Race Detector for Interrupt-driven Programs

著者 (5件)： Feng Haining (Key Laboratory of Software Engineering for Complex Systems, National University of Defense Technology,Changsha,China) ,  Yin Liangze (Key Laboratory of Software Engineering for Complex Systems, National University of Defense Technology,Changsha,China) ,  Lin Wenfeng (China Academy of Engineering Physics,Mianyang,China) ,  Zhao Xudong (Key Laboratory of Software Engineering for Complex Systems, National University of Defense Technology,Changsha,China) ,  Dong Wei (Key Laboratory of Software Engineering for Complex Systems, National University of Defense Technology,Changsha,China)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2020  号： QRS-C  ページ： 465-471  発行年： 2020年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 中断駆動プログラムは,航空宇宙,医療機器,および極端な安全性と安定性を必要とする他の組込みシステムに広く使用されている。しかし,不確かな割込みインタリービング実行は,重大なデータレース問題を引き起こすかもしれない。静的解析は,データレース問題を検出する重要な技術である。既存の方法は,低い精度を持つか,または多くの誤り警報をもたらすのに保守的であり,さらに,より効果的な解決策を必要とする。プログラム検証ツールCBMCは,Cマルチスレッドモデリングの解析と検証において優れた性能を有するが,それは,中断駆動プログラムを支持しなかった。本論文では,中断駆動プログラムにおけるデータレースを検出するためにCBMCに基づく方法を提案した。提案手法は,割込みプリエンプションと同期意味論に対する解析を行うことにより,割込み駆動プログラムの正確な解析を達成し,プログラムのさらなる検証をサポートできる。関連するベンチマークに関する実験結果は,著者らのアプローチの有用性と有効性を実証した。Copyright 2021 The Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 意味論 ,  保全 ,  *インタリービング ,  検出器 ,  プログラム検証 ,  有効性 ,  ベンチマーク ,  組込みシステム
準シソーラス用語： 静的解析 ,  誤警報 ,  プリエンプション ,  航空宇宙 ,  *データ競合 , 【Automatic Indexing@JST】

分類 (1件)： 図形・画像処理一般  (JE04010I)

タイトルに関連する用語 (3件)： 割込み ,  データ競合 ,  検出器