Strumenti Utente

Strumenti Sito


db:verifica_formale

Verifica formale

Approfondimenti

Info

Quest'argomento non è collegato ad altri approfondimenti correlati. Si consiglia, in ogni caso, di controllare sempre [ l'Indice ] degli Approfondimenti

Questa pagina è solo improntata in attesa di completamento da parte dei Collaboratori. Se sei interessato a collaborare attivamente con Extrapedia, leggi come fare [ Collabora ]

Nel contesto dei sistemi hardware e software, la Verifica formale è l'atto di dimostrare o confutare la correttezza degli Algoritmi previsti alla base di un sistema rispetto a determinate specifiche o proprietà formali, usando Metodi formali di Matematica. 1)

La Verifica formale può essere utile per dimostrare la correttezza di sistemi quali: protocolli crittografici, circuiti combinatori, circuiti digitali con memoria interna e software espressi come codice sorgente.

La verifica di questi sistemi è effettuata fornendo una prova formale su un modello matematico astratto del sistema, la corrispondenza tra il modello matematico e la natura del sistema che altrimenti sarebbe nota per costruzione. Esempi di oggetti matematici spesso usati per modellare sistemi sono: macchine a stati finiti, sistemi di transizione etichettati, reti di Petri, sistemi di aggiunta vettoriale, automi temporizzati, automi ibridi, algebra di processo, semantica formale di Linguaggi di programmazione come semantica operazionale, semantica denotazionale, semantica assiomatica e logica di Hoare.


Qualora alcuni link non funzionassero, si prega di comunicarlo allo Staff - staff@extrapedia.org


1)
Alok Sanghavi (21 maggio 2010) - “Che cos'è la verifica formale?”
db/verifica_formale.txt · Ultima modifica: 13/04/2019 16:09 (modifica esterna)