Simulation and Model Checking of Embedded Assembly Program

• Item type: Symposium_02(1)
• 公開日: 2016-10-13
• タイトル: Simulation and Model Checking of Embedded Assembly Program
• タイトル / 言語: en
• タイトル: Simulation and Model Checking of Embedded Assembly Program
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: モデリング，モデル検査，安全分析
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: Kanazawa University
• 著者所属: Kanazawa University
• 著者所属: Kanazawa University
• 著者所属(英): en
• 著者所属(英): Kanazawa University
• 著者所属(英): en
• 著者所属(英): Kanazawa University
• 著者所属(英): en
• 著者所属(英): Kanazawa University
• 著者名: Satoshi, Yamane; Tomonori, Kato; Ryosuke, Konoshita
• 著者名(英): Satoshi, Yamane; Tomonori, Kato; Ryosuke, Konoshita
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: It is important to ensure the safety for embedded software by software model checking. We have developed a verification system for verifying embedded assembly programs. It generates exact Kripke structure including clock cycles by exhaustively and dynamically simulating assembly programs, and simultaneously verify it by model checking in order to avoid the state space explosion. In addition, we have introduced undefined values to reduce the number of states.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: It is important to ensure the safety for embedded software by software model checking. We have developed a verification system for verifying embedded assembly programs. It generates exact Kripke structure including clock cycles by exhaustively and dynamically simulating assembly programs, and simultaneously verify it by model checking in order to avoid the state space explosion. In addition, we have introduced undefined values to reduce the number of states.
• 書誌情報: 組込みシステムシンポジウム2016論文集; 巻 2016, p. 18-26, 発行日 2016-10-13
• 出版者 / 言語: ja
• 出版者: 情報処理学会