На правах рекламы:
ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Авторитетность издания

ВАК - К1
RSCI, ядро РИНЦ

Добавить в закладки

Следующий номер на сайте

2
Ожидается:
16 Июня 2024

В Российском государственном социальном университете рассмотрен и проанализирован предлагаемый автором метод для преодоления проблемы комбинаторного взрыва.

09.08.2016

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

С каждым днем программные и технические системы становятся все более сложными и объемными, а степень их распределенности может измеряться сотнями и даже тысячами вычислительных узлов. В таких условиях полная верификация подобных систем становится весьма затруднительной или в принципе невозможной даже с применением уже существующих методов борьбы с комбинаторным взрывом. Идея предлагаемого в статье метода базируется на том, что процесс верификации должен проводиться аналогично процессу выполнения, то есть в данном случае распределенно. Это позволяет сформулировать новый алгоритмический подход для преодоления проблемы комбинаторного взрыва.

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