Аннотация: Обеспечение согласованного управления доступом является одной из ключевых задач безопасности в гетерогенных системах больших данных. Проблема представляет собой большое число инструментов обработки данных, источников и пользователей информации; разнородность моделей безопасности; сложность гранулированных правил доступа. Анализ временного фактора в данном случае позволит повысить согласованность и надежность разграничения доступа. Целью работы является выбор методологии и инструментария для имплементации временной логики в процессы верификации контроля доступа систем больших данных. Анализируются виды временной логики и методы верификации на основе TLA (Temporal Logic of Actions). Предлагается использование TAL+ для решения поставленной задачи, приводится пример соответствующей спецификации

Ключевые слова: информационная безопасность, большие данные, гетерогенные системы обработки данных, контроль доступа, верификация, темпоральная логика, TLA+