組込み制御Cプログラムのためのリソース制約の簡易モデル検査手法の提案

• Item type: SIG Technical Reports(1)
• 公開日: 2017-03-05
• タイトル: 組込み制御Cプログラムのためのリソース制約の簡易モデル検査手法の提案
• タイトル / 言語: en
• タイトル: A Simple Model Checking Method of Resource Constraints for Embedded C Programs
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: テスト
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 茨城大学
• 著者所属: 茨城大学
• 著者所属(英): en
• 著者所属(英): Ibaraki University
• 著者所属(英): en
• 著者所属(英): Ibaraki University
• 著者名: 鶴見, 昂希; 上田, 賀一
• 著者名(英): Koki, Tsurumi; Yoshikazu, Ueda
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 組込みシステムに要求される仕様として，一定時間内での処理の完了，限られたメモリ容量 ・ メモリ性能での動作の確保があり，時間制約，メモリ制約を満たすことが重要である．また，ソフトウェアの潜在的な不具合のもたらすリスクの増大により，プログラムの信頼性向上が求められ，信頼性向上の手段としてモデル検査が有用である．本研究では組込み制御Cプログラムに対して検証の前処理としてCプログラムを拡張することで制約の追加を行い，有界モデル検査ツールCBMCによってモデル検査を行うことで，厳しいリソース制約を満たしながら，プログラムの高い信頼性を実現する開発手法を提案する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: As specifications required for embedded systems, it is important to satisfy time constraints and memory constraints, such as completion of processing within a certain period of time, operation with limited memory capacity and memory performance. Also, due to the increased risk of potential problems of software, improvement of program reliability is required. Model checking is useful as a means of improving reliability. In this study, we add constraints to C program as preprocessing of verification for embedded control C program and perform model checking by CBMC bounded model checking tool. We propose a development method that realizes high reliability while satisfying stringent resource constraints.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2017-SE-195, 号 25, p. 1-8, 発行日 2017-03-05
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8825
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会