PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Fantechi A., Gnesi S., Ristori G. Costruzione di strumenti per sistemi concorrenti e distribuiti con la teoria. In: Sistemi informatici e calcolo parallelo, pp. 186 - 197. B. Fadini (ed.). FrancoAngeli, 1991.
 
 
Abstract
(English)
Abstract
(Italiano)
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.
Subject


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional