=====  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.{{:magistralesicurezza:sss: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. {{:magistralesicurezza:sss: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. {{:magistralesicurezza:sss: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 {{:magistralesicurezza:sss:01-introduzione_compatibility_mode_.pdf|}}

  * Glossario {{:magistralesicurezza:sss:glossariocompleto.pdf|}}

- SPARK: introduzione  {{:magistralesicurezza:sss:02-spark_compatibility_mode_.pdf|}}

  * Manuale SPARK {{:magistralesicurezza:sss:spark95.pdf|}}

- SPARK: tipi elementari {{:magistralesicurezza:sss:03-spark2_compatibility_mode_.pdf|}}

- SPARK: controllo {{:magistralesicurezza:sss:04-spark-controllo.pdf}}

  * Manuale Examiner {{:magistralesicurezza:sss:examiner_um_win.pdf|}}

- Esercitazione

  * GPS {{:magistralesicurezza:sss:gps.pdf|}}
  * Esempi: {{:magistralesicurezza:sss:sottoprogrammi.zip|}}, {{:magistralesicurezza:sss:randomnumbers.zip|}}

- SPARK: moduli {{:magistralesicurezza:sss:spark-moduli.pdf}}

  * Esempi: oggetto stack {{:magistralesicurezza:sss:intstack.zip|}}, {{:magistralesicurezza:sss:intstackadt.zip|}}
  * SPARK_IO {{:magistralesicurezza:sss:spark95_io.pdf|}}

- Flussi informativi {{:magistralesicurezza:sss:flussiinformativi.pdf|}}

- Tokeneer ID Station - Requisiti {{:magistralesicurezza:sss:tis-srs.pdf|}}

  * TIS - SRS{{:magistralesicurezza:sss:41_1_srs.pdf|}}

- Tokeneer ID Station - Architettura {{:magistralesicurezza:sss:tis-architettura.pdf}}

  * TIS - INFORMED Design {{:magistralesicurezza:sss:tisdesign.pdf|}}
 
- Condizioni di verifica - Parte I {{:magistralesicurezza:sss: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 {{:magistralesicurezza:sss:bin.zip|}} e {{:magistralesicurezza:sss:lib.zip|}} di questa distribuzione.
  * La nuova documentazione è {{:magistralesicurezza:sss:html.zip|qui}}. Istruzioni d'uso {{:magistralesicurezza:sss:usoversione8.zip|qui}}.

- SPARK: tavole sinottiche {{:magistralesicurezza:sss:spark_qrg1.pdf|}} {{:magistralesicurezza:sss:spark_qrg2.pdf|}}

- Tokeneer ID Station - Esercizio {{:magistralesicurezza:sss:tis-architetturaesercizio2.pdf|}}

- Tokeneer ID Station - Ristrutturazione di Clock  {{:magistralesicurezza:sss:time.zip|}}

- Condizioni di verifica - Parte II {{:magistralesicurezza:sss:vcpart2.pdf|}} 

- Condizioni di verifica - Examiner {{:magistralesicurezza:sss:vcexaminer.pdf|lucidi}}

- Esempio di verifica. Prodotto per somme successive:  {{:magistralesicurezza:sss:prodotto.zip|codice}} 

- Condizioni di verifica - Parte III {{:magistralesicurezza:sss:vc2.pdf|}}


- Esempi di verifica. Funzioni {{:magistralesicurezza:sss:funzioni.zip|}}

- Condizioni di verifica - Parte IV {{:magistralesicurezza:sss:vcrefinement.pdf|}}

- Esempi di verifica. Raffinamento {{:magistralesicurezza:sss:vcrefinement.zip|}}

- Condizioni di verifica - Parte V {{:magistralesicurezza:sss:vcrefinementtis.pdf|}}

- Metafile per esaminare TIS (a partire da tismain.adb. Occhio ai path) {{:magistralesicurezza:sss:tismain_smf.pdf|}}
   * sono stati eliminati tutti i body da non eseminare

- Manuale per le condizioni di verifica {{:magistralesicurezza:sss:examiner_genvcs.pdf|}}

- Condizioni di verifica - Parte VI {{:magistralesicurezza:sss:vcrefinementvolatili.pdf|}}

- Metodo di progetto INFORMED -{{:magistralesicurezza:sss:informed_design.pdf|}} {{:magistralesicurezza:sss:informeddesign2.pdf|}}

- Esercizio: {{:magistralesicurezza:sss:boiler.zip|Boiler}}, {{:magistralesicurezza:sss:boilerwithassertions.zip|con asserzioni}}

== NB per gli abbonati a questa pagina ==
La pagina del progetto fonale è un livello sopra: [[magistralesicurezza:sss:progetto|]]

== Lucidi in formato grande ==

- Parte I {{:magistralesicurezza:sss:lucidi1.zip|}}

- Parte II {{:magistralesicurezza:sss:lucidi2.zip|}}

- Parte III {{:magistralesicurezza:sss:lucidi3.zip|}}