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
基金
欧盟地平线“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 条
  • [1] Albert E, 2006, REDUCED CERTIFICATES, P163
  • [2] [Anonymous], 1976, ICSE 76
  • [3] Apel S., 2016, Feature-oriented software product lines
  • [4] Arndt J, 2006, TECHNICAL REPORT
  • [5] Ayavoo D, 2005, LECT NOTES COMPUT SC, V3555, P167
  • [6] Bailey J. W., 1981, 5th International Conference on Software Engineering, P107
  • [7] Basili V. R., 1975, IEEE Transactions on Software Engineering, VSE-1, P390, DOI 10.1109/TSE.1975.6312870
  • [8] A METHODOLOGY FOR COLLECTING VALID SOFTWARE ENGINEERING DATA
    BASILI, VR
    WEISS, DM
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1984, 10 (06) : 728 - 738
  • [9] EXPERIMENTATION IN SOFTWARE ENGINEERING
    BASILI, VR
    SELBY, RW
    HUTCHENS, DH
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1986, 12 (07) : 733 - 743
  • [10] Scaling step-wise refinement
    Batory, D
    Sarvela, JN
    Rauschmayer, A
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2004, 30 (06) : 355 - 371