Titolo del progetto
Attività di progettazione per l'applicabilità della verifica formale del software all'interno del ciclo di produzione aziendale
Il presente progetto consiste in uno studio di fattibilità realizzato da parte
dell'Università degli studi di Genova, facoltà di Ingegneria.
Lo studio, svolto in collaborazione con il DIST, è stato coordinato dal Prof. Armando Tacchella.
Il presente progetto studia la possibilità di inserire all’interno del processo produttivo di Medservice.com l’utilizzo di sistemi automatici per la verifica del software.
Queste attività, inserite nel processo di sviluppo del software, vogliono garantire un prefissato livello di qualità del prodotto finale.
Ai fini di contestualizzare il contributo di questo progetto è opportuno ricordare le definizioni di malfunzionamento, difetto ed errore.
In particolare:
Malfunzionamento (failure): è un funzionamento di un programma diverso da quanto previsto dalla sua specifica
Difetto (fault): è la causa del malfunzionamento
Errore (error): è l’origine del difetto.
Attraverso la verifica del software è possibile individuare alcuni errori in fase di progettazione e quindi prevenire problematiche inerenti il comportamento di sistemi software,
in particolare riguardo alla corrispondenza tra tale comportamento e le specifiche sulla base delle quali i sistemi sono stati realizzati.
Per la realizzazione dello studio, l'università, ha proceduto a svolgere differenti verifiche, anche attraverso l'utilizzo del software, in relazione alla fattibilità di
questa tipologie di attività in ambito aziendale.
Nella ricerca, sono stati presi in considerazione i metodi principali su cui si basa la verifica statica, ovvero la dimostrazione automatica dei teoremi e la verifica dei modelli.
A seguito di questa analisi, la tecnica scelta per questo progetto, è quella della verifica dei modelli
(Model Checking) in quanto ha al suo attivo numerosi casi di successo di utilizzo in ambito industriale.
Visto che i possibili stati di un programma in linea teorica sono infiniti, sono state considerate tecniche che riconducono
il problema della verifica del software a quello della verifica di sistemi con un insieme finito di stati.
Infine, considerato che, dal punto di vista scientifico, la verifica di correttezza del software rimane comunque un problema indecidibile,
il presente progetto ha permesso di concludere che, da un punto di vista pratico, tali tecniche risultano applicabili anche in un contesto PMI.
Questo è dovuto sia all’elevato grado di sofisticazione raggiunto dalle tecniche di verifica allo stato dell’arte, sia al fatto che le applicazioni
oggetto del del presente progetto sono principalmente focalizzate su sistemi embedded a bordo di veicoli o sistemi di segnalamento di terra o di bordo,
che risultano spesso implementazioni a livello software di macchine a stati finiti.
Pertanto gli aspetti che rendono il problema in generale troppo complesso, negli specifici scenari in cui opera prevalentemente Medervice.com,
sono assenti o fortemente attenuati.