Indice

S3 - Risorse

Programma e testi

SPARK: Linguaggio e strumenti per la programmazione sicura.

Testo: [HIS] J. Barnes. High Integrity Software. Addison Wesley. 2006. ISBN 978-0-321-13616-9.

INFORMED: un metodo per la progettazione di dettaglio di programmi sicuri.

Testo: [INF] SPARK Team. INFORMED Design Method for SPARK. Praxis S.P0468.42.4. 2005.informed.pdf

Altre letture

ADA2005: la versione più aggiornata di Ada (in attesa del 2012).

Testo: [ALL] R. A. Cavalli et al. Introducing OCTAVE Allegro. CMU/SEI-2007-TR-012. allegro.pdf

KAOS: un metodo formale per la raccolta dei requisiti di sicurezza.

Testo: [KAO] A. van Lamsveerde. Requirements Engineering. Wiley. 2009. ISBN 978-0-470-01270-3. Capitoli 7-9,15,18.

J. Barnes. Programming in Ada95. Addison Wesley. 1998. Seconda edizione. ISBN 0-201-34293-6.

OCTAVE: un metodo per la raccolta dei requisiti di sicurezza.

R. A. Cavalli et al. Introducing OCTAVE Allegro. CMU/SEI-2007-TR-012. allegro.pdf

KAOS: un metodo formale per la raccolta dei requisiti di sicurezza.

A. van Lamsveerde. Requirements Engineering. Wiley. 2009. ISBN 978-0-470-01270-3. Capitoli 7-9,15,18.

Lucidi

- Introduzione al corso 01-introduzione_compatibility_mode_.pdf

- SPARK: introduzione 02-spark_compatibility_mode_.pdf

- SPARK: tipi elementari 03-spark2_compatibility_mode_.pdf

- SPARK: controllo 04-spark-controllo.pdf

- Esercitazione

- SPARK: moduli spark-moduli.pdf

- Flussi informativi flussiinformativi.pdf

- Tokeneer ID Station - Requisiti tis-srs.pdf

- Tokeneer ID Station - Architettura tis-architettura.pdf

- Condizioni di verifica - Parte I vc.pdf

- Aggiornamento versione SPARK

- SPARK: tavole sinottiche spark_qrg1.pdf spark_qrg2.pdf

- Tokeneer ID Station - Esercizio tis-architetturaesercizio2.pdf

- Tokeneer ID Station - Ristrutturazione di Clock time.zip

- Condizioni di verifica - Parte II vcpart2.pdf

- Condizioni di verifica - Examiner lucidi

- Esempio di verifica. Prodotto per somme successive: codice

- Condizioni di verifica - Parte III vc2.pdf

- Esempi di verifica. Funzioni funzioni.zip

- Condizioni di verifica - Parte IV vcrefinement.pdf

- Esempi di verifica. Raffinamento vcrefinement.zip

- Condizioni di verifica - Parte V vcrefinementtis.pdf

- Metafile per esaminare TIS (a partire da tismain.adb. Occhio ai path) tismain_smf.pdf

- Manuale per le condizioni di verifica examiner_genvcs.pdf

- Condizioni di verifica - Parte VI vcrefinementvolatili.pdf

- Metodo di progetto INFORMED -informed_design.pdf informeddesign2.pdf

- Esercizio: Boiler, con asserzioni

NB per gli abbonati a questa pagina

La pagina del progetto fonale è un livello sopra: S3 - Progetto finale

Lucidi in formato grande

- Parte I lucidi1.zip

- Parte II lucidi2.zip

- Parte III lucidi3.zip