Una tecnica fondamentale di verifica in ogni settore dell’ingegneria è il testing, inteso come la verifica sperimentale del corretto funzionamento di un sistema rispetto a un insieme limitato di condizioni, ritenute particolarmente significative. L’inevitabile presenza di errori nel progetto e nella realizzazione di un sistema di automazione rende necessaria diverse attività di verifica di correttezza, durante tutto il ciclo di sviluppo. Tale attività di verifica sono più complesse e difficili per i sistemi in tempo reale che per i tradizionali sistemi sequenziali o concorrenti, sia a causa del fatto che un sistema di automazione è spesso embedded in un sistema complesso, sia a causa della presenza della variabile tempo. Allo stato dell’arte, l’attività di verifica sperimentale sembra dunque insostituibile e in effetti, l’uso di strategie sistematiche di testing, se supportate da strumenti adatti, può aumentare sia la possibilità di trovare errori che la confidenza nel corretto funzionamento del sistema, nel caso in cui non vengano riscontrati errori. Il testing può essere utile anche quando si ritiene che altre tecniche formali, come ad esempio una dimostrazione di correttezza, siano indispensabili. Sembra infatti ragionevole ottenere un certo grado di confidenza nel sistema con prove sperimentali prima di tentare altre attività difficile e certamente più costose. Questo rapporto presenta i meccanismi di testing supportati dalla metodologia di specifica formale TRIO e sviluppati nell’ambito del progetto europeo FAST (EC n. 25581), che ha visto coinvolti il CESI, la Prover Technology, la Ansaldo Segnalamento Ferroviario, la Sextant Avionique e la Volvo. Il linguaggio di specifica TRIO, sviluppato dal CISE, ENEL Ricerca e Politecnico di Milano, e ora dal CESI in diversi progetti interni e collaborativi, supporta la fase di specifica dei requisiti di un sistema di automazione e quella di verifica e validazione sia omogenee che eterogenee, tramite la generazione di casi di test. Nel approccio TRIO, i casi di test sono descrizioni del comportamento di sistemi, composti dagli eventi che si verificano durante l’esecuzione e dalla loro temporizzazione. Ogni evento è etichettato con un attributo di ingresso o di uscita che consentono di distinguere gli stimoli da fornire al sistema durante il testing dalle risposte attese dal sistema. Nel progetto EC FAST è stata perfezionata una metodologia per identificare/definire specifiche di casi di test che possono guidare le attività di testing a partire dal una specifica formale dei requisiti di un sistema. L’approccio utilizza: • i requisiti funzionali per derivare o riconoscere comportamenti di un sistema che saranno usati come specifiche di casi di test per l’accettazione di un sistema relativamente alle specifiche di requisito.

• la dichiaratività del linguaggio TRIO che consente di specificare vincoli utili per selezionare casi di test significativi. In questo modo l’utente può usare lo stesso linguaggio quando specifica i requisiti di un sistema e quando caratterizza gli scopi del testing L’applicazione del metodo non è limitata alla verifica del software: dato che i casi di test sono derivati dalla specifica del sistema, il metodo può essere utilizzato per verificare qualunque tipo di sistema specificato in modo formale. Il rapporto, un versione rivista di un rapporto (in inglese) del progetto EC FAST che ha definito un approccio al testing basato sulla specifica di requisito, è organizzato come segue: • il capitolo 2 presenta l’approccio TRIO al testing. Una volta introdotto un modello di riferimento per il testing basato sulla specifica, viene riassunto il processo di generazione dei casi di test a partire da una specifica TRIO. • il capitolo 3 introduce la metodologia per la specifica dei casi di test da generare sulla base di una specifica Modular TRIO, in particolare illustra le estensioni linguistiche di Modular TRIO per decorare la specifica, distinguendo le informazioni utili a stimolare il sistema dai risultati attesi, e introducendo nuove formule che caratterizzano gli scopi del test. Inoltre identifica i requisiti che devono essere soddisfatti per consentire la generazione dei casi di test • il capitolo 4 presenta un metodo per la generazione dei casi di test. Nel capitolo vengono introdotte diverse strategie che guidano la generazione di casi di test per la verifica di diversi aspetti del sistema e delle metriche utili a valutare la copertura dei casi di test generati. le appendici riportano la sintassi delle estensioni introdotte per supportare l’attività di generazione dei casi di test.