Questo progetto presentato per l'esame di laboratorio software si colloca nell'ambito dell'ingegneria del software e della verifica formale.

Abstract

Molti linguaggi di descrizione architetturale sono stati proposti negli ultimi anni, con l’obiettivo di descrivere le più ampia classe di sistemi possibile: primo tra tutti l’UML. 

Per ciascuno di questi linguaggi varie sono state le tecniche di model checking applicate nel tentativo di verificare i modelli realizzati rispetto alla specifica. 

Tuttavia la ricerca di un linguaggio universale per la modellazione dei sistemi non è destinata ad avere successo: infatti identificare un unico linguaggio formale, di complessità e dimensioni accettabili, per descrivere sistemi molto diversi fra loro, in modo esaustivo e chiaro, risultato di fatto impossibile. 

Si sono quindi sviluppate varianti dei linguaggi generali per poterli applicare efficacemente a ambiti specifici e particolari: SysML uno di questi linguaggi derivati.

Esso infatti è un linguaggio UML 2 based studiato per la descrizione di sistemi real time. E stato progettato con l’intento di modellare un ampio spettro di sistemi, e la sua potenza sfruttabile soprattutto nello specificare: i requisiti, la struttura, il comportamento e i vincoli alle proprietà del sistema.

Il linguaggio progettato per supportare processi multipli e diversi metodi implementativi che vanno dalla programmazione strutturata alla programmazione object oriented (ogni struttura imporre vincoli diversi ai tipi e alla costruzione dei diagrammi). 

Durante il progetto si è analizzata un importante metodologia di model checking per UML e se ne analizzata l’applicabilità a SysML.