MODEL СHECKING. Верифікація паралельних і розподілених програмних систем 4695

У книзі розповідається про нові результати в області верифікації за допомогою методу model checking і наводяться приклади додатків цього методу в самих різних областях. Розглядаються проблема верифікації, темпоральні логіки, алгоритми model checking для CTL і LTL, структури Кріпке як моделі реагуючих систем, специфікація властивостей реагуючих систем формулами темпоральних логіки, бінарні вирішальні діаграми, символьна верифікація, кількісний аналіз систем і системи реального часу, а також застосування фундаментальних ідей алгоритму model checking в різних додатках. На прикладеному компакт-диску перебувають: інструкція по установці системи верифікації Spin, методичний посібник по цій системі і опис курсової роботи з верифікації нетривіальною системи логічного керування з декількома варіантами завдань.

MODEL СHECKING. Верифікація паралельних і розподілених програмних систем