Семинар «Инжиниринг современных информационных систем»

20 декабря 2024 г. (пятница), 14:00 (10:00 МСК), google-meet

Тема:
Формальный анализ протокола CAN

Докладчик:
к.т.н. Старолетов Сергей Михайлович (ИАиЭ СО РАН)

Аннотация:
В обзорном докладе рассмотрены способы формальной спецификации и верификации канального уровня CAN-шины — высокоскоростной последовательной шины с разрешением коллизий, широко используемой во встраиваемых распределенных системах управления (автомобилестроение, промышленность, авионика). Рассмотрены спецификации для трех видов контроллеров CAN и проверка этих спецификаций по 12 важным свойствам с использованием пакета MurPhi (Murφ).

Ссылка на вебинар для подключения -- https://meet.google.com/iqb-gbix-azj

Страница семинара

Семинар «Инжиниринг современных информационных систем»

11 сентября 2024 г. (среда), 14:00 (10:00 МСК), google-meet

Тема:
Управление требованиями как выравнивание и преобразование моделей

Докладчик:
Артамонов Ким Владимирович (Краудсорсинговый проект Superalign.ru)

Содокладчик:
Никифоров Денис Андреевич (Краудсорсинговый проект Superalign.ru)

Аннотация:
Взаимодействие заказчиков и эксплуатантов при реализации мультидисциплинарных проектов. Управление разработкой нормативных правовых актов, кейс Законодательного Собрания Нижегородской области. Кейс создания студенческого сообщества по моделированию доменных областей и систем поддержки общественной деятельности. Создание проблемно-ориентированных фреймворков для онтологического моделирования.

Ссылка на вебинар для подключения -- https://meet.google.com/iqb-gbix-azj

Страница семинара

Семинар «Инжиниринг современных информационных систем»

14 августа 2024 г. (четверг), 14:00 (10:00 МСК), google-meet

Тема:
LTL-спецификации специального вида для разработки и верификации управляющих программ

Докладчик:
Нейзов Максим Вячеславович (ИАиЭ СО РАН)

Аннотация:

Язык линейной темпоральной логики LTL широко применяется для спецификации свойств реагирующих систем. Однако данный формализм может применяться и для спецификации поведения таких систем. По сравнению со специализированными языками моделирования и спецификации поведения, использование языка LTL имеет некоторые преимущества: (1) отсутствует привязка к конкретному инструментальному средству, (2) LTL-спецификация является математическим объектом, что позволяет применять соответствующий математический аппарат при синтезе и анализе поведения реагирующих систем. В докладе будут представлены три LTL-спецификации специального вида: (1) декларативная — для описания поведения управляющих программ, (2) императивная — для построения императивного кода программ, (3) ограниченно недетерминированного поведения — для описания окружения управляющих программ. Использование предлагаемых LTL-спецификаций позволяет выполнять разработку и верификацию управляющих программ для замкнутых систем (систем с обратной связью).

Для демонстрации подхода используется пример установки для литья пластмасс.

Ссылка на вебинар для подключения -- https://meet.google.com/iqb-gbix-azj

Страница семинара

Семинар «Инжиниринг современных информационных систем»

19 июля 2024 г. (пятница), 14:00 (10:00 МСК), google-meet

Тема:
Моделирование работы Controller Area Network (CAN) методом проверки моделей

Докладчик:
Старолетов Сергей Михайлович (к. ф.-м. н., ИАиЭ СО РАН)

Аннотация: В докладе будут рассмотрены основные первичные документы (даташиты) CAN и трансивера MCP 2515,  алгоритмы отправки, получения сообщений и арбитража на шине, а также предложены способы моделирования протокола CAN с помощью метода Model Checking.

Ссылка на вебинар для подключения -- https://meet.google.com/iqb-gbix-azj

Страница семинара

Семинар «Инжиниринг современных информационных систем»

28 июня 2023 г. (среда), 14:00 (10:00 МСК)

Тема:
Моделирование событийно–дискретных систем (на примере задачи регулирования потоков машин с ограничениями)

Докладчик:
Шорников Юрий Владимирович (д. т. н., ИАиЭ СО РАН)

Аннотация: В докладе рассматривается пример использования гибридно-автоматного подхода для моделирования и верификации событийно–дискретных систем. В качестве модельной задачи выбрана задача управления потоками машин через мост (система Rodin).

Ссылка на вебинар для подключения -- https://meet.google.com/iqb-gbix-azj

Страница семинара

Семинар «Инжиниринг современных информационных систем»

9 декабря 2022 г. (пятница), 15:00 (11:00 МСК)

Тема:
Эффективная реализация модели ассоциативных вычислений на графических ускорителях для решения задач на графах
(соискание уч. степ. канд. техн. наук по специальности 2.3.5 - «Математическое и программное обеспечение вычислительных систем, комплексов и компьютерных сетей», отзыв ведущей организации)

Докладчик:
Снытникова Татьяна Валентиновна (ИВМиМГ СО РАН)

Текст автореферата

Ссылка на вебинар для подключения -- https://meet.google.com/iqb-gbix-azj

Страница семинара

Семинар «Инжиниринг современных информационных систем»

19 июля 2022 г. (вторник), 14:00 (10:00 МСК)

Тема:
Бесшовная объектно-ориентированная разработка

Докладчик:
Александр Наумчев

Аннотация: Проблемы переиспользования требований, проблемы с их понятностью и проверяемостью являются одними из основных угроз для программных проектов. В докладе рассматривается применение объектно-ориентированного подхода к инженерии требований, в частности, рассматривается онлайн-библиотека шаблонов требований и способы их повторного использования.. 

Ссылка на вебинар для подключения -- https://meet.google.com/iqb-gbix-azj

Страница семинара

Семинар «Инжиниринг современных информационных систем»

03 июня 2022 г. (пятница), 15:00 (11:00 МСК)

Тема:
Виды вложенности автоматов: формальная семантика (в рамках автоматно-функционального подхода)

Докладчик:
Нейзов Максим Вячеславович

Аннотация: Дается обзор вложенностей разного вида на конкретном примере, а также обсуждается их формальная семантика в терминахавтоматно-функционального подхода. 

Видео -- https://youtu.be/RevSOB8_OBc

Страница семинара

О развитии автоматного программирования:
отклик А. Шалыто на серию вебинаров ИСИС

Институт автоматики и электрометрии СО РАН и Институт систем информатики СО РАН им. А.П. Ершова проводят межинститутский семинар «Инжиниринг современных информационных систем». На серию вебинаров ИСИС получен отклик от А. А. Шалыто.

Подробнее...

Семинар «Инжиниринг современных информационных систем»

06 мая 2022 г. (пятница), 15:00 (11:00 МСК)

Тема:
Автоматно-функциональный подход к моделированию киберфизических систем (на примере Event-B модели для верификации свойств алгоритма управления движением автомобилей на мосту)

Докладчик:
Нейзов Максим Вячеславович

Аннотация: Описывается оригинальный подход к построению моделей киберфизических систем с целью их дедуктивной верификации. В качестве примера будет рассмотрена задача управления движением автомобилей на мосту. Представлена модель киберфизической системы в нотации Event-B, проведена формализация требований к системе. Верификация выполняется с помощью платформы Rodin.

видео -- https://youtu.be/891jZr-7Mos

Страница семинара