Differenze

Queste sono le differenze tra la revisione selezionata e la versione attuale della pagina.

--- magistralesicurezza:sss:risorse [09/05/2010 alle 19:45 (16 anni fa)] – Carlo Montangero
+++ magistralesicurezza:sss:risorse [27/09/2010 alle 17:43 (15 anni fa)] (versione attuale) – Carlo Montangero
@@ Linea 1: / Linea 1: @@
-{{:magistralesicurezza:sss:time.zip|}}=====  S3 - Risorse =====
+=====  S3 - Risorse =====
 === Programma e testi  ===
@@ Linea 11: / Linea 11: @@
 Testo: [INF] SPARK Team. //INFORMED Design Method for SPARK//. Praxis S.P0468.42.4. 2005.{{:magistralesicurezza:sss:informed.pdf|}}
-== OCTAVE: un metodo per la raccolta dei requisiti di sicurezza. ==
+=== 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|}}
@@ Linea 18: / Linea 20: @@
 Testo: [KAO] A. van Lamsveerde. //Requirements Engineering//. Wiley. 2009. ISBN 978-0-470-01270-3. Capitoli 7-9,15,18.
-=== Altre letture ===
 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 ===
@@ Linea 70: / Linea 78: @@
 - Tokeneer ID Station - Esercizio {{:magistralesicurezza:sss:tis-architetturaesercizio2.pdf|}}
-- Tokeneer ID Station - Ristrutturazione di Clock {{:magistralesicurezza:sss:timet.zip|}} corretta: {{:magistralesicurezza:sss:time.zip|}}
+- Tokeneer ID Station - Ristrutturazione di Clock  {{:magistralesicurezza:sss:time.zip|}}
 - Condizioni di verifica - Parte II {{:magistralesicurezza:sss:vcpart2.pdf|}}
@@ Linea 79: / Linea 87: @@
 - Condizioni di verifica - Parte III {{:magistralesicurezza:sss:vc2.pdf|}}
-   * sono stati eliminati tutti i body da non eseminare
 - Esempi di verifica. Funzioni {{:magistralesicurezza:sss:funzioni.zip|}}
@@ Linea 90: / Linea 98: @@
 - 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|}}