Certifying delta-oriented programs

被引：2
作者：
Rodrigues, Vitor [1 ]
Donetti, Simone [2 ]
Damiani, Ferruccio [2 ]
机构：
[1] Univ Turin, Turin, Italy
[2] Univ Turin, Comp Sci Dept, Turin, Italy
来源：
SOFTWARE AND SYSTEMS MODELING | 2019年 / 18卷 / 05期
基金：
欧盟地平线“2020”;
关键词：
Model-driven development; Delta-oriented programming; Safety properties; Proof-carrying code; Runtime systems; SOFTWARE; TIME; ARCHITECTURE; FRAMEWORK; CHECKING;
D O I：
10.1007/s10270-018-00704-x
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
A major design concern in modern software development frameworks is to ensure that mechanisms for updating code running on remote devices comply with given safety specifications. This paper presents a delta-oriented approach for implementing product lines where software reuse is achieved at the three levels of state-diagram modeling, C/C++source code and binary code. A safety specification is expressed on the properties of reusable software libraries that can be dynamically loaded at run time after an over-the-air update. The compilation of delta-engineered code is certified using the framework of proof-carrying code in order to guarantee safety of software updates on remote devices. An empirical evaluation of the computational cost associated with formal safety checks is done by means of experimentation.
引用
收藏
页码：2875 / 2906
页数：32
相关论文
共 89 条
  • [61] Parkes AP, 2008, FINITE STATE TRANSDU, P189
  • [62] PERCIVAL C, 2006, THESIS
  • [63] Pohl K., 2005, SOFTWARE PRODUCT LIN, V10, DOI 10.1007/3-540-28901-1
  • [64] Raistrick Chris., 2004, MODEL DRIVEN ARCHITE
  • [65] FLOWCHARTS VERSUS PROGRAM DESIGN LANGUAGES - AN EXPERIMENTAL COMPARISON
    RAMSEY, HR
    ATWOOD, ME
    VANDOREN, JR
    [J]. COMMUNICATIONS OF THE ACM, 1983, 26 (06) : 445 - 449
  • [66] Rodrigues V., 2008, P FOR CAISE 08 C MON, P29
  • [67] Certifying execution time in multicores
    Rodrigues, Vitor
    Akesson, Benny
    Florido, Mario
    de Sousa, Simao Melo
    Pedroso, Joao Pedro
    Vasconcelos, Pedro
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2015, 111 : 505 - 534
  • [68] ROst T. B., 2018, ADV SERVICE ORIENTED, V824, P159, DOI [10.1007/978-3-319-79090-9_12, DOI 10.1007/978-3-319-79090-9_12]
  • [69] Rumbaugh J, 2004, UNIFIED MODELING LAN, P2
  • [70] Schaefer I., 2012, International Journal on Software Tools for Technology Transfer (STTT), V14, P477, DOI DOI 10.1007/S10009-012-0253-Y
123456789