Авторитетность издания
ВАК - К1
RSCI, ядро РИНЦ
Добавить в закладки
Следующий номер на сайте
№1
Ожидается:
24 Декабря 2024
Статьи журнала №4 2015
21. Инъектор сбоев для тестирования микропроцессоров типа система на кристалле к одиночным сбоям [№4 за 2015 год]Автор: Чекмарёв С.А. (zaq259@yandex.ru) - Сибирский государственный аэрокосмический университет им. академика М.Ф. Решетнева (инженер);
Аннотация: Для тестирования механизмов обнаружения и коррекции сбоев используют иъектирование ошибок в памяти микропроцессора. Инъектирование имитирует результат воздействия космических тяжелых заряженных частиц. В работе рассмотрен IP-блок инъектора сбоев. IP-блок вносит одиночные сбои в память микропроцессора типа система на кристалле. Приведены схема инъектора сбоев, состав модулей, машина состояний, кратко описана работа во всех режимах инъектирования. Инъектор позволяет вносить сбои в регистровый файл, кэш-память и внешнюю память в различных режимах. Доступны следующие режимы: режим с остановкой и без остановки процессора со случайным или предопределенным покрытиями сбоем. IP-блок инъектора сбоев был применен в СнК-процессоре LEON3. В статье описаны процедуры инъектирования сбоев в память LEON3. Доступ к внутрикристальной памяти осуществляется через DSU-интерфейс. DSU является ведомым устройством на AMBA AHB-шине. Через его регистры инъектор сбоев может остановить работу процессора, модифицировать содержимое внутренней памяти, возобновить работу ПО. Для доступа к внешней памяти процессора LEON3 используется контроллер памяти. Во время эксперимента инъектор собирает статистическую информацию о внесенных и обнаруженных сбоях. Анализ результатов позволяет сделать вывод о чувствительности микропроцессора к одиночным сбоям в памяти. По завершении тестирования инъектор сбоев может быть исключен из состава микропроцессора типа система на кристалле, не оставив в нем никаких «следов».
Abstract: Error injection to the microprocessor memory is used to test fault detection and correction tools. Injection simulates the result of space heavy charged particles influence. This paper describes the developed failure injector IP-core. IP-core makes single event upsets to the memory of the system-on-a-chip (SoC) microprocessor. The paper describes a failure injector scheme, modules structure, a state machine, the work in all injection modes. The injector allows us to add failures to a register file, cache and external memory in different modes. Available modes are: with or without a microprocessor stop the processor with a random failure or predetermined by covering. Failure injector IP-core was applied to the SoC processor LEON3. The article describes the failure injection procedures in LEON3 memory. DSU interface helps to access the on-chip memory. DSU is a slave interface to the AMBA AHB bus. Using its registers the failure injector can stop the processor, modify its internal memory contents, and resume running software. A memory controller is used to access LEON3 external memory. During the experiment the injector collects statistical data on injected and found faults. The analysis of the results leads to a conclusion about the microprocessor sensitivity to single event upsets in the memory. After testing a failure injector can be excluded from the SoC microprocessor without any traces left.
Ключевые слова: инъектор сбоев, leon3, система на кристалле, инъектирование, одиночные сбоиKeywords: seu injector, leon3, system on a chip, injection, single event effects
Просмотров: 9634
22. Подход к развитию системы управления тестированием программных средств [№4 за 2015 год]
Авторы: Корнюшко В.Ф. (arbenina@mitht.ru) - Московский государственный университет тонких химических технологий им. М.В. Ломоносова (профессор), доктор технических наук; Костров А.В. (akostrov@rambler.ru) - Владимирский государственный университет им. Александра Григорьевича и Николая Григорьевича Столетовых (профессор), доктор технических наук; Породникова П.А. (polina.porodnikova@mail.ru) - Владимирский государственный университет им. Александра Григорьевича и Николая Григорьевича Столетовых (аспирант);
Аннотация: В статье поставлена задача формирования подхода к управлению уровнем развития системы управления тестированием (СУТ) в составе системы управления бизнес-процессами разработки ПО в условиях проектного предприятия. Предложено выделить в составе бизнес-процессов разработки ПО бизнес-процесс тестирования, а в составе системы управления разработкой – подсистему управления тестированием как самостоятельные. Рассмотрены особенности организации тестирования в типовых моделях разработки ПО, для различных моделей разработки построены варианты организации выполнения по этапам основных процессов: рецензирование, Review (R); разработка тестов, Test Design (D); выполнение тестов, Test Execution (E); отчетность о тестировании, Test Report (O). Показана роль оценки уровня развития СУТ в процессах управления развитием, предложен подход к определению оценки уровня развития СУТ. Подход основан на определении оценки уровня развития СУТ в условиях различных моделей разработки ПО, прежде всего с использованием экспертной оценки. В качестве методической основы использована классификация стадий зрелости проектного управления. Рассмотрены особенности и возможности применения как прямой, так и многокритериальной экспертной оценки. Предложено отображать вербальное описание стадий зрелости СУТ множеством частных количественных критериев, часть из которых может определяться инструментальными методами; для оценки значений других предлагается проводить многокритериальную экспертизу с участием узких специалистов по профилю каждого из критериев. Рассмотрены варианты алгоритмов одноуровневого определения глобального критерия уровня развития на основе множества оценок частных критериев: вычисление длины вектора в эвклидовом пространстве и определение суммы взвешенных оценок частных критериев. Предложены двухуровневый вариант упорядочения частных критериев и соответствующие алгоритмы обработки множества их оценок, а также наглядная визуализация результатов оценки уровня развития СУТ. Разработанный на основе многокритериальной экспертной оценки подход позволяет определять степень зрелости СУТ ПО и целенаправленно управлять ее развитием.
Abstract: The paper considers the problem of creating an approach to testing management system (TMS) development control as a part of software development business process management system in a project company. The authors suggest to separate software testing process as an independent business process, so software development management system has a testing management subsystem. The paper reviews the features of testing management in typical software development models. There are the variants of basic testing processes implementation: Review (R); Test Design (D); Test Execution (E); Test Report (O). The article shows the role of TMS development evaluation in the development management processes, and provides the approach to its evaluation. The approach is based on TMS development evaluation for different software development models, expert evaluation in particular. Classification of project management maturity stages is used as a methodological basis. The paper considers the features and applicability of both direct and multi-criteria expert evaluation. The authors suggest displaying a verbal description of TMS maturity stages as a set of private quantitative criteria; some of them can be determined by instrumental methods. To evaluate the others it is proposed to make multi-criteria assessment with the assistance of field experts according to each criterion. The paper considers the variants of single-level algorithms to determine a development level global criteria based on multiple assessments of partial criteria: calculation of the length of the vector in Euclidean space and determining the amount of the weighted assessments of partial criteria. The paper proposes a two-level ordering of the partial criteria and corresponding algorithms for processing their set of estimates, as well as a visualization of the results of the TMS development evaluation. The described approach allows assessing the software TMS maturity and managing its development.
Ключевые слова: бизнес-процесс, подход, тестирование, глобальный критерий, частный критерий, уровень развития, программные средства, многокритериальная оценка, экспертная оценка, система управления, оценкаKeywords: business-process, approach, testing, global criterion, partial criterion, development level, software, multi-criteria estimate, expert estimation, a control system, estimation
Просмотров: 11925
23. Задачи обеспечения устойчивости функционирования распределенных информационных систем [№4 за 2015 год]
Автор: Есиков Д.О. (mcgeen4@gmail.com) - Тульский государственный университет (аспирант);
Аннотация: Предложены способы обеспечения устойчивости функционирования распределенных информационных систем. Формализованы задачи обеспечения устойчивости функционирования распределенных информационных систем в составе: математическая модель оптимизации распределения элементов ПО функциональных задач по узлам сети, математическая модель оптимизации распределения информационных ресурсов по центрам хранения и обработки данных, математическая модель определения рационального уровня расходов на формирование комплекса средств хранения данных в центрах хранения и обработки информации, математическая модель оптимизации состава технических средств системы хранения и обработки данных, математическая модель оптимизации распределения резерва информационных ресурсов по центрам хранения и обработки данных. Показано, что они относятся к классу задач дискретной оптимизации, дана их характеристика. Предложен порядок применения комплекса математических моделей обеспечения устойчивости функционирования распределенных информационных систем с указанием входных и выходных данных для каждой модели. Для решения разработанных задач предложено использовать программный комплекс, реализующий метод ветвей и границ по решению задач дискретной оптимизации с булевыми переменными с применением алгоритма предварительного определения порядка ветвления переменных на основе использования теории двойственности. Применение теории двойственности в методе ветвей и границ позволяет существенно усилить отсев бесперспективных вариантов и сократить время решения задач по сравнению с традиционным методом в среднем в 8 раз. Приведены особенности практического использования разработанного комплекса математических моделей на стадиях проектирования, эксплуатации и совершенствования жизненного цикла распределенных информационных систем.
Abstract: The paper considers the ways to ensure distributed information systems sustainability. It formalizes the problems of ensuring sustainability of distributed information systems, which consist of: a mathematical optimization model for functional tasks software elements distribution according to network nodes; a mathematical optimization model for information resources distribution according to data storage and processing centers; a mathematical model for determination of a reasonable expenditure level to form data storage facilities; a mathematical optimization model of technical means for data storage and processing; a mathematical optimization model for information resources reserve distribution on data storage and processing centers. The article shows that they belong to discrete optimization problems and gives their characteristics. It also proposes a procedure for applying a complex of mathematical models to ensure distributed information systems sustainability with indication of input and output data for each model. To solve the abovementioned problems the authors suggest using a software package, which implements the branch and bound method to solve discrete optimization problems with Boolean variables using the algorithm of branching variables predetermined order based on the duality theory. The duality theory in the branch and bound method significantly enhances the screening of unpromising options and reduces the time for solving problems compared with the traditional method on average in 8 times. The paper gives the special aspects of practical use of the developed mathematical model complex during design, maintenance and update of distributed information systems life cycle.
Ключевые слова: устойчивость функционирования, оптимизация по парето, дискретная оптимизация, математические модели, распределенная информационная системаKeywords: operational sustainability, pareto optimization, combinatorial optimization, mathematical models, distributed information system
Просмотров: 10712
24. Реализация процесса поиска решения по модифицированному алгоритму Rete для нечетких экспертных систем [№4 за 2015 год]
Авторы: Михайлов И.С. (fr82@mail.ru) - Национальный исследовательский университет «Московский энергетический институт», кандидат технических наук; Зо Мин Тайк (zawgyi86@gmail.com) - Национальный исследовательский университет «Московский энергетический институт» (аспирант);
Аннотация: В работе рассматриваются основные понятия теории нечетких продукционных экспертных систем. Нечеткие продукционные экспертные системы базируются на наборе правил, представленном в терминах лингвистических переменных. В качестве механизма нечеткого вывода предлагается разработанная модификация алгоритма Rete для нечеткой базы правил. Разработанная модификация обеспечивает ускорение процесса работы системы за счет однократного вычисления одинаковых условий в правилах, а также позволяет формулировать правила и заключения на ограниченном естественном языке. Разработанная формальная модель дерева решений модифицированного алгоритма Rete для нечеткой продукционной базы знаний состоит из множеств вершин-условий, вершин-следствий, отношений между вершинами и отношений для описания правил нечеткой экспертной системы. Созданный алгоритм обрабатывает правила нечеткой базы правил и преобразует их в формат формальной модели дерева решений модифицированного алгоритма Rete. На каждом этапе работы алгоритма выполняется построение нечетких оценок истинности вершин дерева решений с помощью нечетких операторов, что позволяет формулировать условия и следствия в базе правил, а также результаты работы алгоритма поиска решения на ограниченном естественном языке. Также одинаковые условия объединяются при построении дерева решений, что обеспечивает ускорение обработки дерева решений по сравнению с последовательным просмотром правил экспертной системы. Рассмотрен пример работы нечеткой продукционной экспертной системы, функционирующей на основе предложенной модификации алгоритма Rete, показана эффективность предложенного метода.
Abstract: The paper considers the basic concepts of fuzzy production expert systems. Fuzzy production expert systems are based on a set of rules presented in terms of linguistic variables. The authors suggest the developed Rete algorithm modification for a fuzzy rule base as a fuzzy inference tool. This modification accelerates systems operation due to a single computing of the same conditions in the rules. It also formulates the rules and conclusions in the limited natural language. The modified Rete algorithm formal decision tree model for a fuzzy production knowledge base consists of a set of vertex-conditions, vertexsolutions, the relationship between vertices and relations to describe the fuzzy expert system rules. The created algorithm processes the rules from the fuzzy rule base and converts them into the decision tree modified Rete algorithm formal model. Rete algorithm modification is different from a classical algorithm as it is used for fuzzy variables. Therefore, each stage of the algorithm includes building the decision tree vertices fuzzy truth values using fuzzy operators. This allows formulating the conditions and consequences in the rule base, as well as the solutions in the limited natural language. The same conditions are combined during decision tree construction. It accelerates decision tree processing comparing to sequential viewing of expert system rules. The paper describes an operating example of the production fuzzy expert system, which works on the basis of the proposed Rete algorithm modification. It also displays the effectiveness of the proposed method.
Ключевые слова: модификация алгоритма rete, алгоритм rete, нечеткая база правил, нечеткая экспертная системаKeywords: rete algorithm modification, rete algorithm, fuzzy rule base, fuzzy expert system
Просмотров: 10612
25. Разработка и исследование параллельного алгоритма муравьиных колоний для криптоанализа блочных криптосистем [№4 за 2015 год]
Авторы: Чернышев Ю.О. (sergeev00765@mail.ru) - Донской государственный технический университет (профессор), доктор технических наук; Сергеев А.С. (sergeev00765@mail.ru) - Донской государственный технический университет, кандидат технических наук; Рязанов A.H. (sergeev00765@mail.ru) - Донской государственный технический университет (аспирант); Капустин C.А. (skappa@yandex.ru) - Филиал Военной академии связи (доцент), кандидат технических наук;
Аннотация: В статье рассматривается возможность параллельной реализации алгоритмов муравьиных колоний для криптоанализа блочных криптосистем. Отмечена актуальность нового научного направления «природные вычисления», приведена структурная схема криптоанализа стандарта DES с использованием метода муравьиных колоний. Приводится описание параллельной версии алгоритма криптоанализа на основе информационно-логической граф-схемы, матриц следования, логической несовместимости и независимости. На основе методики определения числа процессоров, сущность которой заключается в нахождении максимального множества взаимно независимых операторов в матрице независимости, последовательном проведении фиктивных связей в информационно-логическом графе, не увеличивающих длину критического пути, определено минимальное число процессоров, необходимых для реализации алгоритма криптоанализа. Отмечается, что отличительной особенностью применения биоинспирированных методов криптоанализа является возможность использования самого алгоритма шифрования (или расшифрования) в качестве целевой функции для оценки пригодности ключа, определенного с помощью генетических операций. Вследствие этого при использовании биоинспирированных методов криптоанализа процесс определения секретного ключа (например, при криптоанализе 2-го типа) зависит не столько от сложности шифрующих преобразований, сколько от самого биоинспирированного метода, который должен обеспечивать достаточное разнообразие генерации ключей, что свидетельствует об актуальности задачи исследования возможности применения биоинспирированных алгоритмов (в частности, методов генетического поиска) для криптоанализа блочных криптосистем.
Abstract: The article considers the possibility of parallel implementation of ant colonies algorithms for block cryptosystems cryptanalysis. The authors specify that a new scientific direction “natural calculations” is relevant, provide the block diagram of DES standard cryptanalysis using a method of ant colonies. The parallel version of cryptanalysis algorithm is described on the basis of a data-logical flow graph, sequence matrices, logical incompatibility and independence. The minimum number of the processors for a cryptanalysisis algorithm is defined on the basis of a technique of defining the number of processors. This technique includes finding of a mutually independent operators maximal set in an independence matrix, consecutive fictive linking in a data-logical graph provided that these links don\'t increase a critical way length. A bioinspired cryptanalysis method application is distinguished by the possibility of using an encryption (decryption) algorithm as an objective function of key assessment defined by genetic operations. Therefore, when using the bioinspired cryptanalysis methods the process of private key definition (for example, at type 2 cryptanalysis) depends not on encryption complexity, but on the bioinspired method itself that provides a sufficient variety of key generation. This proves the relevance of the problem connected with a research on the bioinspired algorithms application possibility for block cryptosystems cryptanalysis.
Ключевые слова: множества взаимно независимых операторов, матрица независимости, матрица логической несовместимости, муравьиный алгоритм, криптоанализKeywords: mutually independent operators maximal set, matrix of independence, matrix of logical incompatibility, ant colony optimization, cryptanalysis
Просмотров: 11776
26. Оценка надежности программного обеспечения методами дискретно-событийного моделирования [№4 за 2015 год]
Авторы: Бутакова М.А. (butakova@rgups.ru) - Ростовский государственный университет путей сообщения (профессор, декан), доктор технических наук; Гуда А.Н. (guda@rgups.ru ) - Ростовский государственный университет путей сообщения (профессор, проректор), доктор технических наук; Чернов А.В. (avche@yandex.ru) - Ростовский государственный университет путей сообщения (профессор, зав. кафедрой), доктор технических наук; Чубейко С.В. (greyc@mail.ru) - Ростовский государственный университет путей сообщения, кандидат технических наук;
Аннотация: В статье рассматривается дискретно-событийное моделирование и представлены его отличительные особенности от других видов моделирования. Основное отличие – отсутствие привязки ко времени: достаточно соблюдать последовательность наступления событий, при этом не важно, какой временной промежуток будет между событиями. Дано определение модели дискретно-событийной системы с дополнением ее модельными часами, которые воспроизводят хронологию событий. Решается важная задача генерации списка событий различными способами: объектно-ориентированное и процессно-ориентированное исполнение событий. Подробно рассматриваются оба способа: приводятся иллюстрация, алгоритм и элемент программной реализации. События могут объединяться в группы, которые называются процессами. Процессно-ориентированное моделирование сложнее объектно-ориентированного, так как имеется планировщик процессов. Также в статье рассматривается оценка надежности ПО, базирующаяся на дискретно-событийном подходе. Данный подход основан на идее роста надежности ПО. Поиск ошибок моделируется случайным точечным процессом. При обнаружении ошибки она устраняется, тем самым ПО становится более надежным. Моделирование делится на две части: генерация процессов, имитирующих появление ошибок в ПО, и оценка системной надежности компонентного ПО. В статье рассматриваются варианты расчета вероятности возникновения ошибки в зависимости от структуры программ: последовательная, разветвляющаяся, циклическая и параллельная структура программного компонента. Для каждого варианта представлен иллюстрирующий рисунок и приведена вычислительная схема. Для циклической схемы программного компонента используется вычислительная схема последовательного компонента, так как это своего рода однотипные повторы последовательной структуры программного компонента.
Abstract: The article considers discrete-event modeling and presents its distinctive features comparing to other types of modeling. The main difference is a lack of time reference, i.e. it is enough to keep the sequence of events, and thus the time interval between events isn\'t important. The authors give the definition of a discrete-event system model and add model time, which reproduce the course of events. The article solves the important problem of the event list generation in various ways: object-based and the process-based execution of events. Both ways are considered in detail with the illustration, algorithm and a program implementation element. Events can be united into groups called processes. The process-based modeling is more difficult than object-based as there is a process scheduler. The article also considers the assessment of software reliability based on discrete-event approach. This approach is based on the idea of software reliability growth. Bug scanning is modeled by a stochastic point process. A detected bug is eliminated, thereby the software becomes more reliable. Modeling has two parts: generation of the processes, which imitate introducing bugs in the software, and an assessment of component software system reliability. The paper considers options of calculating bug probability depending on program structure: consecutive, branching, cyclic and parallel. Each option has an illustration and a computation scheme. The cyclic scheme of a software component has the computation scheme of a consecutive component as it is some kind of same-type repetitions of a software component consecutive structure.
Ключевые слова: структура программного компонента, надежность программного обеспечения, процессно-ориентированное моделирование, событийно-ориентированное моделирование, искретно-событийное моделированиеKeywords: software structure, software reliability, process-based modeling, event-based modeling,
Просмотров: 7759
27. Методический аппарат анализа и синтеза комплекса мер разработки безопасного программного обеспечения [№4 за 2015 год]
Авторы: Барабанов А.В. (ab@cnpo.ru) - НПО «Эшелон» (директор), кандидат технических наук; Марков А.С. (mail@cnpo.ru) - НПО «Эшелон» (доцент, генеральный директор), кандидат технических наук; Цирлов В.Л. (vz@cnpo.ru) - НПО «Эшелон» (доцент, исполнительный директор ), кандидат технических наук;
Аннотация: Рассмотрены актуальные вопросы стандартизации серийного производства безопасных программных изделий. Исследованы организационно-технические меры по снижению количества уязвимостей при разработке и сопровождении ПО функционирования автоматизированных систем в защищенном исполнении. Проведена систематизация стандартов и рекомендаций в области разработки безопасного ПО. Выполнен анализ применимости существующих методических подходов к разработке безопасного ПО при проведении оценки соответствия требованиям безопасности информации, в том числе при сертификации программных средств. Показана целесообразность гармонизации разрабатываемых нормативных требований и практических мер с методологиями международных стандартов по линии ISO 15408 и ISO 12207. Введено понятие безопасного ПО. Разработан базовый набор требований, позволяющий проводить и оценку соответствия процессов разработки ПО требованиям к безопасному ПО. При этом обосновано, что набор требований должен опираться прежде всего на принятые политики безопасности и актуальные угрозы. Приведен пример разрабатываемых требований. Разработана оригинальная концептуальная модель анализа и синтеза комплекса мер разработки безопасного ПО, опирающаяся на набор формируемых требований. Показано, что концептуальная модель предоставляет разработчикам ПО возможность научно обоснованного выбора мер разработки ПО. Разработана общая методика выбора комплекса мер безопасной разработки ПО. Представлены косвенные подтверждения эффективности предлагаемого подхода. Отмечено, что предложенный подход лег в основу разработки национального стандарта в области разработки и производства безопасного ПО.
Abstract: The paper considers important issues of secure software products standardization of serial production. The authors analyze organizational and technical measures aimed to reduce the number of vulnerabilities when developing and maintaining secure automated systems software. They also systematize standards and guidelines for secure software development. The authors analyze the applicability of the existing methodological approaches to secure software development during information security assessment (including for the software certification). They show harmonization expediency of the developed regulations and practical measures with the international standards like ISO 15408 and ISO 12207.The paper introduces the concept of secure software. There also is a basic set of requirements to assess compliance of the secure software development process. In this case the set of requirements should be based on information security policies and current threats. There is an example of developed requirements. The authors developed the original conceptual model for the analysis and synthesis of secure software development controls based on a set of generated requirements. The conceptual model gives software developers the ability of science-based choice of software development methods. The authors suggest a general method of selecting a secure software development set. There is the indirect evidence of the proposed approach effectiveness. It is noted that the proposed approach was the basis for a national standard regarding security software development.
Ключевые слова: механизмы безопасности приложений, общие критерии, уязвимости, безопасная программная инженерия, безопасное производство программ, безопасный жизненный цикл, безопасность программ, защита информацииKeywords: application security controls, common criteria, attack, ecure software engineering, software development security, secure lifecycle, security software, security of the information
Просмотров: 13725
28. Эквациональная характеристика формул LTL [№4 за 2015 год]
Авторы: Кораблин Ю.П. (y.p.k@mail.ru) - Российский государственный социальный университет, г. Москва (профессор), доктор технических наук; Шипов А.А. (a-j-a-1@yandex.ru) - Московский технологический университет (МИРЭА) (старший инженер-программист), кандидат технических наук;
Аннотация: Программные системы с каждым днем становятся все более сложными и комплексными, поэтому требуются такие инструменты, которые позволяли бы относительно легко выполнять проверку их работы на соответствие заданным спецификациям, особенно, когда речь идет о больших и распределенных программных системах. Для описания проверяемых условий верифицируемых моделей сегодня используются такие механизмы, как логика линейного времени LTL и логика ветвящегося времени CTL. Однако, как показывает практика, с помощью данных механизмов можно сформулировать лишь относительно небольшое множество однотипных условий, что может существенно усложнить процесс верификации или же сделать его вовсе неэффективным для модели конкретной системы. Проблема корректной формулировки проверяемых на модели свойств является одной из ключевых, так как от этого будет зависеть весь процесс верификации. Таким образом, наличие мощных инструментов и методов, позволяющих однозначно формулировать широкий класс проверяемых свойств, является необходимым требованием для достижения наилучших результатов. В статье предложен механизм, использование которого позволяет существенно расширить группу условий, формулируемых по отношению к проверяемым моделям. Данный эффект достигается путем расширения выразительности логики линейного времени LTL с помощью предлагаемого в статье метода, что в итоге позволяет увеличить эффективность процесса верификации. Теоретический материал статьи подкреплен рядом наглядных примеров работы данного метода, демонстрирующих его практичность. Также приведен пример верификации свойств, сформулированных на основе предложенного метода, для конкретной модели.
Abstract: sian Federationn State Social University, Vilgelma Pika St. 4, Moskow, 129256, Russian Federation) Аbstract. Day by day software systems are becoming more and more complex. Therefore, we need to have some useful instruments to check their capability according to specifications, especially large distributed software systems.
Nowadays, to describe the verifying model conditions it is common to use such mechanisms as linear temporal logic (LTL) and computational tree logic (CTL). However, experience has proven that these mechanisms can help formulate only a relatively small set of the same-type conditions. It can complicate the verification process or make it ineffective for a particular system model.
Correct formulation of model\'s verifying properties is the key problem, as the whole verification process depends on it. Thus, to achieve best results it is required to use powerful tools and techniques, which clearly formulate a wide class of verifying properties. The article describes a mechanism that can significantly extend the group of formulated conditions according to verifiable models. This effect can be achieved by expanding LTL expressivity using the proposed method, which increases the efficiency of the verification process.
The article provides a set of illustrative examples of the method, which demonstrates its practical application. The article also provides the example of properties verification for a particular model based on the proposed method.
Ключевые слова: ctl, ltl, формула временной логики, автомат бюхи, модель крипке, верификацияKeywords: ctl, ltl, temporal logic formula, Buchi automaton, kripke structure, verification
Просмотров: 11233
29. Основные понятия формальной модели семантических библиотек и формализация процессов интеграции в ней [№4 за 2015 год]
Авторы: Атаева О.М. (oli@ultimeta.ru) - Вычислительный центр им. А. А. Дородницына РАН (младший научный сотрудник); Серебряков В.А. (serebr@ultimeta.ru) - Вычислительный центр им. А. А. Дородницына РАН (профессор, зав. отделом), доктор физико-математических наук;
Аннотация: Развитие современных технологий подталкивает к переопределению понятия контента библиотеки, в качестве которого могут выступать и традиционные описания печатных изданий, и любые другие типы объектов. При этом контент цифровых библиотек и физические объекты могут быть связаны различными способами. В работе рассматриваются библиотеки как хранилища структурированных разнообразных данных с возможностью их интеграции с другими источниками данных. Приведены структура тезауруса для возможности определения их тематической направленности и основные понятия, необходимые для описания таких библиотек. Определяя такие понятия, как информационные ресурсы, наборы атрибутов, информационные объекты и другие, связанные с ними, формируют понятийную основу для некоторой предметной области создаваемой семантической библиотеки. Тезаурус же, в свою очередь, обеспечивает терминологическую поддержку этих понятий, облегчая навигацию по информационным объектам системы, поддерживает процесс уточнения и расширения запросов пользователей к системе. Также в статье описаны понятия, необходимые для детализации работ по интеграции данных, основной упор делается на понятия, используемые в процессе приведения данных. Важной характеристикой любого набора данных независимо от его структуры является понятие качества данных. Опираясь на оценку качества данных, можно давать объективную оценку эффективности процессов, происходящих в семантической библиотеке, важнейшим из которых является интеграция данных с другими источниками. Формальная модель понятий, описанная в данной части работы, используется в дальнейшем для описания онтологии такой библиотеки.
Abstract: Modern technology development leads to redefinition of the library content concept, which may be not only a traditional description of printed publications, but also other types of objects. The content of digital libraries and physical objects can be linked in various ways. This article considers the library as a structured data repository suitable for integration with other data sources. The paper presents a thesaurus structure to determine their thematic scope, as well as basic concepts to describe such libraries. Such concepts as information resources, attributes sets, information and other associated objects form a conceptual basis for a generated semantic library subject domain. Thesaurus, in its turn, provides terminology support for these concepts, facilitates information system navigation, supports the process of user query qualification and completion. The article also describes the concepts for detailed data integration work; the emphasis is on the concepts used in the process of data reduction. An important characteristic of any data set regardless of its structure is data quality. Based on data quality assessment it is possible to give an objective assessment of the semantic library process efficiency, where the most important process is data integration with other sources. A formal model of concepts described in the article is used to describe a library ontology.
Ключевые слова: модель данных, приведение данных, качество данных, семантические библиотекиKeywords: Data Model, data reduction, data quality, semantic library
Просмотров: 9768
30. Программный комплекс для анализа данных из социальных сетей [№4 за 2015 год]
Авторы: Батура Т.В. (tatiana.v.batura@gmail.com) - Институт систем информатики им. А.П. Ершова СО РАН (старший научный сотрудник), кандидат физико-математических наук; Мурзин Ф.А. ( murzin@iis.nsk.su) - Институт систем информатики им. А.П. Ершова СО РАН (зам. директора по научной работе), кандидат физико-математических наук; Проскуряков А.В. (alexey.proskuryakov@gmail.com) - Институт систем информатики им. А.П. Ершова СО РАН (аспирант);
Аннотация: Статья посвящена проблемам извлечения и обработки данных из социальных сетей. Рассмотрены различные количественные характеристики, отношения и множества, вычислимые на основе получаемых данных. Важно, что эти характеристики являются конструктивными и могут быть эффективно вычислены или построены при помощи соответствующих алгоритмов. Количество информации, находящейся в социальных сетях, очень велико. При использовании распределенной системы извлечения и обработки данных объем увеличивается еще больше. Поэтому наиболее важной и трудной задачей является выделение той части данных, которую можно было бы достаточно эффективно обработать и которая представляла бы интерес в соответствии с поставленными целями. Для решения этой задачи предлагается применить метод определения количества влияния аудитории на отдельного пользователя. Метод основан на теории динамического социального влияния, предложенной Б. Латане. Данный подход является полезным также при решении задачи определения источника распространения информации. Задача определения количества влияния на пользователя со стороны других пользователей непосредственно связана с задачей обнаружения лидеров мнений – сравнительно популярных пользователей, которые формируют мнение остального большинства. В работе предложен один из возможных методов определения лидеров мнений. Приведено довольно подробное описание разработанного программного комплекса, позволяющего работать с информацией из социальных сетей ВКонтакте и Twitter. Он состоит из шести модулей: извлечения, обработки данных, отслеживания изменений пользовательских данных, анализа данных, построения графовых структур и модуля визуализации данных.
Abstract: The paper focuses on the problems of extracting and processing social network data. It considers various numerical characteristics, relations and sets analyzed on the basis of output data. It is important that these characteristics are constructive and can be effectively calculated or built using corresponding algorithms.
The data amount in social networks is large. It becomes even larger when using distributed data extraction and processing system. That is why the most significant and difficult problem is to determine data, which could be processed effectively enough and is of interest according to the goals. To solve this task, we suggest using the method of determining the amount of audience influence on individual users. The method is based on the dynamic social impact theory proposed by B. Latané. This approach is also useful for solving the problem of determining the primary source of information. This problem is connected to the opinion leader detection problem. Opinion leaders are popular users who form the opinion of the majority. The paper describes one of the methods of opinion leader detection.
The article provides a detailed description of the developed software, which processes information from social networks VKontakte and Twitter. It consists of six modules: extraction module, data processing module, user data change tracking module, data analysis module, graph construction module and data visualization module.
Ключевые слова: межличностный анализ, лидеры мнений, источник распространения информации, обработка данных на естественном языке, анализ социальных сетейKeywords: interpersonal analysis, opinion leaders, primary source of information dissemination, natural language data processing, social network
Просмотров: 11003
◄ ← Предыдущая | 1 | 2 | 3 | 4 | Следующая → ►
