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.
1999
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - ISTI
Software/program verification
Reliability
Security and protection
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14243/391615
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact