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
基金
国家高技术研究发展计划(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 条
  • [21] Data Races and Static Analysis for Interrupt-Driven Kernels
    Chopra, Nikita
    Pai, Rekha
    D'Souza, Deepak
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2019: 28TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2019, 11423 : 697 - 723
  • [22] INTERRUPT-DRIVEN MICROPROCESSOR-BASED OVERCURRENT RELAY
    MANZOUL, MA
    [J]. IEEE TRANSACTIONS ON INDUSTRIAL ELECTRONICS, 1991, 38 (01) : 8 - 9
  • [23] INTERRUPT-DRIVEN DIGITAL CONTROLLER FOR A MAGNETIC SUSPENSION SYSTEM
    LAWSON, MA
    GILLIES, GT
    [J]. REVIEW OF SCIENTIFIC INSTRUMENTS, 1989, 60 (03): : 456 - 466
  • [24] Precise and Efficient Atomicity Violation Detection for Interrupt-Driven Programs via Staged Path Pruning
    Li, Chao
    Chen, Rui
    Wang, Boxiang
    Yu, Tingting
    Gao, Dongdong
    Yang, Mengfei
    [J]. PROCEEDINGS OF THE 31ST ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, ISSTA 2022, 2022, : 506 - 518
  • [25] Performance evaluation of interrupt-driven kernels in gigabit networks
    Salah, K
    El-Badawi, K
    [J]. GLOBECOM'03: IEEE GLOBAL TELECOMMUNICATIONS CONFERENCE, VOLS 1-7, 2003, : 3953 - 3957
  • [26] DESIGNING WITH MICROPROCESSORS .8. INTERRUPT-DRIVEN CIRCUITS
    ZISSOS, D
    [J]. WIRELESS WORLD, 1981, 87 (1545): : 37 - 39
  • [27] iDola: Bridge Modeling to Verification and Implementation of Interrupt-driven Systems
    Liu, Han
    Zhang, Hehua
    Jiang, Yu
    Song, Xiaoyu
    Gu, Ming
    Sun, Jiaguang
    [J]. 2014 THEORETICAL ASPECTS OF SOFTWARE ENGINEERING CONFERENCE (TASE), 2014, : 193 - 200
  • [28] Atomicity Violation Detection for Interrupt-Driven Aerospace Embedded Software
    Yu T.
    Li C.
    Wang B.
    Chen R.
    Jiang Y.
    [J]. Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2023, 60 (02): : 294 - 310
  • [29] Automatic test solution for interrupt-driven based embedded software
    Mei Gong
    Yue Wu
    [J]. PROCEEDINGS OF THE INTERNATIONAL CONFERENCE INFORMATION COMPUTING AND AUTOMATION, VOLS 1-3, 2008, : 1517 - +
  • [30] DESIGNING WITH MICROPROCESSORS .9. MORE ON INTERRUPT-DRIVEN CIRCUITS
    ZISSOS, D
    STONE, G
    [J]. WIRELESS WORLD, 1981, 87 (1546): : 77 - 80