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
- Glossario glossariocompleto.pdf
- SPARK: introduzione 02-spark_compatibility_mode_.pdf
- Manuale SPARK spark95.pdf
- SPARK: tipi elementari 03-spark2_compatibility_mode_.pdf
- SPARK: controllo 04-spark-controllo.pdf
- Manuale Examiner examiner_um_win.pdf
- Esercitazione
- GPS gps.pdf
- Esempi: sottoprogrammi.zip, randomnumbers.zip
- SPARK: moduli spark-moduli.pdf
- Esempi: oggetto stack intstack.zip, intstackadt.zip
- SPARK_IO spark95_io.pdf
- Flussi informativi flussiinformativi.pdf
- Tokeneer ID Station - Requisiti tis-srs.pdf
- TIS - SRS41_1_srs.pdf
- Tokeneer ID Station - Architettura tis-architettura.pdf
- TIS - INFORMED Design tisdesign.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
- sono stati eliminati tutti i body da non eseminare
- 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