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:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
