L’aumento della complessità e della sofisticazione dei sistemi utilizzati nell’ambito dell’automazione del sistema elettrico sta facendo aumentare i rischi di insuccesso dei progetti e rischia di ridurre la robustezza e l’affidabilità funzionale degli automatismi, con possibili problemi per l’esercizio e per la sicurezza del sistema. Questa situazione ha diverse cause, tra cui la ben nota crisi del software, che si è estesa dall’ambito dell’ information technology a quelli dell’information communication technology e dell’automation technology, settori sempre più dipendente dall’utilizzo di software avanzato. Negli ultimi decenni, infatti, il software è andato assumendo importanza sempre maggiore, sino a diventare una delle principali risorse in termini strategici e di investimento. Contemporaneamente la complessità dei sistemi d’automazione è notevolmente aumentata, ed in misura maggiore rispetto ai metodi di produzione del software: si è, infatti, passati da software sequenziale, utilizzato da specialisti, a sistemi reattivi e concorrenti usati dagli utenti finali. Come conseguenza i costi di sviluppo di sistemi in tempo reale stanno aumentando in modo esponenziale, sia in ambito mission critical, in cui le utility elettriche investono notevolmente per sviluppare e aggiornare i sistemi d’automazione utilizzati per la produzione, il trasporto e la distribuzione di energia elettrica, che in ambito safety critical (controlli ferroviari, telecomunicazioni, avvicina, sistemi medicali ecc.). E’ noto inoltre che tali massicci investimenti spesso non portano a risultati positivi: numerose indagini confermano che lo sviluppo di molti sistemi non viene completato e che diversi sistemi non superano i test di tipo e non vengono installati sugli impianti. Considerata l’entità degli investimenti in gioco è quindi naturale chiedere una maggiore qualità del prodotto ed una maggiore lunghezza alla vita dei prodotti, vale a dire di passare dal software usa e getta al software a lunga conservazione. Non sarebbe comunque corretto affermare che i sistemi e le tecniche di produzione del software non si siano evoluti per ridurre i costi e rischi di nsuccesso dei progetti. Il processo di produzione del software è oggi supportato da diverse metodologie, come l’IEC 61131 e l’IEC 61499 (function block) nell’ambito dell’automazione, l’IEC 61804 per il controllo di processo, o lo Unified Modellig Language (UML), nato in ambito in ambito information technology, ma che con le sue esrrecenti estensioni Real Time può essere utilizzato anche in ambito industriale. Tuttavia queste metodologie hanno risolto solo parte i problemi inerenti alla produzione del software; infatti, queste metodologie e gli associati strumenti

commerciali, essendo basati su approcci informali o semiformali, non consentono di validare le specifiche e quindi non supportano un ciclo di sviluppo che garantisca la necessaria qualità dei prodotti. Con l’obiettico di migliorare la qualità e la robustezza dell’automazione, nel progetto di ricerca di ssitema COMINICA/ADSPE sono stati definiti e sperimentati metodi per supportare le fasi di alte della specifica dei requisiti, di progetto e per supportare la verifica di correttezza. In particolare, al fine di estendere e favorire l’impiego di metodi formali in tutte le fasi del ciclo di vita, sono stati definiti: • un approccio per la specifica dei sistemi real time basato su una forma ristretta di linguaggio naturale (LNC o Linguaggio Naturale Controllato) che si appoggia sulla logica temporale TRIO e che consente di specificare un sistema in una forma molto vicina alle tipiche specifiche in linguaggio naturale e di verificarne la correttezza applicando metodi di verifica basati sulla logica temporale metrica. • un approccio alla verifica di correttezza interna e di adeguatezza delle specifiche che consente di verifica e validare specifiche di requisiti per la loro consistenza e adeguatezza • un approccio alla validazione di progetto, relativamente ai requisiti. Questo rapporto presenta i risultati relativi alla verifica e validazione dei sistemi nelle fasi di ingegneria dei requisiti e di progetto. Dopo aver introdotto le esigenze essenziali di una metodologia integrata per la specifica e il progetto dei sistemi e del linguaggio TRIO (linguaggio di riferimento degli studi effettuati), vengono presente tecniche per la verifica di correttezza di specifiche in LNC e di specifiche di progetto basate su reti. In conclusione viene presentata una metodologia per verificare le specifiche tramite la generazione di modelli rilevanti su domini finiti. I risultati ottenuti consentono di preconizzare una effettiva applicazione di approcci formali per migliorare la robustezza funzionale dei sistemi nel ciclo di vita dell’automazione del sistema elettrico, cosa sdempre più rilevante dati i cambiamenti in atto nella organizzazione e nell’eserzio del sistema.