Rapporto tecnico, 1999, ENG

Formal description and validation of an interaction policy in an object-oriented framework

Fantechi A.; Gnesi S.; Semini L.

Università di Firenze, Dipartimento di Sistemi e Informatica, Firenze, Italy; CNR-IEI, Pisa, Italy; Università di Firenze, Dipartimento di Sistemi e Informatica, Firenze, Italy

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.

Keywords

Software/program verification, Reliability, Security and protection

CNR authors

Fantechi Alessandro, Semini Laura, Gnesi Stefania

CNR institutes

ISTI – Istituto di scienza e tecnologie dell'informazione "Alessandro Faedo"

ID: 407459

Year: 1999

Type: Rapporto tecnico

Creation: 2019-10-08 10:15:51.000

Last update: 2023-03-08 13:39:23.000

External links

OAI-PMH: Dublin Core

OAI-PMH: Mods

OAI-PMH: RDF

External IDs

CNR OAI-PMH: oai:it.cnr:prodotti:407459