Viene descritta un'esperienza fatta in un progetto pilota di rivalidazione- mediante specifica e verifica formale- della specifica semi-formale di un sottosistema software di controllo ferroviario.In questo progetto è stato utilizzato l'ambiente di specifica grafico/algebrica e verifica logica JACK, che integra una serie di strumenti software di specifica e verifica di sistemi concorrenti e distribuiti, offrendo un'interfaccia grafica per facilitare l'uso degli strumenti.L'esperienza effettuata ci ha permesso di concludere che il metodo formale è applicabile con successo alla verifica di sistemi reali.
Un'esperienza di specifica e verifica formale di un sottosistema di segnalamento ferroviario
Fantechi A.;Gnesi S.;
1995
Abstract
Viene descritta un'esperienza fatta in un progetto pilota di rivalidazione- mediante specifica e verifica formale- della specifica semi-formale di un sottosistema software di controllo ferroviario.In questo progetto è stato utilizzato l'ambiente di specifica grafico/algebrica e verifica logica JACK, che integra una serie di strumenti software di specifica e verifica di sistemi concorrenti e distribuiti, offrendo un'interfaccia grafica per facilitare l'uso degli strumenti.L'esperienza effettuata ci ha permesso di concludere che il metodo formale è applicabile con successo alla verifica di sistemi reali.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_409082-doc_143714.pdf
solo utenti autorizzati
Descrizione: Un'esperienza di specifica e verifica formale di un sottosistema di segnalamento ferroviario.
Tipologia:
Versione Editoriale (PDF)
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
2.82 MB
Formato
Adobe PDF
|
2.82 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.
