Art

J-GLOBAL ID：201702255569981520   Reference number：17A0864237

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

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

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

Thesaurus term： embedded system ,  Safety ,  deduction ,  real time processing ,  software ,  *program verification ,  symbolic logic ,  computation model ,  temporal logic ,  model ,  embedded software
Semi thesaurus term： Hoare logic ,  linear temporal logic ,  state transition model

JST classification (1)： Computer system development  (JD02010R)

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

Terms in the title (6)： 組込み ,  アセンブリ ,  リアルタイム ,  安全性 ,  演繹 ,  検証