アセンブラのモデル検査におけるモデルの自動生成について

• Item type: SIG Technical Reports(1)
• 公開日: 2007-05-28
• タイトル: アセンブラのモデル検査におけるモデルの自動生成について
• タイトル / 言語: en
• タイトル: Automatic model generation of the assembler program for model checking
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: イーソル株式会社リサーチ＆コンサルテーションサービス部
• 著者所属: イーソル株式会社リサーチ＆コンサルテーションサービス部
• 著者所属(英): en
• 著者所属(英): Research & Consultation Services Group, eSOL Co., Ltd.
• 著者所属(英): en
• 著者所属(英): Research & Consultation Services Group, eSOL Co., Ltd.
• 著者名: 宇佐美, 雅紀; 藤倉, 俊幸
• 著者名(英): Masanori, USAMI; Toshiyuki, FUJIKURA
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: アセンブラプログラムのモデル検査についての知見と，アセンブラプログラムの検査モデルの自動生成について報告する．アセンブラプログラムのモデル検査では，CTL式を使用した到達可能性検査が有効である．また，検査モデルを正確に生成するために，モデル変換スクリプトによるモデルの半自動生成が有効である．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: This paper describes about automatic model generation of the assembler program for model checking and the finding of the model checking of the assembler program. In the model checking of the assembler program, the reachability check that used CTL (Computation Tree Logic) is effective. Moreover, the model's semiautomatic generation with the model conversion script is effective to generate the model accurately.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 情報処理学会研究報告ソフトウェア工学（SE）; 巻 2007, 号 52(2007-SE-156), p. 5-10, 発行日 2007-05-28
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会