Sûreté (propriété de programme)
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).
Pour les articles homonymes, voir Sûreté.
C'est avec la vivacité l'une des deux propriétés théoriques fondamentales des programmes informatiques.
Logique temporelle
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
- 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)
Portail de l’informatique 
Portail de la sécurité informatique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.