?
Concurrency, Specification and Programming. CS&P 2014. Proceedings of the 23th International Workshop on Concurrency, Specification and Programming. Chemnitz, Germany, September 29 - October 1, 2014.
Vol. 1269: CEUR Workshop Proceedings (CEUR-WS.org).
Берлин :
Берлинский университет имени Гумбольдта, 2014.
Научный редактор: Popova-Zeugmann L.
This volume contains the papers presented at CS&P 2014: 23th International Workshop on Concurrency, Specification and Programming held on September 28 - October 1, 2014 in Chemnitz. Since the early seventies Warsaw University and Humboldt-University have alternately organized an annual workshop - since 1993 as CS&P. Over time, it has grown from a bilateral seminar to a meeting attended also by colleagues from other countries than Poland and Germany. This year there are 34 participants from 10 countries.
Главы книги
Ломазова И. А., Popova-Zeugmann L., , in: Concurrency, Specification and Programming. CS&P 2014. Proceedings of the 23th International Workshop on Concurrency, Specification and Programming. Chemnitz, Germany, September 29 - October 1, 2014.Vol. 1269: CEUR Workshop Proceedings (CEUR-WS.org).: Berlin: Humboldt University of Berlin, 2014. P. 126–137.
In this paper we examine how it is possible to control Petri net behavior with the help of time constraints. Controlling here means to force a process to behave in a desirable way by ascribing priorities to transitions and hence transforming a classic Petri net into a Priority Petri net. Liveness and boundedness are crucial ...
Добавлено: 24 октября 2014 г.
Научное направление:
Компьютерные науки
Приоритетные направления:
компьютерно-математическое
Язык:
английский

Humboldt-Universität zu Berlin, 2016.
This volume contains the papers presented at CS&P 2016, the 25th International Workshop on Concurrency, Specification and Programming, held on September 28 - 30, 2016 in Rostock, Germany. Since the early seventies Warsaw University and Humboldt University have alternately organized an annual workshop - since the early nineties known as CS&P. Over time, it has ...
Добавлено: 13 октября 2016 г.
Yaroslavl: Yaroslavl State University, 2013.
Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceedings of the fourth workshop are dedicated to formalisms for program semantics, formal models and verication, programming and specification languages, etc. ...
Добавлено: 14 июля 2013 г.
University of Rzeszow, 2015.
Добавлено: 11 октября 2015 г.
Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018.
Добавлено: 26 октября 2018 г.
Bialystok: Bialystok University of Technology, 2013.
This volume contains the Proceedings of 22nd Concurrency, Specification and Programming (GS&P) Workshop held on September 25-27, 2013 in Warsaw. There were 48 submissions. Each submission was reviewed by two program committee members. The committee decided to accept 40 papers. The Workshop was initiated in the mid 1970s by computer scientists and mathematicians from Warsaw ...
Добавлено: 30 сентября 2013 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87–102
ARM — это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ ...
Добавлено: 24 ноября 2017 г.
Татарников А. Д., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97–100
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промышленных микропроцессоров. ...
Добавлено: 2 февраля 2018 г.
Зыков С. В., Незнанов А. А., Максименкова О. В., Программные системы: теория и приложения 2018 Т. 9 № 4 С. 199–218
В статье обсуждается задача проверки гипотез о типе распределения данных, получаемых при измерениях в образовании, в программных системах. Приведён обзор критериев проверки нормальности, имеющие дискретные аппроксимации, что делает их пригодными для реализации в программных системах. Обсуждается место и необходимость применения указанных критериев при автоматизации измерений в образовании. Результаты обзора положены в основу алгоритма подбора критерия ...
Добавлено: 18 ноября 2018 г.
Татарников А. Д., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2016 Т. II С. 38–45
Генерация тестовых программ и анализ результатов их симуляции на проектной модели являются основным подходом к функциональной верификации микропроцессоров. Верификация – крайне трудоемкий процесс. По некоторым оценкам затраты на нее составляют около 70% от общих трудозатрат на разработку микропроцессора. Это связано с тем, что логика работы современных микропроцессоров содержит огромное количество состояний, и для того, чтобы ...
Добавлено: 12 декабря 2017 г.
Zakharov V.A., Volkanov D. Y., Zorin D. A. и др., Programming and Computer Software 2015 Vol. 41 No. 6 P. 325–335
Checking the correctness of distributed systems is one of the most difficult and urgent problems in software engineering. A combined toolset for the verification of real-time distributed systems (RTDS) is described. RTDSs are specified as statecharts in the Universal Modeling Language (UML). The semantics of statecharts is defined by means of hierarchical timed automata. The ...
Добавлено: 13 октября 2015 г.
Марширов В. В., Марширова Л. Е., Бизнес-информатика 2013 № 2 С. 55–62
Для комплексной оценки индивидуального труда разработчиков программного обеспечения предложен метод расстановки приоритетов. Изложены подходы к определению факторов, влияющих на оценку результатов их труда, к ранжированию факторов и к ранжированию разработчиков по каждому фактору. Предложенная методика может быть использована при разработке регламентов управленческого учета с целью совершенствования управления персоналом с учетом стратегических и тактических задач организации. ...
Добавлено: 27 июня 2013 г.
Максименкова О. В., Незнанов А. А., Программные системы: теория и приложения 2017 Т. 8 № 4 С. 31–46
В статье рассмотрены подходы, модели и методы проектирования и реализации программных средств поддержки измерений в образовании как части комплексных систем поддержки учебного процесса. Основным результатом является формализация понятия контрольно-измерительного материала, его жизненного цикла и смежных понятий с технической точки зрения на современном этапе развития программной инженерии. Формализация проведена на концептуальном уровне с обсуждением некоторых вопросов ...
Добавлено: 21 сентября 2017 г.
Leokhin, Y., Panfilov, P., Procedia Engineering 2015 Vol. 100 P. 1696–1705
Exponential growth in data production and a prominent trend in data center design architecture – a shift from expensive hardware towards a multitude of simple servers – pose new tasks and demand the use of different strategies for data center architects. In this work, a new solutions to distributed systems design are discussed, which are ...
Добавлено: 6 марта 2015 г.
Пономаренко А. А., Мальков Ю. А., Логвинов А. А. и др., Вестник Нижегородского университета им. Н.И. Лобачевского 2012 № 5 С. 409–415
Рассматривается новый подход к решению задачи поиска ближайшего соседа в метрическом пространстве. Предлагается в качестве структуры данных использовать граф, обладающий навигационными свойствами тесного мира, а в качестве алгоритма поиска – алгоритм градиентного спуска. Проблема существования локальных минимумов решается за счет произведения серии независимых поисков. Приведены экспериментальные данные, подтверждающие логарифмическую сложность алгоритма поиска. ...
Добавлено: 4 октября 2013 г.
Piza: Pisa University Press, 2015.
Добавлено: 15 марта 2016 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Silaev M. A., V. A. Silaeva, Journal of Physics: Condensed Matter 2013 Vol. 25 No. 22 P. 1–10
We investigate the multiquantum vortex states in a type-II superconductor in both 'clean' and 'dirty' regimes defined by impurity scattering rate. Within a quasiclassical approach we calculate self-consistently the order parameter distributions and electronic local density of states (LDOS) profiles. In the clean case we find the low temperature vortex core anomaly predicted analytically by ...
Добавлено: 19 ноября 2013 г.
Черешнев Р. И., Арёменко Е. А., Деев А. А. и др., Проблемы развития корабельного вооружения и судового радиоэлектронного оборудования 2015 № 4 С. 92–100
В работе рассмотрены методы и технологии, использованные при разработке специального программного обеспечения пульта управления судового лазерного комплекса (СЛК) и комплекта программных имитаторов информационных потоков, генерируемых оборудованием СЛК при взаимодействии с пультом управления (ПУ). ...
Добавлено: 18 ноября 2015 г.
Lahav O., Namakonov E., Oberhauser J. и др., Proceedings of the ACM on Programming Languages 2021 Vol. 5 No. OOPSLA Article 98
Добавлено: 2 февраля 2022 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125–138
Подсистема памяти является одним из ключевых компонентов микропроцессора. Она включает в себя набор запоминающих устройств различного назначения, объединенных в сложную иерархическую структуру. При этом количество возможных состояний подсистемы крайне велико. По этой причине верификация ее функциональной корректности представляет собой нетривиальную задачу. В настоящее время наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является ...
Добавлено: 10 декабря 2017 г.
Smeliansky R. L., Chemeritsky E. V., Захаров В. А., Automatic Control and Computer Sciences 2014 Vol. 48 No. 7 P. 398–406
Добавлено: 30 сентября 2015 г.
Cham: Springer, 2014.
Труды 25-й международной научной конференции по применениям баз данных и экспертных систем - DEXA 2014 (Мюнхен, Германия, 1-4 сентября 2014). ...
Добавлено: 25 ноября 2014 г.
Berlin: Springer, 2014.
This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 ...
Добавлено: 3 июля 2014 г.
Камкин А. С., М.: МАКС Пресс, 2018.
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.