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