Libri di Testo:

• Metodi Formali

•  Doron A. Peled. Software Reliability Methods. Springer Verlag, 2001
• Michael Huth, Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2005.
  

• Abstract State Machines

•  Egon Boerger, Robert Staerk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer Verlag, 2003
  

Materiale Didattico:

• Lez-0: introduzione al corso
• Lez-0-1: modelli di processo, qualità della specifica e linguaggi per la specifica
• Lez-2-3: macchine a stati finiti (semplici ed estese),  macchine per la comunicazione di processi; esempi di modelli
• Lez-4-5: macchine di stato di UML; esempi di applicazioni
• Lez5bis: diagrammi di attività in UML
  
• Lez-6: OCL
  
• Lez-7: Automi di Kripke
• Lez-8-9: logica CTL ed algoritmo di Model Checking
• Lez-10: Symbolic Model Checking
  
• Lez-11-12: SMV
• Lez-13: Verifica di proprietà di modelli
  
• Lez-14: Astrazione
• Lez-15-16: Abstract State Machines
• Lez-17: Il caso di studio del Lift
  
• Lez-18: ASM multi agenti
• Lez-19: AsmGofer
  
• Lez-20: Il caso di studio del Light Control System