Ověřování systémů a softwaru: Techniky a nástroje pro ověřování modelů

Recenze čtenářů

Aktuálně nejsou k dispozici žádné recenze čtenářů. Hodnocení je založeno na 2 hlasů.

Původní název:

Systems and Software Verification: Model-Checking Techniques and Tools

Obsah knihy:

Kontrola modelů je účinný přístup k formální verifikaci softwaru.

Pokud je to možné, automaticky poskytuje úplné důkazy správnosti nebo pomocí protipříkladů vysvětluje, proč systém není správný. Tato kniha poskytuje základní úvod do této nové techniky.

V první části jsou jednoduše popsány teoretické základy modelové kontroly: přechodové systémy jako formální model systémů, temporální logika jako formální jazyk pro vlastnosti chování a algoritmy modelové kontroly. Druhá část vysvětluje, jak psát bohaté a strukturované specifikace temporální logiky v praxi, zatímco třetí část podává přehled některých hlavních dostupných model checkerů.