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, Bumerdes, Algeria ' INRIA LHS-PEC, 263 Avenue Général Leclerc, 35000, Rennes, France
Abstract: Dynamic software updating (DSU) consists in updating running programs on the fly without any downtime. This feature is interesting in critical applications that must run continuously. Because updates may lead to safety errors and security breaches, the question of their correctness is raised. Formal methods are a rigorous means to ensure the correctness required by applications using DSU. In this paper, we present a formal verification of correctness of DSU in a Java-based embedded system. Our approach is based on three major contributions. First, a formal interpretation of the semantic of update operations to ensure type safety of the update. Secondly, we rely on a functional representation of bytecode, the predicate transformation calculus and a functional model of the update mechanism to ensure the behavioural correctness of the updated programs. It is based on the use of Hoare predicate transformation to derive a specification of an updated bytecode. Thirdly, we use the functional representation to model the safe update point detection mechanism. This mechanism guarantees that none of the updated methods are active. This property is called activeness safety. We propose a functional specification that allows to derive proof obligations that guarantee the safety of the mechanism.
Keywords: dynamic software updating; DSU; formal verification; weakest precondition calculus; dynamic update safety; critical systems.
International Journal of Critical Computer-Based Systems, 2017 Vol.7 No.4, pp.303 - 340
Accepted: 24 Aug 2017
Published online: 09 Feb 2018 *