|
|
|
|
Laurea Specialistica in
Ingegneria Informatica,
Corso di
Metodi Formali nell'Ingegneria del Software
Edizione dell'a.a. 2007/08
Progetti svolti dagli studenti
Torna alla lista dei progetti »
Logiche Temporali al servizio dell'Ingegneria del Software: CTL, CTL*, TRIO e LTLB
- Autori:
- Categorie: Logiche temporali; Verifica di algoritmi, programmi, protocolli e hw
Sommario
Durante il corso di Metodi Formali per l'Ingegneria del Software è stato illustrato l'utilizzo della logica temporale LTL per verificare proprietà di documenti di analisi, come diagrammi degli stati UML, e di programmi, per verificarne la terminazione e la correttezza parziale o totale.
Il presente lavoro si prefigge lo scopo di scendere in profondità nello studio delle logiche temporali, vagliando diverse possibilità e analizzandone i pregi e i difetti, confrontandoli con la già conosciuta LTL, e introducendo per ognuna di esse possibili applicazioni nell'ambito del Model Checking.
Nel capitolo 2 ci si avvicinerà alla logica CTL, per certi versi simile a LTL, e alla logica CTL*, che costituisce un sovrainsieme di entrambe le precedenti, e verrano mostrate applicazioni di CTL nel capitolo 3. Nel capitolo 4 verrà introdotta la logica TRIO, e verrà descritta una visione generale del complesso ma interessante processo per ottenerne un'applicazione pratica. Si vedrà come TRIO abbia importanti analogie con la logica LTLB, ovvero la logica LTL con operatori per il passato, che viene pertanto descritta nel conclusivo capitolo 5, insieme ad una sua applicazione pratica.
Materiale prodotto
|
Home page