?
On Temporal Properties of Nested Petri Nets
P. 122–127.
Дворянский Л. В., Фрумин Д. И.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.
В книге
Камкин А., Петренко А., Терехов А. Perm: -, 2012.
Рыбаков М. Н., Shkatov D., Logical Investigations 2021 Vol. 27 No. 2 P. 93–120
Доказывается неразрешимость логи QCTL и QLTL в языке с двумя переменными и одной одноместной предикатной буквой. ...
Добавлено: 24 января 2022 г.
Mecheraoui K., Карраскель Г. Х., Ломазова И. А., , in: Proceedings of the Conference on Modeling and Analysis of Complex Systems and Processes 2020 (MACSPro 2020)Vol. 2795.: CEUR Workshop Proceedings, 2020. P. 34–45.
Добавлено: 14 января 2021 г.
Добавлено: 20 октября 2020 г.
Рыбаков М. Н., Котикова Е. А., Logical Investigations 2015 Vol. 21 No. 1 P. 86–99
Доказана неполнота по Крипке большого класса исчислений, содержащих аксиоматику CTL и QCL. ...
Добавлено: 20 июля 2020 г.
Рыбаков М. Н., Котикова Е. А., Вестник Тверского государственного университета. Серия: Прикладная математика 2016 № 4 С. 5–19
Показано, как погрузить арифметику TA в предикатный вариант логики ветвящегося времени CTL. ...
Добавлено: 20 июля 2020 г.
Карраскель Г. Х., Ломазова И. А., Itkin I., , in: Proceedings of the MACSPro Workshop 2019Vol. 2478: CEUR Workshop Proceedings.: CEUR-WS.org, 2019. P. 92–103.
Electronic trading systems provide the computational support for stock exchanges. Liquid markets use order-driven systems, i.e., where client requests, for trading financial instruments, are served through individual orders. This paper presents Petri net models assembling some crucial processes executed within order-driven systems such as orders submission, application of precedence rules, and the order matching mechanism. ...
Добавлено: 14 октября 2019 г.
Рыбаков М. Н., Котикова Е. А., В кн.: Десятые Смирновские чтения: материалы Междунар. науч. конф., Москва, 15–17 июня 2017 г.: М.: Современные тетради, 2017. С. 43–44.
Рассматривается первопорядковая темпоральная логика QCTL и её алгоритмические свойства. Показано, что эта логика не явялется рекурсивно перечислимой. ...
Добавлено: 7 октября 2019 г.
Рыбаков М. Н., Чагрова Л. А., Программные продукты и системы 2018 Т. 31 № 3 С. 591–597
В качестве формального средства, описывающего свойства различных структур (в том числе структур вычислений), обычно используют язык логики предикатов. Этот язык, с одной стороны, понятен и удобен, а с другой, многие вопросы, важные с прикладной точки зрения, для него алгоритмически неразрешимы, то есть не могут быть решены программно. Сейчас существует много альтернативных языков, позволяющих описывать вычисления ...
Добавлено: 6 октября 2019 г.
Камкин А. С., М.: МАКС Пресс, 2018.
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018.
Добавлено: 26 октября 2018 г.
Камкин А. С., Татарников А. Д., Смолов С. А. и др., , in: 2015 16th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2015. P. 1–6.
Добавлено: 18 июля 2018 г.
Камкин А. С., Татарников А. Д., Проценко А. С. и др., , in: 2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2017. P. 10–14.
Добавлено: 18 июля 2018 г.
Татарников А. Д., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97–100
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промышленных микропроцессоров. ...
Добавлено: 2 февраля 2018 г.
Мицюк А. А., Котылев Я. В., , in: Tools and Methods of Program Analysis: 4th International Conference, TMPA 2017, Moscow, Russia, March 3-4, 2017, Revised Selected PapersVol. 779: Communications in Computer and Information Science.: Springer, 2018. Ch. 11 P. 127–138.
Добавлено: 30 января 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Известия высших учебных заведений. Физика 2015 Т. 58 № 11-2 С. 70–74
В работе предлагается метод автоматизированного построения тестовых программ, предназначенных для функционального тестирования подсистем памяти одноядерных микропроцессоров. Предложенный метод осно ван на использовании формальных спецификаций механизмов кэширования и трансляции адресов. Различные варианты метода успешно применялись для тестирования промышленных микропроцессоров. ...
Добавлено: 25 января 2018 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., , in: Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer ScienceVol. 10629: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017.: Cham: Springer, 2017. P. 217–220.
Добавлено: 24 января 2018 г.