Software model checking of real-time safety properties for embedded assembly program

嵌入式汇编程序实时安全特性的软件模型检查

• 批准号: 18K11239
• 负责人: Yamane Satoshi
• 金额: $ 2.66万
• 依托单位: Kanazawa University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2018
• 资助国家: 日本
• 起止时间: 2018-04-01 至 2021-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-18K11239/
• 关键词: ソフトウェアモデル検査; 組込みアセンブリプログラム; 抽象化精錬; SMT; Interpolation; 時間Kripke構造; SAT/SMT理論; 抽象化精錬(CEGAR); リアルタイム安全性

项目成果

Lazy Abstractionと精練を用いた組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査

使用惰性抽象和细化对嵌入式汇编程序进行实时软件模型检查

• 发表时间: 2020
• 期刊: 2019年冬のLAシンポジュム
• 作者: 上出広夢;山根智
• 通讯作者: 山根智

Model Checking of Real-Time Properties for Embedded Assembly Program Using Real-Time Temporal Logic RTCTL and Its Application to Real Microcontroller Software

基于实时时序逻辑RTCTL的嵌入式汇编程序实时特性模型检验及其在真实微控制器软件中的应用

• DOI: 10.1587/transinf.2019edp7172
• 发表时间: 2020
• 期刊: IEICE Transactions on Information and Systems
• 影响因子: 0.7
• 作者: Yajun Wu;Satoshi Yamane
• 通讯作者: Satoshi Yamane

Model Check of Real-time Property of Embedded Assembly Program Using CEGAR

利用CEGAR对嵌入式汇编程序实时性进行模型检验

• DOI: 10.1109/compsac.2018.00126
• 发表时间: 2018
• 期刊: 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC)
• 作者: Hiromu Kamide;Kosuke Uemura;Satoshi Yamane
• 通讯作者: Satoshi Yamane

Verification Method of Safety Properties of Embedded Assembly Program by Combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions

• DOI: 10.3390/electronics9071060
• 发表时间: 2020-06
• 期刊: Electronics
• 影响因子: 2.9
• 作者: S. Yamane;Junpei Kobashi;Kosuke Uemura

Comparative Experiment of SPIN and SMT in Model Checking of Embedded Assembly Program

SPIN与SMT在嵌入式汇编程序模型检验中的对比实验

• DOI: 10.1109/gcce50665.2020.9291772
• 发表时间: 2020
• 期刊: 2020 IEEE 9th Global Conference on Consumer Electronics (GCCE)
• 作者: Satoshi Yamane;Kosuke Uemura
• 通讯作者: Kosuke Uemura