user

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 条
  • [31] TRICERA: Verifying C Programs Using the Theory of Heaps
    Esen, Zafer
    Rummer, Philipp
    [J]. 2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD, 2022, 3 : 380 - 391
  • [32] A tool for a formal pattern modeling language
    Kim, Soon-Kyeong
    Carrington, David
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 4260 : 568 - +
  • [33] Formal Behavioral Modeling for Verifying SCA Composition with Event-B
    Graiet, Mohamed
    Lahouij, Aida
    Abbassi, Imed
    Hamel, Lazhar
    Kmimech, Mourad
    [J]. 2015 IEEE INTERNATIONAL CONFERENCE ON WEB SERVICES (ICWS), 2015, : 17 - 24
  • [34] A tool for a formal pattern modeling language
    Kim, Soon-Kyeong
    Carrington, David
    [J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2006, 4260 LNCS : 568 - 587
  • [35] An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms
    Zhang, Min
    Ogata, Kazuhiro
    Futatsugi, Kokichi
    [J]. 2012 19TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), VOL 1, 2012, : 664 - 673
  • [36] PYRELOAD: Dynamic Updating of Python']Python Programs by Reloading
    Tang, Wei
    Zhang, Min
    [J]. 2018 25TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2018), 2018, : 229 - 238
  • [37] A CEGAR-Based Static-Dynamic Approach to Verifying Full Regular Properties of C Programs
    Yang, Kai
    Tian, Cong
    Zhang, Nan
    Duan, Zhenhua
    Du, Hongwei
    [J]. IEEE TRANSACTIONS ON RELIABILITY, 2021, 70 (04) : 1455 - 1467
  • [38] A Formal Modeling Tool for Exploratory Modeling in Software Development
    Oda, Tomohiro
    Araki, Keijiro
    Larsen, Peter Gorm
    [J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2017, E100D (06): : 1210 - 1217
  • [39] Verifying C plus plus Dynamic Binding
    Mommen, Niels
    Jacobs, Bart
    [J]. PROCEEDINGS OF THE 25TH ACM INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS, FTFJP 2023, 2023, : 1 - 7
  • [40] A Categorical Approach for Modeling and Verifying Dynamic Software Architecture
    Ling, Xiang
    [J]. 2013 IEEE 7TH INTERNATIONAL CONFERENCE ON SOFTWARE SECURITY AND RELIABILITY - COMPANION (SERE-C), 2013, : 169 - 176
12345