Computer Science ›› 2014, Vol. 41 ›› Issue (9): 205-209.doi: 10.11896/j.issn.1002-137X.2014.09.038

Previous Articles     Next Articles

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   

  • Online:2018-11-14 Published:2018-11-14

Abstract: The embedded systems are interrupt-driven systems,but the triggered methods of interrupts are with randomness and uncertainty.The behavior of interrupt can be quite difficult to fully understand,and many catastrophic system failures are caused by unexpected behaviors.Therefore,interrupt-driven systems need high quality tests,but there is a lack of effective interrupt system detection methods at present.In this paper,firstly a modeling method of interrupt system was proposed based on time Petri nets,which has ability of describing concurrency and time series.Then the time Petri nets were transformed into timed automata for model checking.Consequentially,a symbolic encoding approach was investigated for formalized timed automata,through which the timed automata could be bounded model checked (BMC) with regard to invariant properties by using Satisfiability Modulo Theories (SMT) solving technique.Finally,Z3 was used in the experiments to evaluate the effectiveness of our approach.

Key words: Interrupt modeling,Bounded model checking,Timed automata,Satisfiability modulo theories,Time petri nets

[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,Bjrner 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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!