Публикации

В статье рассматривается семейство требований доверия к безопасности ADV_SPM «Моделирование политики безопасности», которое определяется стандартом ГОСТ Р ИСО/МЭК 15408-3-2013 «Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности». Обсуждаются задачи, решаемые этим семейством, и вопросы, которые возникают при попытке интерпретировать его требования. На простом примере представляется подход к формализации политик безопасности при помощи языка формальных спецификаций Event-B и инструментов платформы Rodin.

Рассматривается математическое моделирование фазовых переходов  в системе золь-гель с учетом теыенмя жидкости

Рассматривается построение полной математематической модели для процесса полимеризации фибрина с учетом гидродинамических течений

ecomposition is an important phase in the design of medium and large-scale systems. Various architectures of software systems and decomposition methods are studied in numerous publications. Presently, formal specifications of software systems are mainly used for experimental purposes; for this reason, their size and complexity are relatively low. As a result, in the development of a nontrivial specification, different approaches to the decomposition should be compared and the most suitable approach should be chosen. In this paper, the experience gained in the deductive verification of the formal specification of the mandatory entity-role model of access and information flows control in Linux (MROSL DP-model) using the formal Event-B method and stepwise refinement technique is analyzed. Two approaches to the refinementbased decomposition of specifications are compared and the sources and features of the complexity of the architecture of the model are investigated.

This paper proposes a new object model of data for the in-depth analysis of network traffic. In contrast to the model used by most modern network analyzers (for example, Wireshark and Snort), the proposed model supports data stream reassembling with subsequent parsing. The model also provides a convenient universal mechanism for binding parsers, thus making it possible to develop completely independent parsers. Moreover, the proposed model allows processing modified—compressed or encrypted—data. This model forms the basis of the infrastructure for the in-depth analysis of network traffic.

The issue contains papers accepted for presentation at the 10th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE 2016) held in Krasnovidovo, Mozhaysky District, Moscow Oblast, Russia on May 30-June 1, 2016. The paper selection was based on originality and contributions to the field. Each paper was peer-reviewed by at least three referees.

The colloquium’s topics include programming languages, software development tools, embedded and cyber-physical systems, software and hardware verification, formal methods, information security, and others.

This paper presents a memory model with nonoverlapping memory areas (regions) for the deductive verification of C programs. This memory model uses a core language that supports arbitrary nesting of structures, unions, and arrays into other structures and allows reducing the number of user-provided annotations as a result of region analysis. This paper also describes semantics of the core language and normalizing transformations for translating an input annotated C program into a program in the core language. In addition, an encoding is proposed for modeling the memory state of a core-language program with logical formulas as described by the model semantics of the core language. For the model semantics, the soundness and completeness theorems are proved. Additional constraints on the typing context of the core-language terms are described that determine the result of the region analysis enabling the complete modeling of a limited class of programs without using additional annotations. A proof sketch for the theorem stating completeness of the proposed region analysis for a limited class of programs is presented.

This paper considers the problem of the deductive verification of the Linux kernel code that is concurrent and accesses shared data. The presence of shared data does not allow applying traditional deductive verification techniques, so we consider how to verify such a code by proving its compliance to a given specification of a certain synchronization discipline. The approach is illustrated by the examples of a spinlock specification and a simplified specification of the read-copy-update (RCU) API.

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

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

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

Рассмотрены вопросы формализации описания образования тромбов в крови

В данной статье описан алгоритм обхода (извлечения полной информации о структуре) заранее неизвестного ориентированного графа при помощи неограниченного набора конечных автоматов, взаимодействующих при помощи обмена сообщениями и способных перемещаться вдоль дуг графа в соответствии с их ориентацией. В предположении об ограниченности времени работы базовых операций и времени пересылок отдельных сообщений общее время работы алгоритма в худшем случае ограничено O(m+nd), где n — число вершин графа, m — число его дуг, d — диаметр графа, причем эту оценку нельзя улучшить.