A Denotational Model for Interrupt-Driven Programs

被引：1
|
作者：
Huang, Yanhong [1 ]
Zhao, Yongxin [2 ]
Shi, Jianqi [2 ]
Zhu, Huibiao [1 ]
机构：
[1] East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China
[2] Natl Univ Singapore, Sch Comp, Singapore, Singapore
来源：
IEEE SIXTH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS (ICSTW 2013) | 2013年
基金：
国家高技术研究发展计划(863计划); 新加坡国家研究基金会; 中国国家自然科学基金;
关键词：
time; interrupt; denotational semantics;
D O I：
10.1109/ICSTW.2013.9
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
In design of dependable software for real-time embedded systems, the interrupt mechanism plays an important role. Due to the randomicity and nondeterminism of interrupt handling behaviors, the analysis about program behaviors as well as time properties is an important but challenging problem. In a previous work, we presented a small but expressive language for interrupt-driven programs, and suggested a timed operational semantics to specify the meaning of the programs. In this paper, we explore a denotational semantics under a discrete time model for the interrupt-driven programming language. It can deal with the features of the language. We also define a transition which can link the operational semantics and denotational semantics.
引用
收藏
页码：15 / 20
页数：6
相关论文
共 50 条
  • [1] Static race detection of interrupt-driven programs
    Huo, Wei
    Yu, Hongtao
    Feng, Xiaobing
    Zhang, Zhaoqing
    [J]. Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2011, 48 (12): : 2290 - 2299
  • [2] Stack size analysis for interrupt-driven programs
    Chatterjee, K
    Ma, D
    Majumdar, R
    Zhao, T
    Henzinger, TA
    Palsberg, J
    [J]. INFORMATION AND COMPUTATION, 2004, 194 (02) : 144 - 174
  • [3] Stack size analysis for interrupt-driven programs
    Chatterjee, K
    Ma, D
    Majumdar, R
    Zhao, T
    Henzinger, TA
    Palsberg, J
    [J]. STATIC ANALYSIS, PROCEEDINGS, 2003, 2694 : 109 - 126
  • [4] Analyzing and Disentangling Interleaved Interrupt-Driven IoT Programs
    Sun, Yuxia
    Guo, Song
    Cheung, Shing-Chi
    Tang, Yong
    [J]. IEEE INTERNET OF THINGS JOURNAL, 2019, 6 (03) : 5376 - 5386
  • [5] Data Race Detection for Interrupt-Driven Programs via Bounded Model Checking
    Wu, Xueguang
    Wen, Yanjun
    Chen, Liqian
    Dong, Wei
    Wang, Ji
    [J]. 2013 IEEE 7TH INTERNATIONAL CONFERENCE ON SOFTWARE SECURITY AND RELIABILITY - COMPANION (SERE-C), 2013, : 205 - 211
  • [6] Model checking technique for interrupt-driven system
    Zhou, Xiao-Yu
    Gu, Bin
    Zhao, Jian-Hua
    Yang, Meng-Fei
    Li, Xuan-Dong
    [J]. Ruan Jian Xue Bao/Journal of Software, 2015, 26 (09): : 2212 - 2230
  • [7] Disclosing and Locating Concurrency Bugs of Interrupt-Driven IoT Programs
    Sun, Yuxia
    Cheung, Shing-Chi
    Guo, Song
    Cheng, Ming
    [J]. IEEE INTERNET OF THINGS JOURNAL, 2019, 6 (05): : 8945 - 8957
  • [8] Numerical Static Analysis of Interrupt-Driven Programs via Sequentialization
    Wu, Xueguang
    Chen, Liqian
    Mine, Antoine
    Dong, Wei
    Wang, Ji
    [J]. 2015 PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE (EMSOFT), 2015, : 55 - 64
  • [9] Bounded model checking technique for interrupt-driven systems
    State Key Laboratory for Novel Software Technology , Nanjing
    210023, China
    不详
    210093, China
    不详
    710072, China
    不详
    210023, China
    不详
    100094, China
    [J]. Ruan Jian Xue Bao, 10 (2485-2503):
  • [10] Static Analysis of Runtime Errors in Interrupt-Driven Programs via Sequentialization
    Wu, Xueguang
    Chen, Liqian
    Mine, Antoine
    Dong, Wei
    Wang, Ji
    [J]. ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2016, 15 (04)
12345