Программа для проверки корректности контроля доступа в системах больших данных с использованием темпоральной логики

Программа предназначена для проверки корректности контроля доступа при обработке и хранении больших данных. Программа может использоваться в системах больших данных. Функциональные возможности программы: Программа принимает на вход файл, описывающий пользователей системы больших данных, включая имена, функциональные роли, подразделения; файл, описывающий графовую модель системы больших данных в виде списка вершин фрагментов данных и ребер-направлений обработки данных; файл, содержащий ограничения для генерации спецификаций. Программа для всех указанных пользователей генерирует спецификации контроля доступа на основе временной логики TLA+ с учетом заданных ограничений. Выполняется TLC (explicit-state model-checker)-верификация и результирующая матрица доступа сохраняется в выходную HTML-таблицу, где отмечены выявленные нарушения безопасности.