Sistemi a tempo reale - Teoria (2007/2008)

Corso disattivato non visibile

Codice insegnamento
4S01075
Docente
Tiziano Villa
crediti
4
Settore disciplinare
ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Lingua di erogazione
Italiano
Sede
VERONA
Periodo
1° Q dal 3-ott-2007 al 4-dic-2007.

Per visualizzare la struttura dell'insegnamento a cui questo modulo appartiene, consultare * organizzazione dell'insegnamento

Orario lezioni

1° Q
Giorno Ora Tipo Luogo Note
lunedì 11.30 - 13.30 lezione Aula E dal 29-ott-2007  al 30-nov-2007
lunedì 11.30 - 13.30 lezione Aula D dal 3-dic-2007  al 4-dic-2007
giovedì 14.30 - 16.30 lezione Aula B  

Obiettivi formativi

L'obiettivo del corso e' d'introdurre modelli formali e metodologie di progettazione per descrivere, analizzare e sintetizzare sistemi elettronici in tempo reale, con particolare riferimento a sistemi incorporati.

Programma

Metodi formali per sistemi in tempo reale
1. Sistemi combinatori e reattivi
2. Macchine a stati deterministiche, semi-deterministiche e non-deterministiche
3. Composizione di macchine a stati
4. Simulazione, bisimulazione e determinizzazione di macchine a stati
5. Equivalenza, contenimento e minimizzazione di macchine a stati
6. Sintesi di controllori discreti per sicurezza e progressivita'
7. Automi ibridi
8. Automi con orologi e loro discretizzazione
9. Analisi di raggiungibilita' di automi ibridi
10. Sintesi di controllori ibridi per sicurezza e progressivita'
11. Verifica formale di sistemi modellati da automi discreti e ibridi

Metodologia di progettazione di sistemi in tempo reale
1. Introduzione ai sistemi incorporati
2. Processi concorrenti e sistemi operativi in tempo reale
3. Algoritmi per la pianificazione ("scheduling") di processi aperiodici in tempo reale
4. Algoritmi per la pianificazione di processi periodici in tempo reale
5. Analisi degli algoritmi di pianificazione e calcolo di maggioranti significativi

Modalità d'esame

Prova scritta e progetto.

Il progetto richiede la verifica formale di proprieta' di sicurezza di sistemi rappresentati da automi ibridi, mediante l'utilizzo di codici che verificano proprieta' temporali di automi ibridi mediante un'analisi di raggiungibilita'.

Materiale didattico

Documenti