文献

J-GLOBAL ID：201702255569981520   整理番号：17A0864237

組込みアセンブリプログラムのリアルタイム安全性の演繹的検証-□_≦TIMEq⇔□(q∧(time≦TIME))-

Deductive Verification Method of real-time safety properties for embedded assembly program-□_≦TIMEq⇔□(q∧(time≦TIME))-

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

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

シソーラス用語： 組込みシステム ,  安全性 ,  演繹 ,  実時間処理 ,  ソフトウェア ,  *プログラム検証 ,  記号論理 ,  計算モデル ,  時間論理 ,  モデル ,  組込みソフトウェア
準シソーラス用語： Hoare論理 ,  線形時相論理 ,  状態遷移モデル

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

引用文献 (23件)：

• R. Jhala, R. Majumdar:Software model checking, ACM Computing Surveys (CSUR), 2009.
• C. A. R. Hoare: An Axiomatic Basis for Computer Programming, Commun. ACM 12(10), pp.576-580, 1969.
• Nikolaj Bjorner, Kenneth L. McMillan, Andrey Rybalchenko: Program Verification as Satisfiability Modulo Theories. 10th International Workshop on Satisfiability Modulo Theories(SMT 2012), pp.3-11, 2012.
• 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 Issue 3, 2008.
• Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani: Automatic Predicate Abstraction of C Programs. PLDI, pp.203-213, 2001.

タイトルに関連する用語 (6件)： 組込み ,  アセンブリ ,  リアルタイム ,  安全性 ,  演繹 ,  検証