|
Depot Institutionnel de l'UMBB >
Publications Scientifiques >
Publications Internationales >
Veuillez utiliser cette adresse pour citer ce document :
http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/5327
|
| Titre: | A formal verification of dynamic updating in a Java-based embedded system |
| Auteur(s): | Lounas, Razika
Mezghiche, Mohamed
Lanet, Jean-Louis |
| Mots-clés: | Dynamic software updating
Formal verification
Weakest precondition calculus
Dynamic update safety
Critical systems |
| Date de publication: | 2017 |
| Editeur: | Inderscience |
| Collection/Numéro: | International Journal of Critical Computer-Based Systems/ Vol.7, N°4 (2017); pp. 303-340 |
| Résumé: | 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 |
| URI/URL: | http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/5327 |
| ISSN: | 1757-8779 |
| Collection(s) : | Publications Internationales
|
Fichier(s) constituant ce document :
|
Tous les documents dans DSpace sont protégés par copyright, avec tous droits réservés.
|
