An Approach For Formal Verification Of Updated Java Bytecode Programs
Résumé: This paper deals with formal specification and verification of Java bytecode update. Programs update for Java applications has gained a wide interest since it is used for several purposes: transforming semantics of a program, adding features to a program or performing optimizations. In this paper, we focus on program transformations for Java programs at the bytecode level. Because these transformations may introduce errors, our goal is to provide a formal way to verify the update and establish its correctness. Our approach for formal specification and verification of updated Java bytecode programs is based on four ingredients: a formal interpretation of the semantics of update operations, a functional representation of bytecode, bytecode annotation and predicate transformation calculus.We use the concept of Hoare predicate transformation to derive a specification of an annotated bytecode. Annotations are used to express update operations within the code. A functional representation is used to model annotations and bytecode. The approach derives then a new specification for the annotated bytecode using a weakest precondition calculus defined to deal with update operations. Verification conditions are then generated and proved to establish the correction of the update
Mots-clès:
Nos services universitaires et académiques
Thèses-Algérie vous propose ses divers services d’édition: mise en page, révision, correction, traduction, analyse du plagiat, ainsi que la réalisation des supports graphiques et de présentation (Slideshows).
Obtenez dès à présent et en toute facilité votre devis gratuit et une estimation de la durée de réalisation et bénéficiez d'une qualité de travail irréprochable et d'un temps de livraison imbattable!
Aucun fichier associé
Si le fichier est volumineux, l'affichage peut échouer. Vous pouvez obtenir le fichier directement en cliquant sur le bouton "Télécharger".
