计算机科学 ›› 2014, Vol. 41 ›› Issue (9): 205-209.doi: 10.11896/j.issn.1002-137X.2014.09.038
周宽久,常军旺,侯刚,任龙涛,王小龙
ZHOU Kuan-jiu,CHANG Jun-wang,HOU Gang,REN Long-tao and WANG Xiao-long
摘要： 嵌入式系统为中断驱动系统,但中断触发的随机性和不确定性导致中断缺陷很难被追踪发现,并且一旦发生中断故障,往往会使整个嵌入式系统陷入崩溃。因此必须保证中断系统软件的可信性,但是目前缺乏有效的中断系统资源冲突检测方法。针对上述问题,文中首先提出了一种基于时间Petri网的中断系统建模方法,其能够对中断的并发性和时间序列进行有效建模。然后,为方便后续形式化验证,将时间Petri网模型转化为与之等价的时间自动机模型,并提出一种符号编码方法对时间自动机进行形式化编码,将系统模型与所需验证性质编码为一阶谓词逻辑公式,从而能够通过SMT对时间自动机的不变属性进行BMC验证。最后,通过SMT求解器Z3进行实验,实验结果证明了所提方法的有效性。
| [1] Rammig F,Rust C．Modeling of dynamically modifiable embedded real-time systems[C]∥The Ninth IEEE International Workshop on Object-Oriented Real-Time Dependable Systems,2003(WORDS 2003 Fall)．IEEE,2003:28-28 [2] Gu Z,Shin K G．An integrated approach to modeling and analysis of embedded real-time systems based on timed petri nets[C]∥Proceedings 23rd International Conference on Distributed Computing Systems,2003．IEEE,2003:350-359 [3] Costa A,Gomes L．Petri net splitting operation within embedded systems co-design[C]∥2007 5th IEEE International Conference on Industrial Informatics．IEEE,2007,1:503-508 [4] Zhang H,Ai Y．Schedule modeling based on Petri nets for distributedreal-time embedded systems[J]．Jisuanji Gongcheng/ Computer Engineering,2006,32(18):6-8 [5] Merlin P M．A study of the recoverability of computing systems [D]．University of California,Irvine,1974 [6] Cassez F,Roux O H．Structural translation from time Petri nets to timed automata[J]．Journal of Systems and Software,2006,79(10):1456-1468 [7] Lime D,Roux O H．Model checking of time Petri nets using the state class timed automaton[J]．Discrete Event Dynamic Systems,2006,16(2):179-205 [8] Guoyin Z,Ming L,Aihong Y,et al.Methodology of modeling and formal verification based on extended Petri net[J]．Applicaiton Research of Computers,2010,27 [9] Alur R．Timed automata[C]∥Computer Aided Verification．Springer Berlin Heidelberg,1999:8-22 [10] Barrett C,Sebastiani R,Seshia S,et al.Handbook of Satisfiability [M]．Fairfax:IOS Press,2009 [11] Biere A,Cimatti A,Clarke E,et al．Symbolic model checking without BDDs[M]．Springer Berlin Heidelberg,1999 [12] Veanes M,Bjrner N,Raschke A．An SMT approach to bounded reachability analysis of model programs[M]∥Formal Techniques for Networked and Distributed Systems-FORTE 2008．Springer Berlin Heidelberg,2008:53-68 [13] Wang Xiao-liang．Bounded model checking of timed automatabased on Yices[J]．Computer Engineering and Design,2010,31(1):126-129 [14] Weiqiang K,Shiraishi T,Katahira N,et al．An SMT-Based Approach to Bounded Model Checking of Designs in State Transition Matrix[J]．IEICE transactions on information and systems,2011,94(5):946-957 [15] Barrett C,De Moura L,Stump A．Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)[J]．Journal of Automated Reasoning,2005,35(4):373-390 [16] Le Berre D,Simon L．The essentials of the SAT 2003 competition[C]∥Theory and Applications of Satisfiability Testing．Springer Berlin Heidelberg,2004:452-467 |
| No related articles found! |
|
||
首页