信息科学与工程学院机构知识库

Institutional Repository, School of Information Science and Engineering

 

兰州大学机构库  > 信息科学与工程学院  > 会议论文
题名: Verifying OSEK/VDX applications: An optimized SMT-based bounded model checking approach
作者: Zhang, Haitao; Cheng, Zhuo; Tian, Cong; Lu, Yonggang; Li, Guoqiang
收录类别: EI
出版日期: 2016-08-23
会议名称: 15th IEEE/ACIS International Conference on Computer and Information Science, ICIS 2016
会议日期: June 26, 2016 - June 29, 2016
会议地点: Okayama, Japan
英文摘要: OSEK/VDX, a standard of automobile OS, has been widely adopted by many manufacturers to design and implement a vehicle-mounted OS. Currently, with increasing functionalities in vehicles, more and more complex applications are developed based on the OSEK/VDX OS. However, how to ensure the reliability of developed applications is becoming a challenge for developers. Based on our previous work, in this paper we present an efficient approach to verify the developed OSEK/VDX applications. In the presented approach, SMT-based bounded model checking technique is used to carry out verification in order to handle complex applications. Moreover, a series of optimization strategies are proposed and employed to improve the checking capability of our approach. We have implemented a tool according to the proposed approach and conducted many experiments. The experiment results show that our approach is capable of checking the safety property of large-scale OSEK/VDX applications. We also compared our approach with existing checking method, the comparison results indicate that our approach is an efficient and powerful technique in verifying OSEK/VDX applications. © 2016 IEEE.
关键词: Model checking ; Automobile manufacture ; Information science ; Surface mount technology ; Bounded model checking ; Comparison result ; Complex applications ; Design and implements ; Deterministic Scheduler ; Developed applications ; Optimization strategy ; Safety property
作者部门: (1) School of Information Science and Engineering, Lanzhou University, China ; (2) School of Information Science, Japan Advanced Institute of Science and Technology, Japan ; (3) ICTT and ISN Laboratory, Xidian University, China ; (4) School of Software, Shanghai Jiao Tong University, China
通讯作者: Cheng, Zhuo (chengzhuo@jaist.ac.jp)
学科分类: Automobiles;Computer Theory, Includes Formal Logic, Automata Theory, Switching Theory, Programming Theory
会议录: 2016 IEEE/ACIS 15th International Conference on Computer and Information Science, ICIS 2016 - Proceedings
出版者: IEEE
语种: 英语
DOI: 10.1109/ICIS.2016.7550826
EI记录号: 20163902832447
IR记录号: 20163902832447
第一机构:
Citation statistics:
内容类型: 会议论文
URI标识: http://ir.lzu.edu.cn/handle/262010/184030
Appears in Collections:信息科学与工程学院_会议论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
Zhang, Haitao,Cheng, Zhuo,Tian, Cong,et al. Verifying OSEK/VDX applications: An optimized SMT-based bounded model checking approach[C]. 见:15th IEEE/ACIS International Conference on Computer and Information Science, ICIS 2016. Okayama, Japan. June 26, 2016 - June 29, 2016.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Altmetrics Score
 
Google Scholar
Similar articles in Google Scholar
[Zhang, Haitao]'s Articles
[Cheng, Zhuo]'s Articles
[Tian, Cong]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Zhang, Haitao]‘s Articles
[Cheng, Zhuo]‘s Articles
[Tian, Cong]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Email:
Passwd
验 证:
换一张
Have you forgotten your password? Log In
Copyright © 2007-2017  兰州大学 - Feedback
Powered by CSpace