We present an approach to the specification and verification of concurrent systems, by means of a deductive database management system. The approach is based on the synthesis of logic formulas: starting from a temporal logic formula (ACTL logic formula), that represents the requirements of a system, a general model for such formula, is derived. From this model, all the concurrent systems satisfying the formula can be generated. Moreover, we show that this model can be used to verify when a given system, obtained elsewhere, satisfies its requirements expressed by logical specifications.
Sommario non disponibile.
Specification and verification of reactive systems using a deductive database
Asirelli P;Gnesi S
1998
Abstract
We present an approach to the specification and verification of concurrent systems, by means of a deductive database management system. The approach is based on the synthesis of logic formulas: starting from a temporal logic formula (ACTL logic formula), that represents the requirements of a system, a general model for such formula, is derived. From this model, all the concurrent systems satisfying the formula can be generated. Moreover, we show that this model can be used to verify when a given system, obtained elsewhere, satisfies its requirements expressed by logical specifications.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_409732-doc_144099.pdf
accesso aperto
Descrizione: Specification and verification of reactive systems using a deductive database
Tipologia:
Versione Editoriale (PDF)
Dimensione
938.33 kB
Formato
Adobe PDF
|
938.33 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
