Предлагается подход к построению и верификации программ логических контроллеров (ПЛК) для «дискретных» задач. Спецификация программного поведения проводится на языке темпоральной логики линейного времени LTL. Программирование осуществляется на языке ST (Structured Text) по LTL- спецификации. Анализ корректности LTL-спецификации производится с помощью программного средства символьной проверки модели Cadence SMV. Предлагаемый подход к программированию и верификации программ ПЛК демонстрируется на примере. Для дискретной задачи приводятся ST-программа, ее LTL-спецификация и SMV-модель.

Целью статьи является описание подхода к программированию ПЛК, который бы обеспечивал возможность анализа корректности ПЛК-программ с помощью метода проверки модели.

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

Рассматривается моделирование схем потоков работ (workflow) при помощи сетей Петри. Определяется класс сетей потоков работ с ресурсами (RWF- сетей) — обычных workflow-сетей, в которых дополнительно добавлено множество ресурсных позиций, содержащих какую-то начальную разметку (начальный ресурс). Ресурсы могут уничтожаться и производиться при срабатываниях переходов. Мы не накладываем ограничений ни на промежуточные, ни на финальные ресурсные разметки, поэтому сеть может порождать бесконечное множество различных достижимых состояний. RWF-сеть с данной начальной ресурсной разметкой называется бездефектной, если, во-первых, она всегда корректно завершает свою работу, и, во- вторых, любое увеличение начального ресурса не нарушает свойства корректного завершения. Неразмеченная RWF-сеть бездефектна, если она бездефектна при некоторой начальной ресурсной разметке. В данной работе доказана разрешимость обоих вариантов бездефектности для важного подкласса RWF- сетей — сетей с одномерным ресурсом (одной ресурсной позицией). Также представлен алгоритм вычисления наименьшего бездефектного ресурса.

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

Предложен алгоритм (n, t)-пороговой доверенной цифровой подписи с Арбитром, позволяющий доверителю делегировать множеству P, состоящему из n участников, возможность подписывать сообщения от его имени. Доверитель разделяет доверенность между участниками P, таким образом, что только t (t < n) участников и Арбитр, объединившись, могут вычислить подпись. Таким образом, для подписания документа требуется согласие не менее чем t участников. Арбитр участвует в алгоритме в качестве третьего доверенного лица. Он завершает вычисление подписи на основании информации, полученной от t участников. Проверяющий может идентифицировать участников множества P и доверителя. Главной особенностью алгоритма является то, что n участников, вычисляя подпись, не могут вычислить значения секретного ключа доверителя и доверенности.

В 1929 году Б.Н. Делоне привел полную классификацию комбинаторных типов схождений параллелоэдров в гранях коразмерности 3. Оказалось, что любое схождение дуально одному из следующих пяти трехмерных многогранников: тетраэдру, четырехугольной пирамиде, октаэдру, треугольной призме или параллелепипеду. В статье приводится новое доказательство этого результата, основанное на формуле Эйлера. С использованием этой классификации получены некоторые дальнейшие свойства граней коразмерности 3 разбиений пространства на параллелоэдры. Показано, что для граней коразмерности 3 выполнена гипотеза о размерности, т.е. аффинная оболочка центров парал- лелоэдров, сходящихся в грани коразмерности 3, трехмерна. Наконец, установлено, что центры параллелоэдров, сходящихся в грани коразмерности 3, порождают трехмерную подрешетку индекса 1.

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

Предлагается новый подход к множественной аутентификации пользователя в разнородных информационных системах. Описанное решение основано на применении беспроводных ключей — специальных устройств, которые идентифицируют пользователя посредством передачи запрашиваемой ключевой информации с использованием беспроводной связи. Ключевым свойством предложенного подхода является неинтерактивность: вместо двухсторонней аутентификации ключа и информационной системы для защиты данных, хранящихся на ключе, предлагается использование специального алгоритма шифрования. Разработанный алгоритм построен на комбинации стойких криптографических примитивов, что исключает возможность неавторизованным участникам системы читать данные других пользователей, даже при наличии физического доступа к памяти ключа. Указанный подход не требует вычислительной мощности или питания на стороне ключа и не вовлекает пользователя в процесс аутентификации, что позволяет использовать в качестве ключа USB носитель или пассивную NFC метку. Для доказательства корректности работы системы было разработано программное обеспечение, реализующее описанную систему аутентификации для технологий USB и NFC. Также было проведено качественное сравнение полученного решения с существующими аналогами.

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

Рассматривается понятие программно-конфигурируемой сети. Вначале даётся короткая историческая справка о понятии программно-конфигурируемой сети как научно-технической концепции, кем оно было введено и что означает. Авторы статьи рассматривают технологию программно-конфигурируемых сетей как один из возможных этапов и направлений развития сетевых парадигм в целом, не абсолютизируя роли этой технологии. Наряду с достоинствами отмечаются и недостатки программно-конфигурируемых сетей, рассматриваются возможные варианты развития программно-конфигурируемых сетей в контексте гибридизации с другими технологиями, в частности - гибридизация MPLS и SDN. Значительное внимание уделяется протоколу OpenFlow. В конце статьи рассмотрены существующие библиотеки для программной реализации управления программно-конфигурируемой сетью с использованием протокола OpenFlow. Все эти библиотеки предоставляют API для создания модульных приложений управления программно-конфигурируемыми сетями. Для сравнения производительности библиотек приведены результаты сравнительных тестов по пропускной способности и латентности.

Рассмотрены основные подходы по конструктивному созданию открытого сетевого ресурса «Предметно-специфицированного тезауруса по поэтологии», который является одним из уровней информационно-аналитической системы русской поэзии (ИАС РП). Под поэтологией будем понимать группу дисциплин, ориентированную на всестороннее теоретическое и историческое изучение поэзии. ИАС РП будет использоваться в качестве инструмента для широкого спектра исследований, позволяющего определять характерные признаки анализируемых произведений поэзии. Таким образом, тезаурус соответствует базе знаний, из которой будут заимствоваться исходные данные для обучения системы. Описан подход по формированию базы знаний. Тезаурус представляет собой веб-ресурс, включающий предметно-ориентированный справочник, информационно-поисковый инструмент и инструмент для дальнейших анали- тических исследований. Детально рассмотрена проработка терминологического словника, состоящего из 3 тысяч терминов, и комплекса семантических полей. На основании этого представлен rdf-граф предметно-специфицированного тезауруса по поэтологии, содержащий 9 типов объектов и различные виды отношений между ними. Для реализации ресурса применяются Wiki-технологии, что дает возможность хранить данные в форматах Semantic Web.

Одной из главных тенденций последних лет в проектировании программного обеспечения стал переход к парадигме Software as a Service (SaaS), которая несет ряд неоспоримых преимуществ как для компаний-разработчиков ПО, так и для конечных пользователей. Однако вместе с этими преимуществами данный переход несет и новые архитектурные вызовы, одним из которых является организация хранилища данных, которое могло бы удовлетворить нужды компании-провайдера услуг, обеспечив достаточно простой прикладной интерфейс для разработчиков. Для разработки эффективного решения в данной области следует принимать во внимание особенности архитектуры облачных приложений, ключевыми из которых являются потребность в простом масштабировании и быстрой адаптации к меняющимся условиям. В данной работе проводится краткий анализ существующих проблем в области организации облачных систем хранения данных, основанных на реляционной модели, а также предлагается концепция кластера РСУБД, предназначенного для обслуживания приложений с мультиклиентской архитектурой. Кроме того, в статье дается описание имитационной модели подобного кластера, а также основных этапов ее разработки и принципов, заложенных в ее основу.