Oggi i sistemi hardware e software sono ampiamente usati in applicazioni in cui non possono essere accettati errori. E’ questo il caso di moltissimi sistemi di controllo industriale, per cui è critica l’esigenza di software ed hardware affidabile. La complessità di questi sistemi, spesso concorrenti e/o distribuiti, rende assai difficile garantire che il loro funzionamento sia corretto in tutte le situazioni che si possano presentare. Per questo, negli anni recenti è stato ampiamente discusso il problema di produrre in maniera economica ed efficiente specifiche corrette di sistemi industriali complessi. Una soluzione per questo problema, che è emersa in maniera evidente sia in ambito accademico che in ambito industriale, consiste nel ricorso a metodi e strumenti formali. Tali strumenti presentano, infatti, alcune caratteristiche che li rendono potenzialmente interessanti per applicazioni in ambito industriale dove sono necessari strumenti che siano: • non ambigui, permettano, cioè, di specificare il sistema senza che i progettisti debbano preoccuparsi di verificare l’assenza di ambiguità nei documenti prodotti, • supportati da strumenti software che aiutino il progettista nella scrittura, verifica e validazione delle specifiche, • in grado di permettere la definizione di un’opportuna metodologia di specifica che supporti l’attività degli specificatori. I metodi formali, in particolare quelli basati su formalismi di tipo logico matematico, presentano le caratteristiche indicate, in quanto, oltre a fornire linguaggi di specifica non ambigui, consentono di definire un calcolo logico che permette di ragionare sulle specifiche prodotte e di derivare da esse informazioni implicite. Data l’intrinseca complessità degli strumenti logico matematici, dal punto di vista delle applicazioni in ambito industriale è di fondamentale importanza basare l’attività di specifica su strumenti di supporto che siano il più possibile standardizzati e guidino l’utente nella stesura di specifiche corrette. La notazione matematica inoltre consente di strutturare le specifiche in moduli. È importante notare la differenza tra questa nozione di modularizzazione e quella utilizzata nell’ordinaria pratica matematica, dove i nomi denotano direttamente oggetti matematici. Nell’attività di specifica, i nomi si riferiscono invece a parti della stessa descrizione e la strutturazione serve a descrivere le modalità di combinazione ed estensione di questi frammenti di testo e non ad abbreviare la descrizione. Pertanto i meccanismi di strutturazione delle specifiche rappresentano un’estensione dell’ordinaria pratica matematica e devono essere supportati da strumenti che ne evidenzino la correttezza, sulla base di un modello matematico del contenuto della specifica. Un secondo vantaggio dell’uso dei sistemi formali è il supporto che essi danno all’analisi ed alla verifica della specifica. Infatti, una semantica formale cui sia associato un calcolo logico consente di ragionare sulla specifica e derivarne conseguenze. Derivare conseguenze dalla specifica è un aiuto importante per controllare che la specifica soddisfi pienamente le richieste attese e garantisca il corretto funzionamento delle implementazioni. La semantica formale fornisce inoltre una “vista” della specifica che astrae dai dettagli inessenziali dovuti alla sintassi. Questa

vista permette di confrontare varie tecniche di specifica in maniera oggettiva e di determinare nuovi costrutti linguistici di specifica. Questo rapporto introduce una estensione della forma tabellare del Linguaggio Naturale Controllato che consente di specificare le proprietà di un sistema e di utilizzare un approccio property oriented alla specifica che offre un aiuto significativo nella verifica/validazione dei requisiti funzionali ed è quindi essenziale nella caratterizzazione dei sistemi.