Журнал Компьютерра -727   ::   Компьютерра

)

Еще один проект

выполняется по заказу Microsoft и

доказывает безошибочность гипервайзора

новой системы виртуализации компании.

Там, в частности, приходится доказывать,

что области памяти, выделяемые для

работы разным гостевым ОС, не

пересекаются. Конечно, я не удержался от

вопроса, а реально ли, например,

доказать "абсолютную безглючность"

Windows или микропроцессора класса

Pentium 4? Как ответил Сергей,

теоретически реально, практически нет -

слишком велик объем необходимой работы.

Для относительно простых чипов процесс

верификации уже поставлен на поток

(например, коллеги Твёрдышева доказывали

безошибочность FPU процессора Cell), с

софтом пока труднее, проект с Microsoft

- один из первых в этом роде. Не менее

сложную задачу предстоит выполнить по

заказу компании SysGo, которая готовит

операционную систему для лайнеров Airbus

(кстати, она тоже построена на принципах

виртуализации). Цитируя Сергея:

"Написать программу сейчас несложно:

берем несколько индусов, и они

быстренько ваяют код. Вот только вопрос

- насколько корректно она будет

работать. Верифицировать ее гораздо

сложнее". После этого разговора я с

некоторой опаской поднимался на борт

A320 в ганноверском аэропорту - с

системой этого авиалайнера группа

Твёрдышева не работала.



 





Фраунгоферовский институт

интегральных схем демонстрировал

оптический кабель для передачи

HD-сигнала.