Программные продукты и системы

В последнее время широкое распространение в области верификации получил метод Model Checking, или метод проверки на моделях. Суть его – в верификации свойств системы, представленных в виде формул временных логик LTL или CTL. При этом верифицируемая модель может быть задана явно (путем перечисления всех состояний и соединяющих их ребер) или неявно (путем задания булевых функций, определяющих отношение переходов и множество начальных состояний). Однако при верификации больших информационных систем, в том числе и распределенных программных, зачастую приходится иметь дело с очень большим числом состояний вычислительного процесса для их моделей. Например, для программы, в рамках которой одновременно выполняются 10 потоков, причем каждый из них может находиться в одном из 5 состояний, общее число состояний вычислительного процесса может достигать 510 = 9765625, что может стать непреодолимым препятствиям на пути верификации тех или иных ее свойств. Кроме того, в модели могут явно присутствовать вычисления, переход в которые никогда не встретится на практике.

Сегодня существуют два основных подхода к выполнению верификации данных систем:

− построение более абстрактной, менее детализированной модели на базе исходной;

− выполнение верификации модели на ее сжатом, приведенном к некоторому сжатому виду представлении.

Подробное описание дается в статье «Метод ограничений верифицируемых моделей», авторы: Кораблин Ю.П., Шипов А.А. (Российский государственный социальный университет, г. Москва).