Компьютерра, 2008 № 11 (727) | страница 29
В девятом павильоне Цебита традиционно располагается "Future park", собирающий всевозможные инновации, которые еще не пошли в серию. Основу его экспозиции составляют стенды немецких университетов, а вместо ушлых менеджеров по продажам посетителей обычно встречают сами авторы разработок - студенты, аспиранты и их старшие коллеги. Естественно, и рассказывают они о подопечных технологиях другими словами и с иными эмоциями, нежели специально нанятые стендисты, быстренько проштудировавшие за полдня каталог товаров фирмы, о которой до этого и слыхом не слыхивали.
На стенде университета Саарланда ученый с исконно немецким именем Сергей Твёрдышев рассказывал, как его исследовательская группа (проект Verisoft XT, www.verisoft.de) доказывает безошибочность реализации различных программ. Например, в 2009 году Audi планирует выпустить новую модель A4 с опцией dynamic steering. Идея в следующем. Если автомобиль стоит на месте или движется с небольшой скоростью, то малый поворот руля приведет к значительному изменению положения колес, облегчая, например, процесс парковки. А на автобане рулевое управление, напротив, "потупеет", сделав машину менее нервной[Идея, в принципе, не нова, впервые она была реализована, кажется, еще в советских луноходах. Из автопроизводителей с динамическим рулением экспериментировали в числе прочих Seat и Citroen. ].
Конечно, если на скорости 200 км/час система вдруг переключится в парковочный режим - последствия будут малоприятными. Вот группа Твёрдышева и доказывает, что все возможные варианты поведения имплементации (контроллеров и софта) однозначно соответствуют первоначальной задумке. (Не путать с отловом багов, здесь задача более сложная - доказать полное отсутствие ошибок относительно заданной спецификации.)
Еще один проект выполняется по заказу Microsoft и доказывает безошибочность гипервайзора новой системы виртуализации компании. Там, в частности, приходится доказывать, что области памяти, выделяемые для работы разным гостевым ОС, не пересекаются. Конечно, я не удержался от вопроса, а реально ли, например, доказать "абсолютную безглючность" Windows или микропроцессора класса Pentium 4? Как ответил Сергей, теоретически реально, практически нет - слишком велик объем необходимой работы. Для относительно простых чипов процесс верификации уже поставлен на поток (например, коллеги Твёрдышева доказывали безошибочность FPU процессора Cell), с софтом пока труднее, проект с Microsoft - один из первых в этом роде. Не менее сложную задачу предстоит выполнить по заказу компании SysGo, которая готовит операционную систему для лайнеров Airbus (кстати, она тоже построена на принципах виртуализации). Цитируя Сергея: "Написать программу сейчас несложно: берем несколько индусов, и они быстренько ваяют код. Вот только вопрос - насколько корректно она будет работать. Верифицировать ее гораздо сложнее". После этого разговора я с некоторой опаской поднимался на борт A320 в ганноверском аэропорту - с системой этого авиалайнера группа Твёрдышева не работала.
