JACK (the acronym for Just Another Concurrency Kit) is a workbench integrating a set of verification tools for concurrent system specifications, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment offers several functionalities to support the design, analysis and verification of systems specified using process algebras. In this paper we use JACK to formally specify the hardware components of a buffer system. Then we verify, by using the checking capabilities of JACK, the correctness of the specification with respect to some safety requirements, expressed in the action based temporal logic ACTL.
Verifying hardware components with JACK
De Nicola R.;Fantechi A.;Gnesi S.;
1995
Abstract
JACK (the acronym for Just Another Concurrency Kit) is a workbench integrating a set of verification tools for concurrent system specifications, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment offers several functionalities to support the design, analysis and verification of systems specified using process algebras. In this paper we use JACK to formally specify the hardware components of a buffer system. Then we verify, by using the checking capabilities of JACK, the correctness of the specification with respect to some safety requirements, expressed in the action based temporal logic ACTL.| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_409838-doc_144176.pdf
solo utenti autorizzati
Descrizione: Verifying hardware components with JACK
Tipologia:
Versione Editoriale (PDF)
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
2.17 MB
Formato
Adobe PDF
|
2.17 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.
