Семинар «Инжиниринг современных информационных систем»
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
Страница семинара