Sûreté (propriété de programme)
Pour les articles homonymes, voir Sûreté.
Cet article est une ébauche concernant la sécurité informatique.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
En informatique, notamment en méthode formelle, la sûreté (en anglais : safety) est pour un programme le fait de ne pas sortir d'un certain ensemble d'états. Notamment, on exclut la sortie d'un ensemble d'états « sûrs » (les autres indiquant des erreurs).
C'est avec la vivacité l'une des deux propriétés théoriques fondamentales des programmes informatiques.
Logique temporelle
[modifier | modifier le code]En logique temporelle linéaire (LTL), en représentant toute exécution par un mot (potentiellement infini), une propriété de sûreté est associée à des « mauvais préfixes » qui sont des mots finis qui la violent, autrement dit, tout mot commençant par un tel préfixe viole ladite propriété. On caractérise ainsi une propriété de sûreté.
Bibliographie
[modifier | modifier le code]- Rodrigues, Christian Cachin; Rachid Guerraoui; Luís (2010). Introduction to reliable and secure distributed programming (2. ed.). Berlin: Springer Berlin. (ISBN 978-3-642-15259-7)
