Курсы Лекторы Материалы О проекте
Курсы Лекторы Материалы О проекте
Войти
Лекция 11. Наблюдаемая эквивалентность. Планировщик процессов (пример)
Лекция из курса:
Формальная семантика и верификация программного обеспечения
Миронов Андрей Михайлович
Видео не может быть загружено из-за проблем с интернет-соединением или проблем на сервере. Или формат файла не поддерживается вашим браузером.
Лекция 11. Наблюдаемая эквивалентность. Планировщик процессов (пример)
Видео закончится через
NaN:NaN
00:00
00:00
00:15
Следующая секция начнется через 06:46
Наблюдаемая эквивалентность процессов
06:46
Следующая секция начнется через 06:46
Постановка задачи и планы на следующую лекцию
09:48
Следующая секция начнется через 06:46
Другое определение наблюдаемой эквивалентности процессов
15:28
Следующая секция начнется через 06:46
О свойствах наблюдаемой эквивалентности (по аналогии с сильной эквивалентностью)
22:52
Следующая секция начнется через 06:46
Планировщик для операционной системы (пример)
39:49
Следующая секция начнется через 06:46
Представление работы планировщика с помощью циклеров
46:33
Следующая секция начнется через 06:46
Формальное доказательство свойства (последовательность действий, генерируемых планировщиком и обозначенных альфа, является правильной циклической последовательностью)
1:16:08
Следующая секция начнется через 06:46
Схема дальнейшего доказательства
1:20:38
Следующая секция начнется через 06:46
Модификация задачи
Свернуть таймкоды
00:00
00:00
Скорость
x 1.00
x 0.25
x 0.50
x 0.75
x 1.00
x 1.25
x 1.5
x 1.75
x 2.00
x 3.00
x 4.00
Качество
1080p
1080p
720p
480p
00:00
00:00
Скорость
x 1.00
x 0.25
x 0.50
x 0.75
x 1.00
x 1.25
x 1.5
x 1.75
x 2.00
x 3.00
x 4.00
Качество
1080p
1080p
720p
480p

Лекция 11. Наблюдаемая эквивалентность. Планировщик процессов (пример)

00:15
Следующая секция начнется через 06:46
Наблюдаемая эквивалентность процессов
06:46
Следующая секция начнется через 06:46
Постановка задачи и планы на следующую лекцию
09:48
Следующая секция начнется через 06:46
Другое определение наблюдаемой эквивалентности процессов
15:28
Следующая секция начнется через 06:46
О свойствах наблюдаемой эквивалентности (по аналогии с сильной эквивалентностью)
22:52
Следующая секция начнется через 06:46
Планировщик для операционной системы (пример)
39:49
Следующая секция начнется через 06:46
Представление работы планировщика с помощью циклеров
46:33
Следующая секция начнется через 06:46
Формальное доказательство свойства (последовательность действий, генерируемых планировщиком и обозначенных альфа, является правильной циклической последовательностью)
1:16:08
Следующая секция начнется через 06:46
Схема дальнейшего доказательства
1:20:38
Следующая секция начнется через 06:46
Модификация задачи
Свернуть таймкоды
Конспект лекции
Лекция 11. Наблюдаемая эквивалентность. Планировщик процессов (пример)
1 / 4