Programma del corso e materiale di riferimento
(dal 2015/16 al 2018/19)
Prerequisiti
Il corso presuppone la conoscenza dei concetti fondamentali
alla base della sintassi e semantica della
logica proposizionale (o booleana), quali è
possibile acquisire
dal Cap. 2 delle dispense MC14.
Argomenti del corso
- Logica dei predicati
([MC14])
Sintassi e semantica.
Proprietà della logica dei predicati.
Teorie del primo ordine.
- Deduzione automatica
([MC14])
Il metodo dei tableaux per la logica proposizionale.
Algoritmo di unificazione.
Il metodo di risoluzione.
Raffinamenti della risoluzione: risoluzione lineare, risoluzione
con clausole unitarie.
Risoluzione SLD e programmazione logica.
- Il linguaggio Prolog
(Qualunque testo di introduzione al Prolog, ad esempio
[Bra88],
[CM93],
[CLMM97],
[FL88].
I testi seguenti contengono materiale più avanzato sul
linguaggio Prolog:
[NM95],
[Sho94].)
Il compilatore utilizzato è SWI-Prolog
[SWI].
- Metodi formali per la verifica di sistemi
-
Model
checking con LTL (logica temporale lineare).
([Pel] capitoli 1-6,
[MC09],
[Kat: cap. 1 (escluso 1.4) e cap. 2]
Modellazione di un sistema (sistemi di transizioni).
Linguaggi di specifica formale: logica temporale lineare.
Tableaux per la logica temporale lineare.
Automi su parole infinite, automi di Büchi.
Traduzione di formule LTL in automi.
Verifica di proprietà di un sistema rappresentate da formule
LTL.
Il tool per la verifica formale di sistemi software
SPIN.
-
Modellazione e verifica di sistemi con
proprietà temporali
([Kat: cap. 3 (introduzione, 3.1, 3.2 e
3.5); cap. 4 (4.1, 4.2 e 4.9)],
[Tutorial].)
Automi temporizzati.
Linguaggi di
specifica formale: Computational Tree Logic (CTL).
Il tool di modellazione e verifica
UPPAAL. Consultare la
Guida al linguaggio.
Materiale di riferimento
-
[MC14]
M. Cialdea Mayer.
Logica (dispense)
-
[Bra88]
I. Bratko.
Programmare in Prolog per l'Intelligenza Artificiale.
Masson - Addison Wesley, 1988.
-
[CM93]
W. F. Clocksin and C. S. Mellish.
Programmare in Prolog.
Franco Angeli, 1993.
(Il testo originale, in inglese, è disponibile anche
online)
-
[CLMM97]
L. Console, E. Lamma, P. Mello, M. Milano.
Programmazione Logica
e Prolog.
UTET Libreria, 1997.
-
[FL88]
F. Furlan e G.A. Lanzarone.
Prolog. Linguaggio e metodologia di programmazione logica.
Franco Angeli, 1988. Il libro è fuori stampa, ma si può
scaricare la
versione pdf, gentilmente messa a
disposizione dagli autori.
-
[NM95]
U. Nilsson and J. Maluszynski.
Logic, Programming and Prolog.
John Wiley & Sons, 1995.
-
[Sho94]
Y. Shoham.
Artificial Intelligence techniques in Prolog.Morgan Kaufmann, 1994.
-
[SWI]
SWI-Prolog: un compilatore Prolog (Free Software).
Ambienti e strumenti di programmazione:
Program development tools
SWI prolog editor (segnalato da uno studente, non testato dal docente)
Per chi lavora in ambiente
emacs o
Xemacs:
Prolog mode per Emacs (per sistemi Linux Debian o Ubuntu,
istallare il pacchetto prolog-el)
-
[Pel]
D. A. Peled.
Software Reliability Methods.
Springer, 2001.
Gli argomenti dei
capitoli 5 e 6 di questo testo sono trattati anche nelle dispense
MC09.
Questo testo è utile soprattutto per l'introduzione ai metodi
formali e la modellazione di sistemi (capitoli 1 e 4). Si noti che i
capitoli 2 e 3 dello stesso testo riguardano concetti di base trattati
in altra parte del corso.
-
[Kat]
J.-P. Katoen.
Concepts, Algorithms and Tools for Model Checking (Lecture
Notes of the Course
"Mechanised Validation of Parallel Systems", Friedrich-Alexander
Universität Erlangen-Nürnberg).
-
[MC09]
M. Cialdea Mayer.
Logica temporale e verifica di proprietà dei programmi (dispense).
-
[Tutorial]
Gerd Behrmann, Alexandre David, and Kim G. Larsen
A Tutorial on Uppaal 4.0.