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

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

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

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.

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

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

- 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

• La versione 8.1.1 di SPARK supera alcuni problemi riscontrati con la versione precedente. Per installarla, è sufficiente sostituire il contenuto della cartella C:\SPARK\windows con le cartelle bin.zip e lib.zip di questa distribuzione.
• La nuova documentazione è qui. Istruzioni d'uso qui.

- 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

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

- Parte I lucidi1.zip

- Parte II lucidi2.zip

- Parte III lucidi3.zip