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).
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)
Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.