Сергей Старолетов

Avatar1

Сергей Старолетов, доцент кафедры Прикладной математики Алтайского государственного технического университета имени И.И. Ползунова
Кандидат физико-математических наук (2011 г.) Тема диссертации - Моделирование распределенных недетерминированных программных систем и их тестирование на основе автоматных мультиагентных вероятностных моделей. Преподаю курсы для бакалавров и магистров Программной инженерии - тестирование и верификация, компоненты операционных систем, функциональные языки распределенных систем, параллельное программирование, паттерны проектирования, введение в информатику (олимпиадные задачи на языке С). Имею опыт промышленной разработки в аутсорсинговых компаниях в том числе сложного сетевого программного обеспечения. В последнее время думаю над продолжением активных научных исследований в разработке и применении технологий верификации и обеспечения качества в гибридных и высоконадежных программных системах, связанных с повседневной деятельностью современных людей (умные устройства, автомобили, другая техника). Лучший молодой преподаватель АлтГТУ 2014г.


Оценка алгоритмов планирования набора задач в модели системы реального времени методом Model Checking

Моделирование программного обеспечения позволяет абстрагироваться от программных особенностей целевого языка программирования и аппаратной платформы исполнения.

Метод проверки моделей (Model checking) предполагает построение системы переходов в качестве модели программной системы и её формальную верификацию с использованием эффективных обходов данной системы и проверки выполнимости требований в виде формул темпоральной логики, содержащих ключевые переменные системы. Интересным является применение данного метода к анализу свойств операционных систем.

В работе будет продемонстрированы исполнимые модели известных алгоритмов планирования для систем реального времени (RMS, LLF, EDF и др.) на заданном наборе задач, приведены теоретические сведения по каждому алгоритму. Алгоритм реализуется в виде системы переходов на одном из модельных языков. Далее данный набор задач может быть проверен статически на возможность планирования, оценено использование времени процессора и предложен оптимальный алгоритм, если возможно.


Организаторы

При поддержке