%0 Journal Article
%T 基于时间petri网的嵌入式系统中断建模与验证
%A 周宽久？
%A 常军旺？
%A 侯刚？
%A 任龙涛？
%A 王小龙？
%J 计算机科学
%D 2014
%R 10.11896/j.issn.1002-137X.2014.09.038
%X 嵌入式系统为中断驱动系统,但中断触发的随机性和不确定性导致中断缺陷很难被追踪发现,并且一旦发生中断故障,往往会使整个嵌入式系统陷入崩溃。因此必须保证中断系统软件的可信性,但是目前缺乏有效的中断系统资源冲突检测方法。针对上述问题,文中首先提出了一种基于时间petri网的中断系统建模方法,其能够对中断的并发性和时间序列进行有效建模。然后,为方便后续形式化验证,将时间petri网模型转化为与之等价的时间自动机模型,并提出一种符号编码方法对时间自动机进行形式化编码,将系统模型与所需验证性质编码为一阶谓词逻辑公式,从而能够通过smt对时间自动机的不变属性进行bmc验证。最后,通过smt求解器z3进行实验,实验结果证明了所提方法的有效性。
%K 中断建模
%K 有界模型检测
%K 时间自动机
%K 可满足性模理论
%K 时间petri网
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=20140938&flag=1