Трансформация и верификация программы сортировки прикрепленных к шине устройств

Трансформация и верификация программы сортировки прикрепленных к шине устройств

Язык статьи
Русский
Аннотация
Описывается трансформация и верификация программы bus_sort_breadthfirst, принадлежащей ядру ОС Linux и реализующей сортировку устройств, прикрепленных к шине компьютера. Программа трансформируется с языка Си в язык cP с раскрытием макросов, реорганизацией структур и устранением указателей. Далее программа преобразуется на язык функционального программирования WhyML. Для полученной программы строится спецификация и проводится дедуктивная верификация.
УДК
Страницы
1-34
Файл
Номер