Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Применение метода квазинормальных форм к математической модели отдельного нейрона
Get PDFWe consider a scalar nonlinear differential-difference equation with two delays, which models the behavior of a single neuron. Under some additional suppositions for this equation it is applied a well-known method of quasi-normal forms. Its essence lies in the formal normalization of the Poincare – Dulac, the production of a quasi-normal form and the subsequent application of the conformity theorems. In this case, the result of the application of quasi-normal forms is a countable system of differential-difference equations, which manages to turn into a boundary value problem of the Korteweg – de Vries equation. The investigation of this boundary value problem allows to make the conclusion about the behavior of the original equation. Namely, for a suitable choice of parameters in the framework of this equation it is implemented the buffer phenomenon consisting in the presence of the bifurcation mechanism for the birth of an arbitrarily large number of stable cycles.Рассматривается скалярное нелинейное дифференциально-разностное уравнение с двумя запаздываниями, которое моделирует поведение отдельного нейрона. При некоторых дополнительных предположениях к этому уравнению применяется известный метод квазинормальных форм. Суть его заключается в формальной нормализации Пуанкаре – Дюлака, получении квазинормальной формы и последующем применении теорем о соответствии. В данном случае результатом применения квазинормальных форм является счетная система дифференциально-разностных уравнений, которую удается свернуть в краевую задачу типа Кортевега – де Фриза. Исследование этой краевой задачи позволяет сделать вывод о поведении исходного уравнения. А именно, при подходящем выборе параметров в рамках данного уравнения реализуется феномен буферности, состоящий в наличии бифуркационного механизма, обеспечивающего рождение сколь угодно большого числа устойчивых циклов
Разрешимость эквивалентности в перегородчатых моделях программ
Get PDFAlgebraic program models with procedures are designed to analyze program semantic properties on their models called program schemes. Liberisation and equivalence problems are stated for program models with procedures. A subclass of program models with procedures called special gateway models is investigated. A better complexity algorithm for the liberisation in such models is proposed. Primitive program schemes are defined as a subclass of special gateway models. It is shown that the equivalence problem in such models is decidable if the equivalence problem is decidable in special program models without procedures. For some cases of decidability the complexity is evaluated.Алгебраические модели программ с процедурами предназначены для изучения семантических свойств самих программ на их образах–схемах программ. Для моделей программ с процедурами формулируются проблемы либеризации и эквивалентности. Рассматривается подкласс моделей программ с процедурами – специальные перегородчатые модели. Для таких моделей программ улучшена оценка сложности алгоритма, решающего проблему либеризации. Введено понятие примитивных схем программ как подкласса специальных перегородчатых. Для них установлена разрешимость проблемы эквивалентности при разрешимости проблемы эквивалентности в специального вида моделях программ без процедур. Для некоторых случаев разрешимости проблемы эквивалентности приведены оценки сложности
Поддержка эволюции визуальных языков в платформе QReal
Get PDFLike other software artefacts, DSMLs evolve in time. When a DSML changes, instance models might no longer conform to the new DSML metamodel and hence cannot be manipulated with a modelling tool. Therefore, a need for models migration to a new version of metamodel arises. Today, various approaches to this problem exist - from entirely manual to mostly automated. This paper describes a hybrid approach to model migration implemented in DSM platform QReal, which is being developed by the research group of Software Engineering Chair of St. Petersburg State University. That DSM platform implies some specific requirements, such as the support of metamodel interpretation and metamodeling “on the fly” modes. The presented approach realizes model migration when using one of those specific features. Как и другие программные продукты, языки моделирования развиваются со временем. В результате изменений в языке, модели на данном языке могут перестать соответствовать новой метамодели языка, что ведет к невозможности работы с ними с помощью инструментов моделирования. Таким образом, возникает проблема переноса моделей на новую версию языка. В настоящее время существуют различные подходы к решению данной проблемы – от полностью ручных до практически полностью автоматизированных. Данная статья описывает гибридный подход к миграции моделей, реализованный в DSM- платформе QReal, разрабатываемой на кафедре системного программирования Санкт-Петербургского государственного университета. Рассматриваемая система накладывает некоторые специфические требования, такие как под- держка режимов интерпретации метамодели и метамоделирования “на лету”. Представленный в статье подход реализует миграцию моделей при использовании данных возможностей
Управляемые тупики в параллельных ресурсно-ограниченных потоках работ
Get PDFWe study the verification of the soundness property for workflow nets extended with resources. A workflow is sound if it terminates properly (no deadlocks and livelocks are possible). A class of resource-constrained workflow nets (RCWF-nets) is considered, where resources can be used by a process instance, but cannot be created or spent. Two sound RCWF-nets using the same set of resources can be put in parallel. This parallel composition may in some cases produce additional deadlocks. A problem of deadlock avoidance in parallel workflows is studied, some methods of deadlock search and control are presented.Работа посвящена проблеме проверки правильной организованности (бездефектности) сетей потоков работ с ресурсами. Поток работ называется бездефектным, если он может быть корректно завершен от любого достижимого состояния. Рассматривается класс схем ресурсно-ограниченных потоков работ (RCWF-сетей), в которых экземпляры процесса могут использовать внешние ресурсы, но не могут за время своей жизни изменить их количество.Две бездефектные RCWF-сети, использующие один и тот же набор ресурсов, могут быть запущены параллельно. Подобная параллельная композиция в некоторых случаях может порождать дополнительные тупики, вызванные взаимными блокировками. Мы исследуем проблему обнаружения потенциальных блокировок и предлагаем способы организации такого управления сетью, которое позволило бы их избегать
Моделирование согласованного поведения ПЛК-датчиков
Get PDFThe article extends the cycle of papers dedicated to programming and verificatoin of PLC-programs by LTL-specification. This approach provides the availability of correctness analysis of PLC-programs by the model checking method.The model checking method needs to construct a finite model of a PLC program. For successful verification of required properties it is important to take into consideration that not all combinations of input signals from the sensors can occur while PLC works with a control object. This fact requires more advertence to the construction of the PLC-program model.In this paper we propose to describe a consistent behavior of sensors by three groups of LTL-formulas. They will affect the program model, approximating it to the actual behavior of the PLC program. The idea of LTL-requirements is shown by an example.A PLC program is a description of reactions on input signals from sensors, switches and buttons. In constructing a PLC-program model, the approach to modeling a consistent behavior of PLC sensors allows to focus on modeling precisely these reactions without an extension of the program model by additional structures for realization of a realistic behavior of sensors. The consistent behavior of sensors is taken into account only at the stage of checking a conformity of the programming model to required properties, i. e. a property satisfaction proof for the constructed model occurs with the condition that the model contains only such executions of the program that comply with the consistent behavior of sensors
Угловой пограничный слой в нелинейных эллиптических задачах, содержащих производные первого порядка
Get PDFIn a rectangular domain the first boundary value problem is considered for a singularly perturbed elliptic equationε 2∆u − ε αA(x, y) ∂u/∂y = F(u, x, y, ε)with a nonlinear on u function F. The complete asymptotic solution expansion uniform in a closed rectangle is constructed for α > 1. If 0 < α < 1, the uniform asymptotic approximation is constructed in zero and first approximations. The features of the asymptotic behavior are noted in the case α = 1 .В прямоугольной области рассмотрена первая краевая задача для сингулярно возмущенного эллиптического уравненияε 2∆u − ε αA(x, y) ∂u/∂y = F(u, x, y, ε)с нелинейной по u функцией F. Для α > 1 построено полное асимптотическое разложение решения, равномерное в замкнутом прямоугольнике. Если 0 < α < 1, то равномерное асимптотическое приближение строится в нулевом и первом приближении. Отмечены особенности асимптотики в случае α = 1
Анализ и верификация MSC-диаграмм распределённых систем с помощью раскрашенных сетей Петри
Get PDFThe standard language of message sequence charts MSC is intended to describe scenarios of object interaction. Due to their expressiveness and simplicity MSC diagrams are widely used in practice at all stages of system design and development. In particular, the MSC language is used for describing communication behavior in distributed systems and communication protocols. In this paper the method for analysis and verification of MSC and HMSC diagrams is considered. The method is based on the translation of (H)MSC into coloured Petri nets. The translation algorithms cover most standard elements of the MSC including data concepts. Size estimates of the CPN which is the result of the translation are given. Properties of the resulting CPN are analyzed and verified by using the known system CPN Tools and the CPN verifier based on the known tool SPIN. The translation method has been demonstrated by the example.Стандартный язык диаграмм последовательных сообщений MSC предназначен для описания сценариев взаимодействия объектов. Благодаря своей выразительности и простоте MSC-диаграммы широко применяются на практике на всех этапах проектирования и разработки программных систем. В частности, язык MSC используется для спецификации поведения в распределенных системах и коммуникационных протоколах. В работе рассматривается метод анализа и верификации диаграмм MSC и HMSC. Метод основывается на трансляции конструкций (H)MSC в раскрашенные сети Петри. Описываемые правила трансляции охватывают большинство конструкций стандарта, включая концепцию данных. Приводятся оценки размера сетей Петри, полученных в результате трансляции. Свойства построенных сетей анализируются и верифицируются с помощью известной системы CPN Tools и системы автоматической верификации на основе SPIN. Работоспособность данного метода продемонстрирована на примере
Моделирование, спецификация и построение программ логических контроллеров
Get PDFA new approach to construction of reliable discrete PLC-programs with timers — programming based on specification and verification — is proposed. Timers are modelled in a discrete way. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language according to a LTLspecification. A new approach to programming of PLC is shown by an example. The proposed programming approach provides an ability of a correctness analysis of PLC-programs using the model checking method. The programming requires fulfillment of the following two conditions: 1) a value of each variable should be changed not more than once per one full PLC-program implementation (per one full working cycle of PLC); 2) a value of each variable should only be changed in one place of a PLC-program. Under the proposed approach the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations that increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable
Построение и верификация ПЛК-программ по LTL-спецификации
Get PDFAn approach to construction and verification of PLC-programs for discrete tasks is proposed. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language according to an LTL-specification. The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV. A new approach to programming and verification of PLCprograms is shown by an example. For a discrete problem we give a ST-program, its LTL-specification and an SMV-model.A purpose of the article is to describe an approach to programming PLC, which would provide a possibility of PLC-program correctness analysis by the model checking method.Under the proposed approach the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations that increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable. In addition, an SMV-model of a PLC-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV