Metodi e Strumenti per la Verifica

Scopo del corso è di esporre il problema della verifica di sistemi concorrenti 
e distribuiti usando diversi formalismi per la descrizione dei sistemi e metodi per la specifica e la verifica delle loro proprietà.  

 Il corso introdurrà formalismi per la descrizione  di sistemi concorrenti, distribuiti e con tempo reale. 
In particolare verranno considerati Automi temporizzati, Reti di Petri e Statecharts, affrontandone gli aspetti 
semantici e di verifica delle loro proprietà. Si presenteranno strumenti automatici che verranno utilizzati per 
sviluppare specifiche  e prove per casi di esempio.

 The course will introduce formalisms fot the description of concurrent, distributed and real-time systems. 
In particular, Timed automata, Petri nets and Statecharts will be considered and their semantical aspects and 
verification problems will be tackled.  Automatic tools for specification and verification will be described and used to develop 
specifications and verifications for sample cases.

 Articoli sui formalismi considerati.