В статье предложен метод антивирусной защиты мобильных устройств, основанный на применении доверенных цифровых подписей и алгоритма (n, t)- пороговой доверенной цифровой подписи с арбитром. Особенность предложенного метода заключается в отсутствии необходимости устанавливать антивирусное программное обеспечение на мобильное устройство. Достаточно иметь программное обеспечение, проверяющее цифровые подписи, и располагать доступом в сеть Интернет. Метод реализуется на базе инфраструктуры открытых ключей (PKI), что позволяет минимизировать затраты при внедрении.

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

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

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

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

Рассмотрим линейную рекуррентную последовательность векторов {⃗

Получено обобщение одной классической теоремы К.Сексенбаева о полициклических группах. Сексенбаев доказал, что если полициклическая группа G аппроксимируема конечными p-группами для бесконечного множества простых чисел p, то она нильпотентна. Напомним, что группа G называется аппроксимируемой конечными p-группами, если для любого неединичного элемента a группы G существует гомоморфизм группы G на некоторую конечную p-группу, при котором образ элемента a отличен от 1. Одним из обобщений понятия полициклической группы является понятие группы конечного ранга. Напомним, что группа G называется группой конечного ранга, если существует целое положительное число r такое, что любая конечно порожденная подгруппа группы G порождается не более чем r элементами. Доказано следующее обобщение теоремы Сексенбаева: если группа G конечного ранга аппроксимируема конечными p-группами для бесконечного множества простых чисел p, то она нильпотентна. Более того, доказано, что если для каждого множества π, состоящего из почти всех простых чисел, группа G конечного ранга аппроксимируема конечными нильпотентными π-группами, то она нильпотентна. Для нильпотентной группы конечного ранга получено необходимое и достаточное условие аппроксимируемости конечными π-группами, где π — множество простых чисел.

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

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

В статье доказывается приводимость пространства M^ref_P³ (2; −1, 4, 2) модулей стабильных рефлексивных пучков ранга 2 с классами Черна c₁ = −1, c₂ = 4, c₃ = 2 на P³. Это первый пример приводимого пространства в серии пространств модулей стабильных рефлексивных пучков ранга 2 с c₁= −1, c₂ = 4, c₃ = 2m, m = 1, 2, 3, 4, 5, 6, 8. Найдены две неприводимые компоненты этого пространства, имеющие ожидаемую размерность 27, и дается их геометрическое описание посредством конструкции Серра.