en fr A Formal Proof of a Unix Path Resolution Algorithm Preuve formelle dun algorithme de résolution de chemins dans Unix Report as inadecuate




en fr A Formal Proof of a Unix Path Resolution Algorithm Preuve formelle dun algorithme de résolution de chemins dans Unix - Download this document for free, or read online. Document in PDF available to download.

1 Institute of Software 2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623 3 LRI - Laboratoire de Recherche en Informatique

Abstract : In the context of file systems like those of Unix, path resolution is the operation that given acharacter string denoting an access path, determines the target object file, directory, etc. designated bythis path. This operation is not trivial because of the presence of symbolic links. Indeed, the presence ofsuch links may induce infinite loops.In this report we consider a path resolution algorithm that always terminate. We propose a formal specifi-cation of path resolution and we formally prove that our algorithm terminates on any input, and is correctand complete.

Résumé : Dans le contexte des systèmes de fichiers comme celui d’UNIX, la résolution d’un chemin estl’opération qui étant donnée une chaîne de caractère dénotant un chemin d’accès, détermine l’objet ciblefichier, répertoire, etc. désigné par ce chemin. Cette opération n’est pas triviale à cause de la présencede liens symboliques. En effet, la présence de tels liens peut induire la présence de boucles infinies.Dans ce rapport nous considérons un algorithme de résolution de chemin qui termine toujours. Nousproposons une spécification formelle de la résolution de chemins et nous prouvons formellement la ter-minaison de notre algorithme, sa correction et sa complétude.

en fr

Keywords : Formal Specification Deductive Verification Program Verifier Why3 Unix file system Path resolution

Mots-clés : résolution de chemin Système de fichier Unix environnement de preuve Why3 preuve de programmes Spécification formelle





Author: Ran Chen - Martin Clochard - Claude Marché -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents