Verifica Automatica

Obiettivi Formativi

Un sistema reattivo è un sistema (in genere concorrente) che interagisce con l'ambiente in cui opera. Cioè un sistema reattivo reagisce all'input (dall'ambiente) producendo un output (verso l'ambiente) e cambiando il suo stato interno. Ecco alcuni esempi di sistemi reattivi: Sistemi Embedded , SOC (Systems On Chip) , Sistemi Operativi , Protocolli , Sistemi di Controllo, Hardware Digitale, Sistemi Ibridi (cioè sistemi dinamici nei quali lo stato ha sia componenti discrete che componenti continue). La progettazione di sistemi reattivi avviene con un time-to-market sempre più corto e/o con un costo degli errori sempre più alto. Questo tende a far crescere sempre più il costo della fase di testing per tali sistemi. Ad esempio il costo del testing nel progetto di sistemi reattivi oggi è tipicamente nell'ordine del 50% del costo totale. A causa della forte competizione del mercato, per molti prodotti di largo consumo (e.g. cpu, hardware digitale, cellulari, sistemi embedded in generale) è necessario diminuire sempre più sia il time-to market che il costo della progettazione. Questo vuol dire diminuire il tempo dedicato al testing ed allo stesso tempo aumentarne la copertura.

L'obiettivo dei metodi di verifica automatica è esattamente quello di progettare algoritmi e tools che diano una copertura del 100% (testing esaustivo) in un tempo ragionevole. Gli obiettivi del percorso di verifica automatica sono dunque quelli di mettere in grado lo studente di:

usare proficuamente i tools di verifica automatica disponibili sul mercato; progettare algoritmi che possano migliorare le perferomance dei tools esistenti.

Sbocchi Professionali

Una formazione sulle tematiche di verifica automatica, validazione e testing trova ovviamente spazio di lavoro in qualsiasi azienda in cui si progettano sistemi embedded (hardware e/o software). Per maggiori informazioni si veda questo sito sul model checking http://www.dsi.uniroma1.it/~tronci/model-checking/casalab.html . Il percorso prevede un totale di 8 moduli, secondo lo schema che segue.

Prerequisiti

• Tutti gli esami del primo biennio della laurea triennale in Informatica.
• Calcolo delle Probabilità oppure Sistemi a Molte Componenti

Insegnamenti Obbligatori

• Verifica Automatica
• Ingegneria del Software 2
• Sicurezza dei Dati e delle Reti
• Programmazione Matematica (MAT/09)

Insegnamenti a Scelta

• quattro insegnamenti a scelta tra
  • Algoritmi per Reti
  • Algoritmi Paralleli e Distribuiti
  • Crittografia
  • Ingegneria del Software 1
  • Matematica Computazionale (MAT/08)
  • Programamzione di Rete
  • Reti Avanzate
  • Sistemi Operativi 2
  • Tecniche di Sicurezza dei Sistemi
  • Teoria della Concorrenza
  • Teoria della Dimostrazione
  • Teoria dell'Informazione
  • Teoria dei Sistemi (ING-INF/04)(Ingegneria)