| 基于时间Petri网的嵌入式系统中断建模与验证 |
| |
| 引用本文： | 周宽久,常军旺,侯刚,任龙涛,王小龙. 基于时间Petri网的嵌入式系统中断建模与验证[J]. 计算机科学, 2014, 41(9): 205-209,219 |
| |
| 作者姓名： | 周宽久 常军旺 侯刚 任龙涛 王小龙 |
| |
| 作者单位： | 1. 大连理工大学软件学院 大连116620;大连理工大学软件评测中心 大连116620
2. 大连理工大学软件学院 大连116620 |
| |
| 基金项目： | 本文受国家自然科学基金:航天多核嵌入式软件可信性验证与系统原型(61272174)资助 |
| |
| 摘 要： | 嵌入式系统为中断驱动系统,但中断触发的随机性和不确定性导致中断缺陷很难被追踪发现,并且一旦发生中断故障,往往会使整个嵌入式系统陷入崩溃。因此必须保证中断系统软件的可信性,但是目前缺乏有效的中断系统资源冲突检测方法。针对上述问题,文中首先提出了一种基于时间Petri网的中断系统建模方法,其能够对中断的并发性和时间序列进行有效建模。然后,为方便后续形式化验证,将时间Petri网模型转化为与之等价的时间自动机模型,并提出一种符号编码方法对时间自动机进行形式化编码,将系统模型与所需验证性质编码为一阶谓词逻辑公式,从而能够通过SMT对时间自动机的不变属性进行BMC验证。最后,通过SMT求解器Z3进行实验,实验结果证明了所提方法的有效性。
|
| 关 键 词： | 中断建模 有界模型检测 时间自动机 可满足性模理论 时间Petri网 |
| 收稿时间： | 2013-10-12 |
| 修稿时间： | 2014-03-21 |
Interrupt Modeling and Verification for Embedded Systems Based on Time Petri Nets |
| |
| ZHOU Kuan-jiu,CHANG Jun-wang,HOU Gang,REN Long-tao and WANG Xiao-long. Interrupt Modeling and Verification for Embedded Systems Based on Time Petri Nets[J]. Computer Science, 2014, 41(9): 205-209,219 |
| |
| Authors: | ZHOU Kuan-jiu CHANG Jun-wang HOU Gang REN Long-tao WANG Xiao-long |
| |
| Affiliation: | School of Software,Dalian University of Technology,Dalian 116620,China;Software Evaluation & Test Center,Dalian University of Technology,Dalian 116620,China;School of Software,Dalian University of Technology,Dalian 116620,China;School of Software,Dalian University of Technology,Dalian 116620,China;School of Software,Dalian University of Technology,Dalian 116620,China;School of Software,Dalian University of Technology,Dalian 116620,China |
| |
| Abstract: | |
| |
| Keywords: | Interrupt modeling Bounded model checking Timed automata Satisfiability modulo theories Time petri nets |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
