文献

J-GLOBAL ID：202002232737530751   整理番号：20A1933959

有界モデル検査に基づく並行バグ発見【JST・京大機械翻訳】

Concurrent Bug Finding Based on Bounded Model Checking

著者 (1件)： Vujosevic Janicic Milena (Faculty of Mathematics, University of Belgrade, Studentski trg 16, 11 000 Belgrade, Serbia)
資料名： International Journal of Software Engineering and Knowledge Engineering  (International Journal of Software Engineering and Knowledge Engineering)
巻： 30  号： 5  ページ： 669-694  発行年： 2020年 
JST資料番号： W0383A  ISSN： 0218-1940  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： シンガポール (SGP)  言語： 英語 (EN)

抄録/ポイント： 自動化および信頼できるソフトウェア検証は高品質ソフトウェアの開発にとって極めて重要である。形式的方法は,例えば可能な実行時間誤差を見つけるため,ソフトウェアを実行することなく,異なる種類のバグを見つけるのに使用できる。モデル検査と記号実行のような方法は,非常に正確な静的解析を提供するが,実世界プログラムは必ずしもよくはスケールしない。スケーラビリティ問題に取り組む一つの方法は,これらの種類のソフトウェア解析で使用される複雑なアルゴリズムに新しい同時および逐次アプローチを適用することである。本論文では,有界モデル検査の異なる変異体を比較し,2つの同時手法,すなわち,手続き内解析の一貫性と手続き間分析の同時性を提案した。有界モデル検査と記号実行に基づくツール,ソフトウェア検証ツールLAVにおいてこれらのアプローチを実行した。得られた改善を評価するために,標準有界モデル検査手法(全ての正しさ条件が単一化合物式に置かれる)と逐次アプローチ(そこでは,正しさ条件を別々に,他の1つ)で,同時アプローチを,実験的に比較した。結果は,多くの場合,提案した同時アプローチが顕著な改良を与えることを示した。Copyright 2020 World Scientific Publishing Company All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  自動化 ,  同時性 ,  ソフトウェア ,  *ソフトウェア障害 ,  プログラム検証 ,  *モデル検査
準シソーラス用語： 静的解析 ,  実行時間 ,  高品質 ,  *有界 , 【Automatic Indexing@JST】

著者キーワード (4件)： ソフトウェア検証 ,  自動バグ発見 ,  有界モデル検査 ,  並列および並行アプローチ

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (5件)： 有界 ,  モデル検査 ,  並行 ,  バグ ,  発見