Спецификация модели управления доступом на языке темпоральной логики действий Лэмпорта (Александр Козачок, ISPRASOPEN-2018)