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
相关论文
共 50 条
  • [31] Refactoring Delta-Oriented Product Lines to Enforce Guidelines for Efficient Type-Checking
    Damiani, Ferruccio
    Lienhardt, Michael
    LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: DISCUSSION, DISSEMINATION, APPLICATIONS, ISOLA 2016, PT II, 2016, 9953 : 579 - 596
  • [32] Automatic refactoring of delta-oriented SPLs to remove-free form and replace-free form
    Ferruccio Damiani
    Michael Lienhardt
    Luca Paolini
    International Journal on Software Tools for Technology Transfer, 2019, 21 : 691 - 707
  • [33] Formal Foundations for Analyzing and Refactoring Delta-Oriented Model-Based Software Product Lines
    Pietsch, Christopher
    Kelter, Udo
    Kehrer, Timo
    Seidl, Christoph
    SPLC'19: PROCEEDINGS OF THE 23RD INTERNATIONAL SYSTEMS AND SOFTWARE PRODUCT LINE CONFERENCE, VOL A, 2020, : 207 - 217
  • [34] Fine-Grained Test Case Prioritization for Integration Testing of Delta-Oriented Software Product Lines
    Lachmann, Remo
    Lity, Sascha
    Al-Hajjaji, Mustafa
    Fuerchtegott, Franz
    Schaefer, Ina
    PROCEEDINGS OF THE 7TH INTERNATIONAL WORKSHOP ON FEATURE-ORIENTED SOFTWARE DEVELOPMENT (FOSD'16), 2016, : 1 - 10
  • [35] Automatic refactoring of delta-oriented SPLs to remove-free form and replace-free form
    Damiani, Ferruccio
    Lienhardt, Michael
    Paolini, Luca
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2019, 21 (06) : 691 - 707
  • [36] From Pairwise to Family-based Generic Analysis of Delta-oriented Model-based SPLs
    Pietsch, Christopher
    Kelter, Udo
    Kehrer, Timo
    SPLC '21: PROCEEDINGS OF THE 25TH ACM INTERNATIONAL SYSTEMS AND SOFTWARE PRODUCT LINE CONFERENCE, VOL A, 2021,
  • [37] Generating Adaptable User Interface in SPLE Using Delta-Oriented Programming and Interaction Flow Modeling Language
    Fadhlillah, Hafiyyan Sayyid
    Adianto, Daya
    Azurat, Ade
    Sakinah, Siti Ina
    SPLC'18: PROCEEDINGS OF THE 22ND INTERNATIONAL SYSTEMS AND SOFTWARE PRODUCT LINE CONFERENCE - VOL 2, 2018, : 52 - 55
  • [38] Certifying assembly programs with trails
    Wei Wang
    Frontiers of Computer Science in China, 2011, 5 : 472 - 485
  • [39] Certifying assembly programs with trails
    Wang, Wei
    FRONTIERS OF COMPUTER SCIENCE IN CHINA, 2011, 5 (04): : 472 - 485
  • [40] V4rdiac: Tooling for Multidisciplinary Delta-Oriented Variability Management in Cyber-Physical Production Systems
    Fadhlillah, Hafiyyan Sayyid
    Feichtinger, Kevin
    Bauer, Philipp
    Kutsia, Elene
    Rabiser, Rick
    26TH ACM INTERNATIONAL SYSTEMS AND SOFTWARE PRODUCT LINE CONFERENCE, SPLC 2022, VOL B, 2022, : 34 - 37
12345