Art

J-GLOBAL ID：201702267540802228   Reference number：17A0521668

Verification Methods of real-time properties for embedded assembly program

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

Author (1)： YAMANE SATOSHI (金沢大 大学院自然科学研究科)
Material： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
Volume： 116  Issue： 525(MSS2016 81-94)  Page： 11-16  Publication year： Mar. 09, 2017 
JST Material Number： S0532B  ISSN： 0913-5685  Document type： Proceedings
Article type： 原著論文  Country of issue： Japan (JPN)  Language： JAPANESE (JA)

Thesaurus term： *assembler ,  *real time processing ,  *model checking ,  *deduction ,  abstraction ,  *embedded system ,  program analysis ,  discrete time system ,  computation model ,  state transition diagram ,  temporal logic ,  Safety
Semi thesaurus term： 組込みアセンブリプログラム ,  リアルタイム性 ,  演繹的検証 ,  抽象化精錬 ,  state transition model ,  temporal logic

JST classification (2)： Language processors  (JD03040F) ,  Computer system development  (JD02010R)

Reference (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.

Terms in the title (7)： 組込み ,  アセンブリ ,  リアルタイム ,  検証 ,  手法 ,  モデル検査 ,  演繹