L’attività riportata nel documento riguarda una Metodologia di specificazione e analisi di strategie di recupero delle anomalie per il controllo dei processi industriali. Il compito della Metodologia è di guidare l’analista di un’applicazione di automazione nel processo di specificazione/analisi dei requisiti che garantiscono all’applicazione di sopravvivere e continuare a funzionare in presenza di avversità, di varia natura e origine, che colpiscono i componenti dell’infrastruttura di informazione e comunicazione. Coerentemente con quanto indicato dagli standard di settore quali [IEC 61508, 1997] e [IEC60300, 2001], la Metodologia proposta è costituita da tre Schemi per la dependability che utilizzano tre formalismi diversi di specifica/analisi: il paradigma statico dei diagrammi classe della notazione standard UML [UML, 2003], la logica temporale TRIO [TRIO, 2000] e il paradigma operazionale delle Reti di Petri Stocastiche SPN [Molloy, 1982] storicamente più usato per la valutazione delle prestazioni e della dependability. Lo Schema UML costituisce il livello di ingresso della Metodologia e consiste in un insieme predefinito di diagrammi classe specifici per il dominio dei sistemi di automazione, e delle linee guida che indicano come applicare lo Schema generico ad un caso specifico. I diagrammi classe dello Schema vengono concepiti come un supporto alla collezione di requisiti e/o alla strutturazione e/o revisione di requisiti espressi in forma testuale. Le informazioni disponibili nello Schema UML possono essere riutilizzate come un punto di partenza per le formalizzazioni TRIO e SPN. Il processo di costruzione delle Reti SPN è stato studiato nell’ambito di un’attività di Dottorato di Ricerca condotta presso l’Università di Torino. Pertanto la presentazione di questa parte è demandata alla Tesi di Dottorato di [Bernardi, 2003]. L’obiettivo del presente rapporto è quello di fornire i risultati degli sviluppi metodologici relativi allo Schema TRIO e alla sua relazione con lo Schema UML. I contenuti di questo rapporto costituiscono pertanto lo sviluppo dello Schema TRIO accennato, rispettivamente, nei capitoli 6 e 7 del precedente rapporto di Ricerca di Sistema [Vulnera, 2001] che introduceva la Metodologia. Lo Schema UML viene qui riferito e parzialmente spiegato quando necessario. Per una presentazione dettagliata dello Schema UML si rimanda al documento [Depaude, 2002]. TRIO è una logica temporale lineare nata negli anni ’90 da un’attività di ricerca congiunta Politecnico di Milano ed ENEL-Centro di Ricerca in Automatica. Esso era stato concepito come un linguaggio formale dichiarativo per la specifica di sistemi in tempo reale. Dalle sue origini ad oggi sono stati sviluppati diversi dialetti e strumenti. Nello Schema TRIO per la dependability si fa uso del Linguaggio TRIO Modulare e degli strumenti sviluppati nel progetto europeo FAST www.prover.com/fast. Nell’ambito

del progetto FAST gli strumenti TRIO sono stati valutati su tre applicazioni relative a tre settori diversi: un sistema di controllo della velocità a bordo dell’automobile (proposto da Volvo), un controllore del segnalamento ferroviario (proposto da Ansaldo), un sistema di gestione del traffico aereo (proposto da Sextant Avionique). Nella Metodologia TRIO viene usato per specificare e analizzare requisiti di dependability e strategie di rimedio delle anomalie in un ambito logico temporale. Lo Schema TRIO include un insieme di tecniche che facilitano la costruzione e l’analisi di questo tipo di requisiti. Lo Schema definisce i passi per la costruzione incrementale della specifica e un insieme di sessioni di prova per effettuarne l’analisi. I passi e le sessioni di prova per la dependability utilizzano ed estendono le tecniche della metodologia base del linguaggio TRIO descritta in [TRIO, 2000]. Il processo di costruzione e analisi della specifica proposto dallo Schema TRIO viene esemplificato sul caso di studio di un sistema di automazione delle Cabine Primarie della Rete Elettrica di Distribuzione, chiamato PSAS. Lo Schema TRIO per il caso PSAS rappresenta la formalizzazione della strategia di recupero di errori e failures implementata nel Prototipo descritto nel rapporto di Ricerca di Sistema [Vulnera, 2003]. Nella formalizzazione della strategia PSAS vengono considerati gli aspetti relativi al comportamento ciclico e alle sincronizzazioni di un sistema di automazione distribuito e locale alla Cabina Primaria. Per ovvie ragioni di comunicabilità con la comunità scientifica, le parti formali della Metodologia sono in lingua inglese. Il rapporto è strutturato in capitoli che descrivono i componenti dello Schema TRIO per la dependability, come segue: • il capitolo 2 descrive il processo di costruzione della specifica TRIO • il capitolo 3 descrive il passo di derivazione della struttura TRIO dai diagrammi UML • il capitolo 4 descrive l’aggiunta di conoscenza di dominio pre-esistente alla struttura derivata • il capitolo 5 descrive il passo di completamento finale della specifica TRIO • il capitolo 6 descrive le linee guida del processo di analisi della specifica TRIO il capitolo 7 riassume i risultati raggiunti.