Компонентная верификация операционных систем

В работе рассматриваются полученные недавно результаты на пути к полномасштабной верификации промышленно используемых операционных систем (ОС). Таковыми считаются не системы, разработанные в целях демонстрации определенной исследовательской идеи, а ОС, активно используемые в каких-то областях экономики и управленческой деятельности и развиваемые на протяжении значительного времени. Предлагается декомпозиция заявленной цели верификации промышленной ОС в целом на задачи верификации различных компонентов ОС и их различных свойств, методы решения которых в дальнейшем можно интегрировать в метод достижения общей цели. На данном этапе пока рассматриваются различные подходы к решению выделенных отдельных задач. Статья является экспликацией опыта верификации различных компонентов нескольких ОС и интеграции используемых для этого технологий, полученного в рамках проектов, проводимых в ИСП РАН.