Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Синтез тестов с гарантированной полнотой для недетерминированных временных автоматов
Get PDFNowadays, the behaviour of many systems can be properly described by taking into account time constraints, and this motivates the adaptation of existing Finite State Machine (FSM)- based test derivation methods to timed models. In this paper, we propose a method for deriving conformance tests with the guaranteed fault coverage for a complete possibly nondeterministic FSM with a single clock; such Timed FSMs (TFSMs) are widely used when describing the behaviour of software and digital devices. The fault domain contains every complete TFSM with the known upper bounds on the number of states and finite boundary of input time guards. The proposed method is carried out by using an appropriate FSM abstraction of the given TFSM; the test is derived against an FSM abstraction and contains timed input sequences. Shorter test suites can be derived for a restricted fault domain, for instance, for the case when the smallest duration of an input time guard is larger than two. Moreover, the obtained test suites can be reduced, while preserving the completeness, when all input time guards of the specification and an implementation are right closed (or all intervals are left closed). Experiments are conducted to study the length of test suites constructed by different methods.В настоящее время при описании поведения дискретных систем достаточно часто необходимо принимать во внимание временные аспекты, и соответственно появляется необходимость в распространении автоматных методов синтеза тестов с гарантированной полнотой на временные автоматы. В данной статье мы предлагаем метод построения проверяющих тестов с гарантированной полнотой для полностью определенного, возможно, недетерминированного автомата с одной временной переменной. Такие временные автоматы используются при описании поведения программного обеспечения и цифровых устройств. Область неисправности содержит все полностью определенные автоматы с заданным числом состояний и известной верхней оценкой на интервалы, описывающие временные ограничения. Предлагаемый метод опирается на построение по заданному временному автомату соответствующей конечно автоматной абстракции (абстрактного автомата). По абстрактному автомату строится проверяющий тест, последовательности которого суть временные входные последовательности. Более короткие тесты можно построить, если ввести дополнительные ограничения на область неисправности, например, для случая, когда известна наименьшая продолжительность каждого временного интервала в тестируемой реализации, и её величина больше двух. Кроме того, тест можно сократить с сохранением его полноты в случае, когда все интервалы для временных ограничений закрыты справа (или все интервалы закрыты слева). Приводятся результаты проведенных компьютерных экспериментов по сравнению длин тестов, построенных по временному автомату различными методами.
К вопросу об измерении уровня абстракции диаграмм состояний на основе тестирования мутаций
No full textAbstract. The notation of state machines is widely adopted as a formalism to describe the behaviour of systems. Usually, multiple state machine models can be developed for the very same software system. Some of these models might turn out to be equivalent, but, in many cases, different state machines describing the same system also differ in their level of abstraction. In this paper, we present an approach to actually measure the abstractness level of state machines w.r.t. a given implemented software system. A state machine is considered to be less abstract when it is conceptionally closer to the implemented system. In our approach, this distance between state machine and implementation is measured by applying coverage criteria known from software mutation testing. Abstractness of state machines can be considered as a new metric. As for other metrics as well, a known value for the abstractness of a given state machine allows to assess its quality in terms of a simple number. In model-based software development projects, the abstract metric can help to prevent model degradation since it can actually measure the semantic distance from the behavioural specification of a system in form of a state machine to the current implementation of the system. In contrast to other metrics for state machines, the abstractness cannot be statically computed based on the state machine’s structure, but requires to execute both state machine and corresponding system implementation. The article is published in the author’s wording. Система обозначений диаграмм состояний (state machines) широко применяется в качестве формального средства описания поведения систем. Обычно для одной и той же программной системы можно создать много разных диаграмм состояний. Некоторые из этих моделей могут оказаться эквивалентными, но во многих случаях разные диаграммы состояний описывают одну и ту же систему на разных уровнях абстракции. В этой статье мы предлагаем подход, позволяющий провести фактическое измерение уровня абстракции диаграмм состояний по отношению к заданной реализации программной системы. Диаграмма состояний считается тем менее абстрактной, чем ближе она концептуально к реализованной системе. Согласно нашему подходу эта отдаленность диаграммы состояний от реализации системы измеряется путем применения критерия покрытия, используемого для тестирования мутации программного обеспечения. Уровень абстракции диаграмм состояний можно рассматривать как новый вид метрики. Что касается других метрик, то знание значения уровня абстракции заданной диаграммы состояний дает возможность оценить ее качество в числовых терминах. В тех проектах по разработке программного обеспечения, которые начинаются с построения модели, метрика абстракции может помочь избежать деградации моделей, поскольку она позволяет измерить фактическое отдаление спецификации поведения системы, представленной в виде диаграммы состояний, от текущей реализации системы. В отличие от прочих метрик для диаграмм состояний уровень абстракции нельзя вычислить статически, основываясь лишь на структуре самой диаграммы; для этого нужно сравнивать выполнения диаграмм состояний и соответствующую реализацию системы. Статья публикуется в авторской редакции.
Пополнение ядра оператора дифференцирования
Get PDFWhen investigating piecewise polynomial approximations in spaces L_p, \; 0~<~p~<~1, the author considered the spreading of k-th derivative (of the operator) from Sobolev spaces on spaces that are, in a sense, their successors with a low index less than one. In this article, we continue the study of the properties acquired by the differentiation operator with spreading beyond the space .The study is conducted by introducing the family of spaces Y_p^1, \; 0 <p < 1, which have analogy with the family W_p^1, \; 1 \le p <\infty. This approach gives a new perspective for the properties of the derivative. It has been shown, for example, the additivity property relative to the interval of the spreading differentiation operator: Here, for a function defined on [x_{n-1}; x_n], \; a~=~x_0 < x_1 < \cdots <x_m~=~b, was defined. One of the most important characteristics of a linear operator is the composition of the kernel.During the spreading of the differentiation operator from the space on the space the kernel does not change. In the article, it is constructively shown that jump functions and singular functions belong to all spaces and Consequently, the space of the functions of the bounded variation is contained in each and the differentiation operator on satisfies the relation Also, we come to the conclusion that every function from the added part of the kernel can be logically named singular.При изучении кусочно-полиномиальных приближений в пространствах 0~<~p~<~1, автором было рассмотрено распространение -й производной (оператора) с соболевских пространств на пространства, являющиеся в определённом смысле их преемниками и имеющие нижний индекс меньше единицы. Данная статья продолжает работы автора по исследованию свойств, обретаемых оператором дифференцирования при распространении его за границы пространства . Исследования проводятся с помощью введения семейства пространств Y_p^1,\; 0~<~p~<~1,( имеющего аналогию с семейством )W_p^1,\; 1~\le~p~<~\infty. Пространства снабжены квазинормами, построенными на основе квазинорм соответствующих пространств и для них выполняется . Такой подход даёт новый взгляд на свойства производной. Например, была показана аддитивность относительно интервала продолженного оператора дифференцирования:Здесь для функции заданной на [x_{n-1};x_n],\; a~=~x_0 < x_1 < \cdots < x_m~=~b, определено Одной из наиболее важных характеристик линейного оператора является состав ядра. При распространении оператора дифференцирования с пространства на пространства его ядро не изменяется. В статье конструктивно показано, что функции скачков и сингулярные функции принадлежат всем пространствам и для них Следовательно, пространство функций ограниченной вариации содержится в каждом и оператор на удовлетворяет соотношению Также приходим к выводу, что сингулярной логично назвать каждую функцию из добавленной части ядра
Математическая модель эксперимента Николсона
Get PDFConsidered is a mathematical model of insects population dynamics, and an attempt is made to explain classical experimental results of Nicholson with its help. In the first section of the paper Nicholson’s experiment is described and dynamic equations for its modeling are chosen. A priori estimates for model parameters can be made more precise by means of local analysis of the dynamical system, that is carried out in the second section. For parameter values found there the stability loss of the problem equilibrium of the leads to the bifurcation of a stable two-dimensional torus. Numerical simulations based on the estimates from the second section allows to explain the classical Nicholson’s experiment, whose detailed theoretical substantiation is given in the last section. There for an atrractor of the system the largest Lyapunov exponent is computed. The nature of this exponent change allows to additionally narrow the area of model parameters search. Justification of this experiment was made possible only due to the combination of analytical and numerical methods in studying equations of insects population dynamics. At the same time, the analytical approach made it possible to perform numerical analysis in a rather narrow region of the parameter space. It is not possible to get into this area, based only on general considerations.Рассматривается математическая модель динамики численности насекомых и предпринимается попытка объяснения с ее помощью классических экспериментальных результатов Николсона. В первой части работы описывается эксперимент Николсона и выбираются динамические уравнения для его моделирования. Априорные оценки параметров модели удается уточнить с помощью локального анализа динамической системы, который выполнен во втором разделе. В нем найдены значения параметров, при которых потеря устойчивости состоянием равновесия задачи приводит к бифуркации устойчивого двумерного тора. Численный счет, выполненный на основе оценок из второго раздела, позволяет объяснить классический эксперимент Николсона, развернутое теоретическое обоснование которого дано в последнем разделе. В нем для аттрактора системы вычислен старший ляпуновский показатель. Характер изменения этого показателя при изменении коэффициента линейного роста задачи позволяет дополнительно сузить область поиска параметров модели. Обоснование данного эксперимента стало возможным лишь в результате сочетания аналитических и численных методов исследования уравнений динамики популяций насекомых. При этом аналитический подход дал возможность проводить численный анализ в достаточно узкой области пространства параметров. Попасть в эту область, исходя лишь из общих соображений, не представляется возможным
Решение вида движущегося фронта двумерной задачи реакция-диффузия
Get PDFIn this paper, we study the moving front solution of the reaction-diffusion initialboundary value problem with a small diffusion coefficient. Problems in such statements can be used to model physical processes associated with the propagation of autowave fronts, in particular, in biophysics or in combustion. The moving front solution is a function the distinctive feature of which is the presence in the domain of its definition of a subdomain where the function has a large gradient. This subdomain is called an internal transition layer. In the nonstationary case, the position of the transition layer varies with time which, as it is well known, complicates the numerical solution of the problem as well as the justification of the correctness of numerical calculations. In this case the analytical method is an essential component of the study. In the paper, asymptotic methods are applied for analytical investigation of the solution of the problem posed. In particular, an asymptotic approximation of the solution as an expansion in powers of a small parameter is constructed by the use of the Vasil’eva algorithm and the existence theorem is carried out using the asymptotic method of differential inequalities. The methods used also make it possible to obtain an equation describing the motion of the front. For this purpose a transition to local coordinates takes place in the region of the front localization. In the present paper, in comparison with earlier publications dealing with two-dimensional problems with internal transition layers the transition to local coordinates in the vicinity of the front has been modified, that led to the simplification of the algorithm of determining the equation of the curve motion.В настоящей работе проведено исследование решения вида движущегося фронта начально-краевой задачи реакция-диффузия с малым коэффициентом диффузии. Задачи в таких постановках можно использовать для моделирования физических процессов, связанных с распространением автоволновых фронтов, в частности в биофизике или при описании процессов горения. Решение вида фронта – это функция, которая характеризуется тем, что в области её определения существует подобласть, в которой функция обладает большим градиентом. Эта подобласть называется внутренним переходным слоем. В нестационарном случае положение переходного слоя изменяется со временем, что, как известно, затрудняет численное решение задачи, а также обоснование корректности численных расчетов. В таком случае необходимым компонентом исследования является аналитический подход. В настоящей работе для аналитического исследования решения поставленной задачи применены асимптотические методы. В частности, при помощи алгоритма Васильевой построено асимптотическое приближение решения в виде разложения по степеням малого параметра, а доказательство существования решения вида движущегося фронта проведено при помощи асимптотического метода дифференциальных неравенств. Используемые методы также позволяют получить уравнение, описывающее движение фронта. С этой целью в области переходного слоя осуществляется переход к локальным координатам. В настоящей работе по сравнению с известными ранее публикациями, касающимися двумерных задач с внутренними переходными слоями, метод перехода к локальным координатам в окрестности фронта был модифицирован, что привело к упрощению алгоритма определения уравнения движения кривой
Полиэдральные характеристики задач о сбалансированном и несбалансированном двудольных подграфах
Get PDFWe study the polyhedral properties of three problems of constructing an optimal biclique in a bipartite graph. In the first problem we consider a balanced biclique with the same number of vertices in both parts and arbitrary edge weights. In the other two problems it is required to find maximum or minimum unbalanced bicliques with a fixed number of vertices and non-negative edges. All three problems are established to be NP-hard. We study the polytopes and the cone decompositions of these problems and their 1-skeletons. We describe the adjacency criterion in the 1-skeleton of the balanced biclique polytope. Clique number of 1-skeleton is estimated from below by a superpolynomial function. For both unbalanced biclique problems we establish the superpolynomial lower bounds on the clique numbers of the graphs of non-negative cone decompositions. These values characterize the time complexity in a broad class of algorithms based on linear comparisons.Исследуются полиэдральные характеристики трех задач о построении оптимальных полных двудольных подграфов двудольных графов. В первой задаче рассматриваются сбалансированные подграфы с одинаковым числом вершин в каждой доле и произвольными весами ребер. В двух других задачах речь идет о несбалансированных подграфах максимального и минимального веса с неотрицательными ребрами. Устанавливается, что все три задачи являются NP-трудными. В работе изучаются многогранники и конусные разбиения рассматриваемых задач, а также их графы. Для задачи о сбалансированном подграфе приводится условие смежности вершин в полиэдральном графе и графе соответствующего конусного разбиения. Плотность полиэдрального графа оценивается снизу сверхполиномиальной функцией. Для задач о несбалансированных подграфах строятся сверхполиномиальные нижние оценки плотности графов неотрицательных конусных разбиений. Полученные результаты характеризуют временную трудоемкость задач в широком классе алгоритмов, использующих линейные сравнения
Импульсно-рефрактерный режим в кольцевой цепи синаптически связанных осцилляторов нейронного типа
Get PDFIn the paper, a mathematical model of a neural network with an even number of ring synaptic interaction elements is considered. The model is a system of scalar nonlinear differentialdifference equations, the right parts of which depend on large parameters. The unknown functions included in the system characterize the membrane potentials of the neurons. The search of special impulse-refraction cycles within the system of equations is of interest. The functions with odd numbers of the impulse-refraction cycle have an asymptotically high pulses and the functions with even numbers are asymptotically small. Two changes allow to study a two-dimension nonlinear differential-difference system with two delays instead of the system. Further, a limit object that represents a relay system with two delays is defined by a large parameter tending to infinity. There exists the only periodic solution of the relay system with the initial function from a suitable function class. This is structurally proved, by using the step method. Next, the existence of relaxation periodic solutions of the two-dimension singularly perturbed system is proved by using the Poincare operator and the Schauder principle. The asymptotics of this solution is constructed, and it is proved that the solution is close to the decision of the relay system. Because of the exponential estimate of the Frechet derivative of the Poincare operator it implies the uniqueness and stability of solutions of the two-dimension differential-difference equation with two delays. Furthermore, with the help of reverse replacement the proved result is transferred to the original system. В настоящей работе рассматривается математическая модель кольцевой нейронной сети из четного числа синаптически взаимодействующих элементов. Модель представляет собой систему скалярных нелинейных дифференциально-разностных уравнений, правые части которых зависят от большого параметра. Неизвестные функции, входящие в систему, характеризуют мембранные потенциалы нейронов. Представляет интерес поиск в рамках данной системы уравнений специальных, так называемых импульсно-рефрактерных режимов, а именно периодических решений, в которых функции с номерами одной четности обладают асимптотически большим всплеском на периоде, а другой четности — всюду асимптотически малы. С этой целью последовательно делается две замены, позволяющие перейти от исследования исходной системы к двумерной системе скалярных нелинейных дифференциально-разностных уравнений с двумя запаздываниями. Далее, при стремлении большого параметра к бесконечности определяется предельный объект, представляющий собой релейную систему уравнений с двумя запаздываниями. Конструктивно, с использованием метода шагов, доказывается, что решение релейной системы уравнений с начальной функцией из подходящего класса совпадает с одной и той же периодической функцией с требуемыми свойствами. Затем определяется оператор последований Пуанкаре и с использованием принципа Шаудера доказывается существование релаксационного периодического решения двумерной сингулярно возмущенной системы. Для этого строится асимптотика этого решения, а затем доказывается его близость к решению релейной системы уравнений. Из экспоненциальной оценки производной Фреше оператора Пуанкаре следует единственность в построенном классе функций решения двумерной дифференциально-разностной системы уравнений с двумя запаздываниями, а также обосновывается его экспоненциальная орбитальная устойчивость. Далее, с помощью обратной замены доказанный результат переносится на исходную систему
Подход к верификации семейства мультиагентных систем разрешения конфликтов
Get PDFIn the paper, we describe a verification method for families of distributed systems generated by context-sensitive network grammar of a special kind. This grammar includes special non-terminal symbols, so called quasi-terminals, which uniquely correspond to grammar terminals. These quasi-terminals specify processes which are merging of base system processes, in contrast to simple nonterminals which specify networks of parallel compositions of the processes. The method is based on model checking technique and abstraction. An abstract representative model for a family of systems depends on their specification grammar and system properties to be verified. This model simulates the behaviour of the systems in such a way that the properties which hold for the representative model are satisfied for all these systems. The properties of the representative model can be verified by model checking method. The properties of a generated system are specified by universal branching time logic ∀CTL with finite deterministic automata as atomic formulas. We show the use of this method for verification of some properties of a multiagent system for conflict resolution, in particular, for context-dependent disambiguation in ontology population. We also suggest that this approach should be used for verification of computations on sub-grids which are sub-graphs of computation grids. In particular, we consider the computation of parity of the active processes number in a sub-grid.В данной работе мы описываем метод верификации для семейств распределенных систем, которые порождаются контекстно-зависимой сетевой грамматикой специального вида. Эта грамматика содержит специальные нетерминальные символы ䷘ квази-терминалы. Квази-терминалы однозначно соответствуют терминалам грамматики и могут задавать процессы,которые определяются слиянием базовых процессов системы, в то время как нетерминалы задают сети параллельных композиций этих процессов. Данный метод верификации основан на техниках верификации моделей и абстракции. Абстрактная репрезентативная модель семейства систем зависит от задающей их грамматики и верифицируемых свойств системы. Эта модель симулирует поведение заданных систем таким образом, что свойства, которые выполняются в репрезентативной модели, также выполняются и во всех заданных системах. Проверку свойств репрезентативной модели можно осуществлять с помощью метода проверки моделей. Свойства порождаемых систем специфицируются с помощью универсальной логики ветвящегося времени ∀CTL с конечными детерминированными автоматами в качестве атомарных формул. Мы показываем, что предложенный метод верификации можно применять для проверки некоторых свойств мультиагентных систем разрешения конфликтов, в частности, систем разрешения неоднозначностей при пополнении онтологий. Также показано, что этот подход можно использовать для верификации вычислений на подрешетках, являющихся подграфами решеток вычислений, например, для вычисления четности числа работающих процессов
Об алгебраических циклах на расслоенных произведениях неизотривиальных семейств регулярных поверхностей с геометрическим родом
Get PDFLet ) be a projective family of surfaces (possibly with degenerations) over a smooth projective curve . Assume that the discriminant loci are disjoint, for any smooth fibre and the period map associated with the variation of Hodge structures (where is a smooth part of the morphism ), is non-constant. If for generic geometric fibres and the following conditions hold: (i) is an odd integer; (ii) , then for any smooth projective model of the fibre product the Hodge conjecture on algebraic cycles is true. If, besides, the morphisms are smooth, are odd prime numbers and , then forПусть - проективное семейство поверхностей (возможно, с вырождениями) над гладкой проективной кривой . Предположим, что дискриминантные локусы не пересекаются, причем для любого гладкого слоя и отображение периодов, ассоциированное с вариацией структур Ходжа (где - гладкая часть морфизма ), является непостоянным. Если для общих геометрических слоев и выполнены следующие условия: (i) является нечетным числом; (ii) , то для любой гладкой проективной модели расслоенного произведения верна гипотеза Ходжа об алгебраических циклах. Если, кроме того, морфизмы гладкие, - нечетные простые числа и , то дл
Сетевая модель для задачи целочисленного сбалансирования четырехмерной матрицы
Get PDFThe problem of integer balancing of a four-dimensional matrix is studied. The elements of the inner part (all four indices are greater than zero) of the given real matrix are summed in each direction and each two- and three-dimensional section of the matrix; the total sum is also found. These sums are placed into the elements where one or more indices are equal to zero (according to the summing directions). The problem is to find an integer matrix of the same structure, which can be produced from the initial one by replacing the elements with the largest previous or the smallest following integer. At the same time, the element with four zero indices should be produced with standard rules of rounding - off. In the article the problem of finding the maximum multiple flow in the network of any natural multiplicity is also studied. There are arcs of three types: ordinary arcs, multiple arcs and multi-arcs. Each multiple and multi-arc is a union of linked arcs, which are adjusted with each other. The network constructing rules are described. The definitions of a divisible network and some associated subjects are stated. There are defined the basic principles for reducing the integer balancing problem of an -dimensional matrix ( ) to the problem of finding the maximum flow in a divisible multiple network of multiplicity . There are stated the rules for reducing the four-dimensional balancing problem to the maximum flow problem in the network of multiplicity 5. The algorithm of finding the maximum flow, which meets the solvability conditions for the integer balancing problem, is formulated for such a network.Рассматривается задача целочисленного сбалансирования четырехмерной матрицы. В исходной вещественной матрице элементы внутренней части (все четыре индекса больше нуля) просуммированы по каждому направлению и каждому плоскому и трехмерному сечению матрицы, а также найдена общая сумма. Данные суммы размещаются в элементах матрицы, у которых один или несколько индексов равны нулю (в соответствии с направлениями суммирования). Ищется целочисленная матрица той же структуры, получаемая из исходной заменой элементов на округления до целого сверху или целого снизу. При этом элемент с четырьмя нулевыми индексами получается по обычным правилам округления. В статье рассматривается также задача о наибольшем кратном потоке в сети произвольной натуральной кратности к. Определяется три типа дуг в сети: обычная дуга, кратная дуга, мультидуга. Каждая кратная и мультидуга представляет собой объединение к связанных дуг, согласованных между собой. Задаются правила построения сети. Вводится понятие делимой сети и ряд связанных определений. Определяются общие принципы сведения задачи целочисленного сбалансирования -мерной матрицы ( ) к задаче о максимальном потоке в делимой кратной сети кратности к . Задаются правила сведения четырехмерной задачи сбалансирования к задаче о наибольшем потоке в сети кратности 5. Для этой сети формулируется алгоритм нахождения максимального потока, удовлетворяющего условиям разрешимости задачи сбалансирования