In questo lavoro viene descritto un sistema che permette di provare sia proprietà comportamentali che logiche di sistemi concorrenti specificati con algebre di processo e con una logica delle azioni chiamata ACTL. Il sistema è stato realizzato integrando due strumenti esistenti, AUTO e EMC. Il primo costruisce Sistemi di Transizione Etichettati con azioni, a partire da un termine dell'algebra di processo, il secondo verifica la validità di formule CTL su macchine a stati finiti (Strutture di Kripke). I due strumenti vengono integrati implementando due funzioni di traduzione; la prima trasforma formule ACTL in formule CTL, la seconda trasforma Sistemi di Transizione Etichettati in Strutture di Kripke. La correttezza dell'integrazione segue dal fatto che le funzioni di traduzione preservano la soddisfacibilità delle formule logiche.
Costruzione di strumenti per sistemi concorrenti e distribuiti con la teoria
De Nicola R;Fantechi A;Gnesi S;
1991
Abstract
In questo lavoro viene descritto un sistema che permette di provare sia proprietà comportamentali che logiche di sistemi concorrenti specificati con algebre di processo e con una logica delle azioni chiamata ACTL. Il sistema è stato realizzato integrando due strumenti esistenti, AUTO e EMC. Il primo costruisce Sistemi di Transizione Etichettati con azioni, a partire da un termine dell'algebra di processo, il secondo verifica la validità di formule CTL su macchine a stati finiti (Strutture di Kripke). I due strumenti vengono integrati implementando due funzioni di traduzione; la prima trasforma formule ACTL in formule CTL, la seconda trasforma Sistemi di Transizione Etichettati in Strutture di Kripke. La correttezza dell'integrazione segue dal fatto che le funzioni di traduzione preservano la soddisfacibilità delle formule logiche.File | Dimensione | Formato | |
---|---|---|---|
prod_447263-doc_161165.pdf
solo utenti autorizzati
Descrizione: Costruzione di strumenti per sistemi concorrenti e distribuiti con la teoria
Tipologia:
Versione Editoriale (PDF)
Dimensione
2.44 MB
Formato
Adobe PDF
|
2.44 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.