Аннотация доклада.

Такие методы и средства автоматизации процессов работы с формальными теориями, как нахождение и проверка правильности доказательств, активно развиваются в последние десятилетия. Однако до начала нахождения доказательств теорем и до проверки их правильности необходимо породить гипотезы, которые впоследствии станут теоремами. Специальные инструменты для порождения гипотез в импликативной форме хорошо известны и изучены в Анализе Формальных понятий (АФП). Используемая в АФП формализация может найти применения в самых разных областях науки и техники. Однако существующие методы не являются достаточно гибкими для применения и процесс автоматизации такого исследования недостаточно хорошо изучен и проиллюстрирован, что препятствует дальнейшему распространению АФП. Целью исследования, результаты которого представлены в докладе, является разработка методов и средств автоматизации исследования импликативных зависимостей на основе методологии АФП.

Аннотация доклада.

Теория систем переписывания представляет эффективный аппарат для решения ряда важных проблем информатики, искусственного интеллекта и компьютерной алгебры. При определении системы переписывания отправной точкой обычно является эквациональная теория, множество правил которой состоит из равенств. Доклад посвящен задаче построения, исследования и компьютерной реализации класса алгебраических систем (LP-структур), в полной мере отражающего семантику условной эквациональной теории, с целью обоснования и автоматизации эквивалентных преобразований, оптимизации и верификации такой теории.

Построен класс эквациональных LP-структур, обладающий новыми свойствами и адекватно отражающий семантику условных эквациональных теорий. Доказано существование и получен эффективный способ построения логической редукции эквациональных LP-структур. В приложениях он означает минимизацию соответствующих условных эквациональных теорий. Показано, что произвольная эквациональная LP-структура может быть приведена к каноническому виду. Впервые введено понятие продукционно-логического уравнения в эквациональной LP-структуре и обоснован способ его решения, что в приложении соответствует полному обратному выводу. Концепция уравнений может быть применена для верификации условных эквациональных теорий. Разработан и реализован программный продукт, обладающий новыми возможностями исследования и оптимизации условных эквациональных теорий.

Аннотация доклада.

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

Аннотация доклада.

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

Аннотация доклада.

Существующий взгляд сегодня на феномен информации противоречив и вызывает больше вопросов, чем позволяет ответить на уже имеющиеся. Странное отношение к определению этого феномена связано, видимо, с тем, что, имея на сегодня массу (около 400) различных определений этого феномена, человечество не имеет единого мнения по этому вопросу - вот уже почти 100 лет. Может возникнуть впечатление, что человечество с этим примирилось, в связи с исчерпанием усилий по пониманию сути данного вопроса. С другой стороны и тоже, в связи в этим, важность этого вопроса ушла в тень и, создалось впечатление, что эта тема потеряла актуальность за отсутствием новых идей. Даже, поднимается вопрос:- ну, какая разница – пользуемся же? Однако, последние попытки пытливых умов «пощупать» информацию и другие факты, говорят о необходимости глубокого понимания этого феномена. Поэтому, и не только в связи с этим, продолжим дискуссию о том:- что, - как, - когда, - почему и в виде чего мы можем представить себе эту «не энергию и не материю».

Аннотация доклада.

В докладе представлен усовершенствованный метод обратного логического вывода, основанный на решении уравнений в LP-структурах – специальном классе алгебраических систем. Стратегия релевантного обратного вывода обеспечивает минимизацию количества обращений к внешнему источнику информации (базе данных или интерактивному пользователю). Запросы по возможности отправляются для тех фактов, которые действительно необходимы при выводе. Отрицательный ответ на единственный запрос исключает все последующие запросы об элементах связанного подмножества фактов. Кроме того, при LP-выводе предпочтение отдается тестированию множеств фактов минимальной мощности. Концепция LP-вывода также применима для верификации знаний. Исследуются вопросы выбора параметров релевантности. Анализируется применение параллельных вычислений. Описывается программная реализация. Представленные возможности демонстрируются на множестве тестовых примеров. Результаты экспериментов обработаны методами математической статистики.

Аннотация доклада.

В докладе рассматривается задача «структура – свойство», которая состоит в выявлении зависимостей между структурой химического соединения и его физико-химическими свойствами (QSPR), а также биологической активностью (QSAR). Задача «структура – свойство» является актуальной задачей распознавания образов и для её решения в настоящий момент активно используются методы машинного обучения. Актуальным является решение задачи «структура – свойство», реализующее построение и использование правил отказа от прогноза для конкретных моделей, а также автоматическую адаптацию дескрипторного описания под задачу прогнозирования конкретной биологической активности или физико-химического свойства. В докладе представлены результаты разработки метода прогнозирования свойств химических соединений, получившего название адаптивной двухфазной схемы решения задачи «структура – свойство», а также универсального алгоритма построения ограничений допустимости и алгоритмов независимой адаптации дескрипторного описания под задачи прогнозирования свойств химических соединений и построения ограничений допустимости.

Аннотация доклада.

Локальные поставщики сетевых услуг (лПСУ) предоставляют пользователям разнообразные сервисы, требующие передачи больших объемов данных (IP-телефония, видео-конференции, сетевые хранилища данных, виртуальные рабочие пространства и т. п.). Постоянный рост сложности сетей требует развития формальных методов их анализа на основе измерительной информации о потоках данных, полученных в условиях реальных рабочих нагрузок, что, в свою очередь, требует разработки экспериментальных платформ (ЭП) для получения этой информации путем встраивания их в существующие сети.

Для исследования эффективности использования сетей в бизнес процессах ЭП должна предоставлять доступ к данным измерений, структурированным как по сетевым устройствам, так и по элементарным пространственным, организационным и аппаратно-программным единицам ИКТ-инфраструктуры предприятия и их произвольным агрегациям.

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

Аннотация доклада.

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

В докладе будет представлен разработанный автором алгоритм и его программная реализация, основанные на идее разбиения каждого предложения на части «что», «где», «когда» и вычисления смысловой близости предложения путем анализа близости этих частей по отдельности.

Аннотация доклада.

Традиционно механизм управления доступом рассматривается как основа обеспечения безопасности компьютерных систем, в особенности защищенных операционных систем (ОС) с мандатным управлением доступом. Для научного исследования свойств этого механизма за более чем 40 лет построены десятки теоретических моделей. Однако большинство отечественных разработчиков защищенных ОС используют (как правило, только формально) для реализации механизма управления доступом устаревшие, неадекватные условиям функционирования современных ОС модели (например, классическую модель Белла-ЛаПадулы), что не позволяет повысить доверие к безопасности получаемого решения. В связи с этим может оказаться полезным анализ результатов построения механизма управления доступом в отечественной защищенной ОС Astra Linux Special Edition на основе новой мандатной сущностно-ролевой ДП-модели (сокращенно, МРОСЛ ДП-модели), в которой обеспечивается сочетание мандатного управления доступом, мандатного контроля целостности с перспективным ролевым управлением доступом. В МРОСЛ ДП-модели применен новый подход, когда роли и административные роли представляются как аналоги сущностей-контейнеров, что позволяет задать в ОС иерархию ролей в виде виртуальной файловой системы. Все вносимые в модель элементы рассматриваются, во-первых, с точки зрения их реализации в ОС, во-вторых, с учетом перспектив дальнейшего строгого теоретического обоснования свойств моделируемой ОС (формулирования алгоритмически проверяемых условий безопасности). Кроме того, модель разрабатывается с учетом обеспечения возможности с использованием методик верификации кода программ осуществить вывод и формальное обоснование корректности реализации модели непосредственно в программном коде механизма управления доступом защищенной ОС Astra Linux Special Edition.

Аннотация доклада.

Доклад посвящен описанию архитектуры программной системы организации распределенных вычислений на основе платформы Erlang/OTP. В докладе будет представлен опыт использования этой системы в составе виртуального полигона для моделирования grid- и cloud-инфраструктур.

Рассматривается следующая постановка задачи организации распределенных вычислений. Имеется динамически формируемый набор вычислительных узлов. На каждом таком узле может выполняться вычислительное задание. Вычислительное задание определяется именем программы (исполняемого файла) и аргументами командной строки. Результатом выполнения вычислительного задания является стандартный вывод программы. На каждом вычислительном узле запущен компонент целевой программной системы в виде отдельного Erlang/OTP приложения. Подобное приложение предоставляет возможность запустить процесс, под управлением которого будет выполнено вычислительное задание, а его результат будет доставлен потребителю. Потребитель имеет возможность получить текущий список узлов, на которых могут выполняться его вычислительные задания.

Аннотация доклада.

Формализм схем радикалов основан на концепции среды радикалов, предназначен для формализации проблемных областей сложных систем и ориентирован на программную реализацию. В докладе рассматриваются схемы радикалов, характерные для проблемной области создания прикладных программных средств, предназначенных для сложных систем. Акцент сделан на статическом аспекте схем радикалов – на рассмотрении «моментальных снимков» фрагментов («сечений») среды радикалов, представляющей проблемную область. Схемы радикалов сравниваются с конструкциями, характерными для некоторых известных инструментальных программных средств.

Аннотация доклада.

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