?
Как разработать простое средство верификации систем реального времени
Моделирование и анализ информационных систем. 2012. Т. 19. № 6. С. 45–56.
Волканов Д. Ю., Захаров В. А., Зорин Д. А., Коннов И. В., Подымов В. В.
Исследуется задача верификации систем реального времени (СРВ). Для описания СРВ удобно использовать диаграммы состояний UML с семантикой, определяемой иерархическими автоматами. Для верификации СРВ часто применяется средство UPPAAL, разработанное для проверки формул логики TCTL на сети временных автоматов. Основным результатом данной статьи является алгоритм трансляции иерархических автоматов в сеть временных автоматов и обоснование его корректности.
Язык:
русский
Добавлено: 11 июня 2026 г.
Добавлено: 19 мая 2026 г.
Добавлено: 28 апреля 2026 г.
Добавлено: 20 апреля 2026 г.
СПб.: АО "ЦТСС", 2025.
В научном издании представлены труды Двенадцатой всероссийской научно-практической конференции по имитационному моделированию и его применению в науке и промышленности «Имитационное моделирование. Теория и практика» (ИММОД-2025) по следующим направлениям: - теоретические основы и методология имитационного и комплексного моделирования; - методы исследования и оценки качества моделей, валидация и верификации моделей; - методы и системы распределенного моделирования; - ...
Добавлено: 17 апреля 2026 г.
Медведев В. О., / Series arXiv "math". 2026.
We investigate the interplay between the dimension of the space of static potentials and the geometric and topological structure of the underlying static three-manifold. A partial classification of boundaryless static manifolds is obtained in terms of this dimension. We also treat the case of static manifolds with boundary. In particular, we prove that if a ...
Добавлено: 3 апреля 2026 г.
Gabdullin N., Андросов И. А., / Series Computer Science "arxiv.org". 2026.
Добавлено: 2 апреля 2026 г.
Гордин В. А., Smirnov M. A., Russian Meteorology and Hydrology 2025 No. 50 P. 1016–1028
Для интерполяции комплексного прогноза геопотенциала и температуры в точки регулярной сетки проводилась статистическая оценка трехмерных авто- и кросс-кореляционных функций для инкрементов от первого приближения. В качестве первого приближения использованы поля прогноза по модели ICON. ...
Добавлено: 17 февраля 2026 г.
Степанянц В. Г., , in: 2025 International Russian Automation Conference (RusAutoCon).: IEEE, 2025. P. 982–986.
Добавлено: 3 октября 2025 г.
Poplavsky E., Кузнецова А. М., Troitskaya Y., Journal of Marine Science and Engineering 2023 Vol. 11 No. 6 Article 1239
В данной работе представлен анализ нового метода восстановления параметров пограничного слоя атмосферы в ураганах. Данный метод основан на аппроксимации верхней параболической части профиля скорости ветра и восстановлении нижней логарифмической части. На основе логарифмической части получены скорость трения, скорость приземного ветра и коэффициент аэродинамического сопротивления. Полученные данные используются для верификации данных моделирования в модели WRF-ARW. Изучен ...
Добавлено: 10 декабря 2024 г.
Акельев Е. В., ВИВЛIОθИКА: E-Journal of Eighteenth-Century Russian Studies 2023 Т. 11 С. 241–270
Как практикующие историки приходят к тем или иным убеждениям? Как отличить «гипотетическое» от «доказанного»? Почему в определенный момент те или иные интерпретации находят всеобщую поддержку в научном сообществе, а другие нет? И как в дальнейшем общепризнанные интерпретации могут быть опровергнуты? Эти вопросы находятся в центре внимания этой статьи, но рассматриваются не отвлеченно, на уровне теории, ...
Добавлено: 23 ноября 2023 г.
Федотов И. А., Хританков А. С., Обидаре М. Д., Программная инженерия 2022 № 4 С. 200–208
Многосторонние соглашения используются в системах распределенного реестра и блокчейн-сетях для согласования изменений в системе. Если один из участников сети предлагает транзакцию на запись, то сначала ее должны подтвердить определенные участники сети. Многостороннее соглашение, или консенсус, определяет состав этих участников. На основе предыдущих ответов можно посчитать вероятность подтверждения транзакции для каждого из участников. В настоящей работе ...
Добавлено: 20 сентября 2022 г.
Кухаренко В. А., Зиборов К. В., Садыков Р. Ф. и др., Моделирование и анализ информационных систем 2020 Т. 27 № 4 С. 454–471
Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации ...
Добавлено: 31 мая 2021 г.
Гнатенко А. Р., Захаров В. А., Системная информатика 2020 Vol. 17 P. 21–32
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться ...
Добавлено: 9 ноября 2020 г.
Сторчевой М. А., В кн.: Мораль и универсальностьВып. 3.: М.: Издательский дом "Гуманитарий", 2020. С. 147–160.
В этой статье мы обосновываем тезис о том, что универсальная этика может быть построена на основе научного подхода, что позволяет обосновать ее универсальность и спасти от методологических обвинений в субъективизме или релятивизме. Вначале мы объясняем выбор критериев научности: 1) точная терминология, 2) корректный логический анализ, 3) эмпирическая верификация, 4) точность эмпирических измерений. Затем мы выстраиваем ...
Добавлено: 31 октября 2020 г.
Слободенюк Е. Д., В кн.: Модель доходной стратификации российского общества: динамика, факторы, межстрановые сравнения.: Издательство Нестор-История, 2018. Гл. 1.4 С. 93–116.
Глава посвящена вопросу того, какой именно должна быть черта бедности в ее монетарном относительном выражении в доле от медианы среднедушевых доходов по стране. В западных исследованиях, посвященных проблематике доходной стратификации, используются различные величины, колеблющиеся в пределах 0,5 - 0,75 от медианы среднедушевого дохода. На основе данных о рисках бедности делается вывод о том, что черта ...
Добавлено: 16 апреля 2019 г.
Кулямин В. В., Петренко А. К., Хорошилов А. В., Труды Института системного программирования РАН 2018 Т. 30 № 6 С. 367–382
В работе рассматриваются полученные недавно результаты на пути к полномасштабной верификации промышленно используемых операционных систем (ОС). Таковыми считаются не системы, разработанные в целях демонстрации определенной исследовательской идеи, а ОС, активно используемые в каких-то областях экономики и управленческой деятельности и развиваемые на протяжении значительного времени. Предлагается декомпозиция заявленной цели верификации промышленной ОС в целом на задачи ...
Добавлено: 14 февраля 2019 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.