Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
О преподавании формальных моделей и алгоритмов анализа параллельных систем
No full textThere is a widespread and rapidly growing interest to the parallel programming nowadays. This interest is based on availability of supercomputers, computer clusters and powerful graphic processors for computational mathematics and simulation. MPI, OpenMP, CUDA and other technologies provide opportunity to write C and FORTRAN code for parallel speed-up of execution without races for resources. Nevertheless concurrency issues (like races) are still very important for parallel systems in general and distributed systems in particular. Due to this reason, there is a need of research, study and teaching of formal models of concurrency and methods of distributed system verification.The paper presents an individual experience with teaching Formal Models of Concurrency as a graduate elective course for students specializing in high-performance computing. First it sketches course background, objectives, lecture plan and topics. Then the paper presents how to formalize (i.e. specify) a reachability puzzle in semantic, syntactic and logic formal models, namely: in Petri nets, in a dialect of Calculus of Communicating Systems (CCS) and in Computation Tree Logic (CTL). This puzzle is a good educational example to present specifics of different formal notations.The article is published in the author’s wording.В настоящее время наблюдается огромный практический интерес к параллельному программированию. Этот интерес обусловлен доступностью супер-ЭВМ, компьютерных кластеров и мощных графических процессоров для массового использования в вычислительной математике и компьютерном моделировании. Кроме того, такие технологии параллельного программирования, как MPI, OpenMP и CUDA, позволяют использовать безопасным образом опыт программирования на классических языках Си и FORTRAN для ускорения вычислений, избегая конфликтов (“гонок”) из-за ресурсов. Однако такой прогресс параллельного программирования не означает, что конкуренция из-за ресурсов не может возникать в параллельных общего вида, в так называемых распределенных системах в частности. Поэтому остается актуальным изучение и преподавание формальных моделей параллелизма и средств верификации поведенческих свойств параллельных (распределенных) систем. В статье представлен опыт преподавания специального курса по формальным моделям параллелизма для магистрантов и аспирантов, специализирующихся в области высокопроизводительных вычислений. Сначала в статье дан обзор курса в целом, предварительных знаний, необходимых для этого курса, целей и задач курса, представлен план лекций и список рекомендованной литературы. Затем представлен пример одной поучительной головоломки (на достижимость в пространстве состояний) и ее формализации средствами семантических, синтаксических и логических моделей, как-то: сетями Петри, средствами исчисления параллельных взаимодействующих процессов (CCS) и темпоральной логики CTL. Эта головоломка — хороший пример для того, чтобы показать специфику и пользу каждого из рассмотренных формализмов.Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.Статья публикуется в авторской редакции
Устойчивость простейших периодических решений в уравнении Стюарта–Ландау с большим запаздыванием
Get PDFWe study the local dynamics of the Stuart–Landau equation with large delay in the neibourhood of periodic solutions. We find sufficient conditions of instability of periodic solutions and sufficient conditions of their stability.Исследуется устойчивость простейших периодических решений комплексного уравнения с большим запаздыванием с кубической нелинейностью в зависимости от значений параметров. Найдены достаточные условия устойчивости и неустойчивости периодических решений. Описана геометрия областей устойчивости и неустойчивости в плоскости параметров, задающих главную часть решения
Оценка требуемых скоростей передачи данных при организации беспроводной связи между ядрами центрального процессора
Get PDFIn this paper, a principal architecture of common purpose CPU and its main components are discussed, CPUs evolution is considered and drawbacks that prevent future CPU development are mentioned. Further, solutions proposed so far are addressed and a new CPU architecture is introduced. The proposed architecture is based on wireless cache access that enables a reliable interaction between cores in multicore CPUs using terahertz band, 0.1-10THz. The presented architecture addresses the scalability problem of existing processors and may potentially allow to scale them to tens of cores. As in-depth analysis of the applicability of the suggested architecture requires accurate prediction of traffic in current and next generations of processors, we consider a set of approaches for traffic estimation in modern CPUs discussing their benefits and drawbacks. The authors identify traffic measurements by using existing software tools as the most promising approach for traffic estimation, and they use Intel Performance Counter Monitor for this purpose. Three types of CPU loads are considered including two artificial tests and background system load. For each load type the amount of data transmitted through the L2-L3 interface is reported for various input parameters including the number of active cores and their dependences on the number of cores and operational frequency
Особенности формирования диссипативных структур, описываемых уравнением Курамото–Сивашинского
Get PDFIn the present work, we study the features of dissipative structures formation described by the periodic boundary value problem for the Kuramoto-Sivashinsky equation. The numerical algorithm which is based on the pseudospectral method is presented. We prove the efficiency and accuracy of the proposed numerical method on the exact solution of the equation considered. Using this approach, we performed the numerical simulation of dissipative structure formations described by the Kuramoto–Sivashinsky equation. The influence of the problem parameters on these processes are studied. The quantitative and qualitative characteristics of dissipative structure formations are described. We have shown that there is a value of the control parameter at which the processes of dissipative structure formation are observed. In particular, using the cyclic convolution we define the average value of this parameter. Also, we find the dependence of the amplitude of the structures on the value of control parameter.Рассматриваются процессы самоорганизации диссипативных структур в физических системах, описываемых уравнением Курамото–Сивашинского. Разработан вычислительный алгоритм, позволяющий проводить моделирование процессов, описываемых данным уравнением. Проведено тестирование и продемонстрирована эффективность вычислительной процедуры. Исследован процесс формирования диссипативных структур в зависимости от параметров модели. При помощи метода циклической свертки определен диапазон изменения управляющего параметра, при котором имеют место процессы самоорганизации, а также исследованы качественные и количественные характеристики рассматриваемого процесса. В частности получена зависимость амплитуды сформировавшейся структуры от величины управляющего параметра
Автоматизация формальной верификации программ на языке Пифагор
No full textNowadays, due to software sophistication, programs correctness is more often proved by means of formal verification. The method of deduction based on Hoare logic could be used for any programminglanguage and it has the capability of partial automation of the proof process. However, the method of deduction is not widely used for verification of parallel programs because of high complexity of theprocess. The usage of the functional data-flow paradigm of parallel programming allows to decrease the complexity of the proof process. In this article a proof process of correctness of functional data-flow parallel programs in the Pifagor language is considered. The proof process of a program correctness is considered as a tree where each node is a program data-flow graph, whose edges are marked with formulas in a specification language. The tree root is the initial program data-flow graph with a precondition and a postcondition, which describe restrictions on input variables and correctness conditions of the result of the program execution, respectively. Basic transformations of the data-flow graph are edge marking, equivalent transformation, splitting, folding of the program. By means of these transformations the data-flow graph is transformed and finally is reduced to a set of formulas in the specification language. If all these formulas are identically true, the program is correct. Several modules is distinguished in the system: “Program correctness prover”, “Axioms and theorems library management system” and “Errors analysis and output of information about errors”. According to this architecture, the toolkit for supporting formal verification was developed. The main functionality of the system implementation is considered.В связи с увеличением сложности программного обеспечения корректность программы всёчаще доказывается с помощью методов формальной верификации. Дедуктивный анализ на основе исчисления Хоара применим для произвольных языков программирования и допускает частичную автоматизацию процесса. Однако дедуктивный анализ не нашёл широкого применения для верификации параллельных программ из-за высокой сложности процесса. Использование функционально-потоковой парадигмы параллельного программирования позволяет снизить сложность доказательства. В работе рассматривается процесс доказательства корректности функционально-потоковых параллельных программ на языке Пифагор и предлагается архитектура инструментального средства для поддержки процесса доказательства. Процесс доказательства корректности программы представляется в виде дерева, каждый узел которого — информационный граф программы, в котором дуги размечены формулами на языке спецификации. Корнем дерева является информационный граф программы с предусловием и постусловием, которые описывают ограничения на входные переменные и условия корректности результата работы программы соответственно. Основные преобразования, применимые к информационному графу программы: разметка дуг, эквивалентное преобразование, расщепление, свертка программы. Посредством данных преобразований информационный граф модифицируется и, в конечном счете, сводится к набору формул на языке спецификации, истинность которых будет свидетельствовать о корректности программы. Предложена архитектура системы поддержки процесса доказательства, которая позволяет строить дерево доказательства. В системе выделено несколько основных модулей: «Модуль доказательства корректности программы», «Система управления библиотекой аксиом и теорем» и «Модуль анализа ошибок и выдачи информации об ошибках». Согласно описанной архитектуре, разработано инструментальное средство для поддержки формальной верификации, которая позволяет строить дерево доказательства. Описана основная функциональность реализации системы
Задача адаптации обобщенного нейронного элемента
Get PDFA perspective model of the neuron cell | the generalized neural element (GNE) is studied in this article. This model has the universal character. It combines properties of the neuron-oscillator and the neuron-detector. The problem of adaptation of the generalized neural element is formulated and solved.Изучается перспективная нейронная модель - обобщенный нейронный элемент (ОНЭ). Эта модель носит универсальный характер, объединяя свойства нейрона-автогенератора и нейрона-детектора. Ставится и решается задача адаптации обобщенного нейронного элемента автогенераторного типа
Катастрофа голубого неба в системах с неклассическими релаксационными колебаниями
Get PDFThe feasibility of a known blue-sky bifurcation in a class of three-dimensional singularly perturbed systems of ordinary differential equations with one fast and two slow variables is studied. A characteristic property of the considered systems is that they permit so-called nonclassic relaxation oscillations, that is, oscillations with slow components asymptotically close to time-discontinuous functions and a δ-like fast component. Cases when blue-sky bifurcation leads to a relaxation cycle or stable two-dimensional torus are analyzed. Also the question of homoclinic structure emergence is considered.Исследуется вопрос о реализуемости известной бифуркации типа катастрофы голубого неба в некотором классе трехмерных сингулярно возмущенных систем обыкновенных дифференциальных уравнений с одной быстрой и двумя медленными переменными. Характерная особенность рассматриваемых систем состоит в том, что в них происходят так называемые неклассические релаксационные колебания. Таковыми принято называть колебания, у которых медленные компоненты асимптотически близки к некоторым разрывным по времени функциям, а быстрая компонента δ-образна. Разбираются случаи, когда в результате катастрофы голубого неба возникает устойчивый релаксационный цикл или устойчивый двумерный инвариантный тор. Рассматривается также вопрос о появлении гомоклинических структур
АВТОВОЛНОВЫЕ ПРОЦЕССЫ В КОЛЬЦЕВОЙ НЕЙРОННОЙ ЦЕПИ С ОДНОНАПРАВЛЕННОЙ СВЯЗЬЮ
Get PDFThe article is devoted to the mathematical modeling of neural activity. We propose new classes of singularly perturbed differential-difference equations with delay of Volterra type. With these systems, the models as a single neuron or neural networks are described. We study attractors of ring systems of unidirectionally coupled impulse neurons in the case where the number of links in the system increases indefinitely. In order to study periodic solutions of travelling wave type of this system, some special tricks are used which reduce the existence and stability problems for cycles to the investigation of auxiliary system with impulse actions. Using this approach, we establish that the number of stable self-excited waves simultaneously existing in the chain increases unboundedly as the number of links of the chain increases, that is, the well-known buffer phenomenon occurs.Статья посвящена проблеме математического моделирования нейронной активности. Предлагаются новые классы сингулярно возмущенных дифференциально-разностных уравнений с запаздыванием вольтерровского типа, с помощью которых описывается функционирование как отдельного нейрона, так и нейронных сетей. Проводится исследование аттракторов кольцевой системы однонаправленно связанных импульсных нейронов при неограниченном увеличении числа звеньев цепочки. Для изучения ее периодических решений автоволнового типа используются некоторые специальные приемы, сводящие проблемы существования и устойчивости циклов к анализу вспомогательной системы обыкновенных дифференциальных уравнений с импульсным воздействием. На этом пути устанавливается, что при увеличении числа звеньев цепочки количество сосуществующих в ней устойчивых автоволновых решений неограниченно растет, т.е. имеет место известное явление буферности
Анализ локальных бифуркаций для уравнения с запаздыванием, зависящим от искомой функции
Get PDFIn this paper, a first-order equation with state-dependent delay and with a nonlinear right-hand side is considered. Conditions of existence and uniqueness of the solution of initial value problem aresupposed to be executed. The task is to study the behavior of solutions of the considered equation in a small neighborhood of its zero equilibrium. Local dynamics depends on real parameters which are coefficients of equation right-hand side decomposition in a Taylor series. The parameter which is a coefficient at the linear part of this decomposition has two critical values which determine a stability domain of zero equilibrium. We introduce a small positive parameter and use the asymtotic method of normal forms in order to investigate local dynamics modifications of the equation near each two critical values. We show that the stability exchange bifurcation occurs in the considered equation near the first of these critical values, and the supercritical Andronov – Hopf bifurcation occurs near the second of them (if the sufficient condition is executed). Asymptotic decompositions according to correspondent small parameters are obtained for each stable solution. Next, a logistic equation with state-dependent delay is considered as an example. The bifurcation parameter of this equation has one critical value. A simple sufficient condition of Andronov – Hopf bifurcation occurence in the considered equation near a critical value is obtained as a result of applying the method of normal forms.В работе рассматривается уравнение первого порядка с запаздыванием, зависящим от искомойфункции, с нелинейной правой частью. Для этого уравнения предполагаются выполненными усло-вия существования и единственности решения начальной задачи. Ставится задача исследованияповедения решений рассматриваемого уравнения в малой окрестности его нулевого положения рав-новесия. Изучение локальной динамики проводится в зависимости от вещественных параметров 첐коэффициентов тейлоровского разложения правой части. Параметр, являющийся коэффициентомпри линейном члене, имеет два критических значения, определяющих область устойчивости ну-левого положения равновесия. Чтобы исследовать изменение локальной динамики уравнения припереходе данного параметра через критические значения, вводится малый параметр и применяет-ся асимптотический метод нормальных форм. Показывается, что для первого случая в уравненииимеет место бифуркация обмена устойчивостью, а для второго случая 움 суперкритическая бифур-кация Андронова – Хопфа (при выполнении достаточного условия). Для каждого из устойчивыхрежимов получены их асимптотические разложения по соответствующим малым параметрам. За-тем в качестве примера рассматривается логистическое уравнение с запаздыванием, зависящимот искомой функции. Для этого уравнения бифуркационный параметр имеет единственное кри-тическое значение. С помощью метода нормальных форм устанавливается простое достаточноеусловие возникновения суперкритической бифуркации Андронова – Хопфа в уравнении при пере-ходе параметра через критическое значение
Исследование стационарных режимов дифференциально-разностного уравнения динамики популяции насекомых
Get PDFRelaxation oscillations in a first order differential equation with two delays are considered. On the basis of a special asymptotic big parameter method the problem of studying dynamics of an equation is reduced to the analysis of nonlinear mappings. Each cycle of these mappings corresponds to a periodic solution of the initial equation with the same stability.Исследуются релаксационные колебания в уравнении первого порядка с двумя запаздываниями. На основе специального асимптотического метода большого параметра, разработанного автором, вопрос о динамике решений сводится к анализу решений нелинейных отображений. Для каждого цикла таких отображений построены соответствующие периодические решения исходного уравнения с наследованием свойств устойчивости