Verificarea sistemelor și a software-ului: Tehnici și instrumente de verificare a modelelor

Recenzii ale cititorilor

În prezent, nu există recenzii ale cititorilor. Evaluarea se bazează pe 2 voturi.

Titlul original:

Systems and Software Verification: Model-Checking Techniques and Tools

Conținutul cărții:

Verificarea modelelor este o abordare puternică pentru verificarea formală a software-ului.

Atunci când este aplicabilă, aceasta furnizează automat dovezi complete de corectitudine sau explică, prin intermediul unor contraexemple, de ce un sistem nu este corect. Această carte oferă o introducere de bază în această nouă tehnică.

Prima parte descrie în termeni simpli bazele teoretice ale verificării modelelor: sistemele de tranziție ca model formal al sistemelor, logica temporală ca limbaj formal pentru proprietățile comportamentale și algoritmii de verificare a modelelor. A doua parte explică cum se pot scrie în practică specificații bogate și structurate de logică temporală, în timp ce a treia parte trece în revistă unele dintre principalele verificatoare de modele disponibile.