講演抄録/キーワード |
講演名 |
2013-10-24 10:30
組込みCISCアセンブリプログラムの記号モデル検査 ○渡邊健太・チャン ヘジン・櫻井孝平・山根 智(金沢大) SS2013-36 |
抄録 |
(和) |
組込みシステムは年々大規模化・複雑化が進み,安全性・信頼性の検証はますます困難となっている.
そのため,プログラムを漏れ無く検証できる有効な検証手法として,正しさを自動的に証明できる形式的検証手法が注目されている.
本研究では,スタックオーバーフローや多重割り込みなど,ハードウェア依存の特性を持つ検証事項について有効なアセンブリプログラムの形式的検証手法を提案する. |
(英) |
The more complicated embedded systems are, the more difficult verification of safety and reliability is.
Therefore, the formal verification, which can prove rightness automatically, attracts attention as an exhaustive verification method for programs.
This research provides effective formal verification method of hardware-dependence, for example, stack overflow and multiplex interruption. |
キーワード |
(和) |
組込みシステム / マイクロコントローラ / アセンブリプログラム / モデル検査 / / / / |
(英) |
Embedded System / Microcontroller / Assembly Program / Model Checking / / / / |
文献情報 |
信学技報, vol. 113, no. 269, SS2013-36, pp. 1-5, 2013年10月. |
資料番号 |
SS2013-36 |
発行日 |
2013-10-17 (SS) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2013-36 |