Verifica di sistemi e software: Tecniche e strumenti di verifica dei modelli

Recensioni dei lettori

Attualmente non ci sono recensioni dei lettori. La valutazione si basa su 2 voti.

Titolo originale:

Systems and Software Verification: Model-Checking Techniques and Tools

Contenuto del libro:

Il model checking è un approccio potente per la verifica formale del software.

Quando è applicabile, fornisce automaticamente prove complete di correttezza o spiega, tramite controesempi, perché un sistema non è corretto. Questo libro fornisce un'introduzione di base a questa nuova tecnica.

La prima parte descrive in termini semplici le basi teoriche del model checking: i sistemi di transizione come modello formale dei sistemi, la logica temporale come linguaggio formale per le proprietà comportamentali e gli algoritmi di model checking. La seconda parte spiega come scrivere in pratica specifiche logiche temporali ricche e strutturate, mentre la terza parte esamina alcuni dei principali model checker disponibili.