KUPC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs

被引：1
|
作者：
Qian, Jiaqi [1 ]
Zhang, Min [1 ]
Wang, Yi [2 ]
Ogata, Kazuhiro [3 ]
机构：
[1] ECNU, Shanghai Key Lab Trustworthy Comp, Shanghai, Peoples R China
[2] Rochester Inst Technol, GCCIS, Rochester, NY 14623 USA
[3] Japan Adv Inst Sci & Technol, Nomi, Japan
来源：
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2019) | 2019年 / 11424卷
关键词：
SOFTWARE; FRAMEWORK;
D O I：
10.1007/978-3-030-16722-6_17
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Dynamic Software Updating (DSU) is a useful technique for updating running software without incurring any downtime. Its correctness must be guaranteed because updating a running software is a complicated and safety-critical process. In this paper, we present a formal tool called KupC for modeling and verifying dynamic updating of C programs. The tool is built on K-a formal semantic framework for programming languages. We formalize a patch-based dynamic updating mechanism in K based on the formal executable operational semantics of C. The formalization automatically yields an interpreter and several verification tools, which can be used to formally analyze the correctness of dynamic updating for C programs. To our knowledge, KUPC is the first formal tool for code-level verification of dynamic software updating.
引用
收藏
页码：299 / 305
页数：7
相关论文
共 50 条
  • [1] Formal modeling and verifying of FMS
    Xu, G
    Wu, ZM
    [J]. ETFA 2003: IEEE CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOL 2, PROCEEDINGS, 2003, : 315 - 320
  • [2] Formal Modeling for Verifying SCA Dynamic Composition with Event-B
    Lahouij, Aida
    Hamel, Lazhar
    Graiet, Mohamed
    [J]. 2015 IEEE 24TH INTERNATIONAL CONFERENCE ON ENABLING TECHNOLOGIES - INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES, 2015, : 29 - 34
  • [3] Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates
    Zhang, Min
    Ogata, Kazuhiro
    Futatsugi, Kokichi
    [J]. 2015 22ND ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2015), 2015, : 159 - 166
  • [4] Formal Modeling for Verifying SCA Composition
    Hamel, Lazhar
    Graiet, Mohamed
    Kmimech, Mourad
    [J]. 2015 IEEE 9TH INTERNATIONAL CONFERENCE ON RESEARCH CHALLENGES IN INFORMATION SCIENCE (RCIS), 2015, : 193 - 204
  • [5] Soft verifying dynamic features in dynamic programs
    Hou, Honglun
    Lv, Jia
    Wu, Minghui
    [J]. Information Technology Journal, 2013, 12 (24) : 8116 - 8122
  • [6] Formal Architecture Modeling of Sequential C-Programs
    Westman, Jonas
    Nyberg, Mattias
    [J]. FORMAL ASPECTS OF COMPONENT SOFTWARE, 2016, 9539 : 312 - 329
  • [7] Toward A Unified Operational Semantics-based Approach to Modeling and Verifying Dynamic Software Updating
    Qian, Jiaqi
    [J]. PROCEEDINGS OF 2018 IEEE 9TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS), 2018, : 649 - 652
  • [8] Verifying Arithmetic in Cryptographic C Programs
    Liu, Jiaxiang
    Shi, Xiaomu
    Tsai, Ming-Hsien
    Wang, Bow-Yaw
    Yang, Bo-Yin
    [J]. 34TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2019), 2019, : 564 - 576
  • [9] Verifying Parallel Programs with Dynamic Communication Structures
    Atig, Mohamed Faouzi
    Touili, Tayssir
    [J]. IMPLEMENTATION AND APPLICATION OF AUTOMATA, PROCEEDINGS, 2009, 5642 : 145 - +
  • [10] Verifying parallel programs with dynamic communication structures
    Touili, Tayssir
    Atig, Mohamed Faouzi
    [J]. THEORETICAL COMPUTER SCIENCE, 2010, 411 (38-39) : 3460 - 3468
12345