Formal methods are increasingly used to validate the design of software and hardware components of safety critical systems. We describe here a case study where a formal verification method was applied in practice. As a case study we have considered a safe interaction policy between communicating objects, the Multiple Levels of Integrity policy. This policy can be seen as a communication protocol that guarantees the integrity of sensible data. Formal specification is given using a process algebra, and validation is done following a model checking approach.
Formal description and validation of an interaction policy in an object-oriented framework
Fantechi A;Gnesi S;
1999
Abstract
Formal methods are increasingly used to validate the design of software and hardware components of safety critical systems. We describe here a case study where a formal verification method was applied in practice. As a case study we have considered a safe interaction policy between communicating objects, the Multiple Levels of Integrity policy. This policy can be seen as a communication protocol that guarantees the integrity of sensible data. Formal specification is given using a process algebra, and validation is done following a model checking approach.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
prod_407459-doc_142788.pdf
accesso aperto
Descrizione: Formal description and validation of an interaction policy in an object-oriented framework
Dimensione
314.1 kB
Formato
Adobe PDF
|
314.1 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.