Bounded Model Checking Technique for Interrupt-Driven Systems
Author:
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [20]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    This paper proposes an approach to model and verify a certain class of interrupt-driven aerospace control systems. These interrupt-driven systems consist of interrupt handlers and system-scheduling tasks. When an interrupt event occurs, the corresponding interrupt-handler executes in response. An interrupt-handler may leave some post-processing works to the system tasks by setting some control variables to certain values. The operating system schedules a set of tasks periodically to deal with routine tasks and some post-processing of interrupt events. In this paper, timed automata labeled with interrupts are used to model interrupt events and task scheduling events. The execution processes of interrupts are modeled by pseudo-code of interrupt handlers and the interrupt vector. Control variables are used to model the interactions between interrupt processing and system tasks while the tasks perform post-processing of interrupts according to the values of control variables set by interrupt handlers. A bounded model checking algorithm is presented in this paper to check these models w.r.t some important timing properties. The algorithm explores all feasible paths in K steps using the depth-first searching method. During the exploring process, time constraints and time requirements in the specification are calculated by the SMT solver Z3.

    Reference
    [1] Silberschatz A, Galvin PB, Gagne G. Operating System Concepts. 8th ed., Boston: Addison-Wesley Longman Publishing Co., Inc., 2008.
    [2] Walker W, Cragon HG. Interrupt processing in concurrent processors. IEEE Computer, 1995,28(6):36-46. [doi: 10.1109/2.386984]
    [3] Clarke EM, Grumberg O, Peled DA. Model Checking. Cambridge: MIT Press, 2000.
    [4] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235. [doi: 10.1016/0304-3975(94) 90010-8]
    [5] Henzinger TA. The theory of hybrid automata. In: Inan MK, Kurshan RP, eds. Verification of Digital and Hybrid Systems. 2000, 170:265-292. [doi: 10.1007/978- 3-642-59615-5_13]
    [6] Biere A, Cimatti A, Clarke E, Zhu YS. Symbolic model checking without BDDs. In: Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. LNCS 1579, Berlin, Heidelberg: Springer-Verlag, 1999. 193-207. [doi: 10.1007/3-540- 49059-0_14]
    [7] Amla N, Kurshan R, McMillan KL, Medel R. Experimental analysis of different techniques for bounded model checking. In: Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. LNCS 2619, Berlin, Heidelberg: Springer-Verlag, 2003. 34-48. [doi: 10.1007/3-540-36577-X_4]
    [8] Brylow D, Damgaard N, Palsberg J. Static checking of interrupt-driven software. In: Proc. of the 23rd Int'l Conf. on Software Engineering. IEEE, 2001. 47-56. [doi: 10.1109/ICSE.2001.919080]
    [9] Brylow D, Palsberg J. Deadline analysis of interrupt-driven software. IEEE Trans. on Software Engineering, 2004,30(10):634-655. [doi: 10.1109/TSE.2004.64]
    [10] Stoddart B, Cansell D, Zeyda F. Modeling and proof analysis of interrupt driven scheduling. In: Proc. of the Formal Specification and Development in B 2007. LNCS 4355, Berlin, Heidelberg: Springer-Verlag, 2006. 155-170. [doi: 10.1007/11955757_14]
    [11] Schlich B. Model checking of software for microcontrollers. ACM Trans. on Embedded Computing Systems, 2010,9(4):1-27. [doi: 10.1145/1721695.1721702]
    [12] Xu L. SMT-Based bounded model checking for real-time systems. In: Proc. of the 8th Int'l Conf. on Quality Software. Oxford, 2008. 120-125. [doi: 10.1109/QSIC.2008.10]
    [13] Alur R, Courcoubetis C, Dill DL. Model-Checking in dense real-time. Journal of Information and Computation, 1993,104(1):2-34. [doi: 10.1006/inco.1993.1024]
    [14] Kindermann R, Junttila TA, Niemela I. Bounded model checking of an MITL fragment for timed automata. In: Proc. of the 13th Int'l Conf. on Application of Concurrency to System Design (ACSD). 2013. 216-225. [doi: 10.1109/ACSD.2013.25]
    [15] Alur R, Feder T, Henzinger TA. The benefits of relaxing punctuality. Journal of the ACM, 1996,43(1):116-146. [doi: 10.1145/ 227595.227602]
    [16] Hou G, Zhou KJ, Chang JW, Li R, Li MC. Interrupt modeling and verification for embedded systems based on time Petri nets. In: Proc. of the 10th Int'l Symp. on Advanced Parallel Processing Technologies. LNCS 8299, Berlin, Heidelberg: Springer-Verlag, 2013. 62-76. [doi: 10.1007/978-3-642-45293-2_5]
    [17] Bouajjani A, Esparza J, Maler O. Reachability analysis of pushdown automata: Application to model-checking. In: Proc. of the CONCUR'97: Concurrency Theoy, Vol.1243. Berlin, Heidelberg: Springer-Verlag, 1997. 135-150. [doi: 10.1007/3-540-63141-0_ 10]
    [18] Jia XX, Liu C, Wu J, Liu YP, Jin MZ, Liu C. A novel Web test runner based on pushdown automation. Computer Science, 2006,33(4):269-273 (in Chinese with English abstract). [doi: 10.3969/j.issn.1002-137X.2006.04.077]
    附中文参考文献:
    [18] 贾晓霞,刘昶,吴际,柳永坡,金茂忠,刘超.一个基于下推自动机的Web测试自动执行器.计算机科学,2006,33(4):269-273. [doi: 10.3969/j.issn.1002-137X.2006.04.077]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

周筱羽,顾斌,赵建华,杨孟飞.中断驱动控制系统的有界模型检验技术.软件学报,2015,26(10):2485-2503

Copy
Share
Article Metrics
  • Abstract:2636
  • PDF: 4674
  • HTML: 1209
  • Cited by: 0
History
  • Received:July 01,2014
  • Revised:October 31,2014
  • Online: October 10,2015
You are the first2038072Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063