This paper presents the rigorous validation of an integrity policy by means of the application of formal methods and related support tools for its specification and verification. The protocol which carries out the integrity policy is formally specified and formally validated, exploiting model-checking. Specific interaction patterns, which subsume the most complex interaction schemata, are considered and temporal logic formulae expressing the non-violation of integrity rules are checked on them.
Achieving fault tolerance by a formally validated interaction policy
Gnesi S;
2006
Abstract
This paper presents the rigorous validation of an integrity policy by means of the application of formal methods and related support tools for its specification and verification. The protocol which carries out the integrity policy is formally specified and formally validated, exploiting model-checking. Specific interaction patterns, which subsume the most complex interaction schemata, are considered and temporal logic formulae expressing the non-violation of integrity rules are checked on them.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_43861-doc_128152.pdf
solo utenti autorizzati
Descrizione: Achieving fault tolerance by a formally validated interaction policy
Tipologia:
Versione Editoriale (PDF)
Dimensione
489.05 kB
Formato
Adobe PDF
|
489.05 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
