You can view the full text of this article for free using the link below.

Title: Formal methods in dynamic software updating: a survey

Authors: Razika Lounas; Mohamed Mezghiche; Jean-Louis Lanet

Addresses: LIMOSE Laboratory, Faculty of Sciences, University of M'hamed Bougara of Boumerdes, Avenue de l'indépendance, 35000, Boumerdes, Algeria; Xlim Laboratory, University of Limoges, 123 Avenue Albert Thomas, 87700, Limoges, France ' LIMOSE Laboratory, Faculty of Sciences, University of M'hamed Bougara of Boumerdes, Avenue de l'indépendance, 35000, Boumerdes, Algeria ' INRIA LHS-PEC, 263 Avenue Général Leclerc, 35000, Rennes, France

Abstract: Dymanic software updating (DSU) consists in updating running programs on-the-fly without any downtime that leads to systems unavailability. The use of DSU in critical applications raises several issues related to update correctness. Indeed, an erroneous dynamic update may introduce safety vulnerabilities and security breaches. In this perspective, the use of formal methods has gained a large interest since they respond to the high need of rigor required by such applications. Several frameworks were developed to first express update correctness which is based on several criteria. Then, the proposed formalisms are used to specify DSU systems, express correctness criteria and establish them. In this paper, we present a review of researches on the application of formal methods to DSU systems. We give a classification of systems according to the paradigms of programming languages and then we explain the correctness criteria and categorise the articles regarding the approaches of formalisation to establish the correctness. This information is useful to help ongoing researches in having an overview on the application of formal methods in DSU.

Keywords: dynamic software updating; DSU; formal methods; correctness criteria; critical systems; systems safety; code update; data update; update timing; semantical correctness.

DOI: 10.1504/IJCCBS.2019.098794

International Journal of Critical Computer-Based Systems, 2019 Vol.9 No.1/2, pp.76 - 114

Accepted: 08 Jun 2018
Published online: 02 Apr 2019 *

Full-text access for editors Full-text access for subscribers Free access Comment on this article