文献

J-GLOBAL ID：201702267540802228   整理番号：17A0521668

組込みアセンブリプログラムのリアルタイム性の検証手法-組込みプログラムのためのモデル検査と演繹的検証-

Verification Methods of real-time properties for embedded assembly program

著者 (1件)： 山根智 (金沢大 大学院自然科学研究科)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 116  号： 525(MSS2016 81-94)  ページ： 11-16  発行年： 2017年03月09日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 組込みシステムでは,論理的正当性だけではなく,リアルタイム性の検証が重要である。本論文では,組込みプログラムのリアルタイム性の検証を目的に,以下のような離散時間のリアルタイム性を検証するモデル検査と演繹的検証の手法を提案する。(1)まず,動的プログラム解析により,組込みアセンブリプログラムから実行時間を付与した状態遷移モデルを構築する。(2)次に,状態遷移モデルを対象に,RTCTL式のモデル検査を行う。(3)次に,状態遷移モデルを対象に,RTLTL式の演繹的検証を行う。(4)最後に,モデル検査と演繹的検証の抽象化精錬検証手法を述べる。(著者抄録)

シソーラス用語： *アセンブラ ,  *実時間処理 ,  *モデル検査 ,  *演繹 ,  抽象 ,  *組込みシステム ,  プログラム解析 ,  離散時間系 ,  計算モデル ,  状態遷移図 ,  時間論理 ,  安全性
準シソーラス用語： 組込みアセンブリプログラム ,  リアルタイム性 ,  演繹的検証 ,  抽象化精錬 ,  状態遷移モデル ,  時相論理

分類 (2件)： 言語プロセッサ  (JD03040F) ,  計算機システム開発  (JD02010R)

引用文献 (20件)：

• R Jhala, R Majumdar:Software model checking, ACM Com-puting Surveys (CSUR), 2009.
• R Wilhelm, et-al.:The worst-case execution-time problem-overview of methods and survey of tools, ACM Transactions on Embedded Computing Systems (TECS), Volume 7 Issue3, 2008.
• Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani : Automatic Predicate Abstraction of C Pro-grams. PLDI, pp.203-213, 2001.
• Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Gregoire Sutre : Lazy abstraction. POPL, pp.58-70, 2002.
• Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith : Modular Verification of Software Compo-nents in C. IEEE Trans. Software Eng. 30(6), pp.388-402, 2004.

タイトルに関連する用語 (7件)： 組込み ,  アセンブリ ,  リアルタイム ,  検証 ,  手法 ,  モデル検査 ,  演繹