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

 

На

стенде университета Саарланда ученый с

исконно немецким именем Сергей Твёрдышев

рассказывал, как его исследовательская

группа (проект Verisoft XT,

www.verisoft.de) доказывает

безошибочность реализации различных

программ. Например, в 2009 году Audi

планирует выпустить новую модель A4 с

опцией dynamic steering. Идея в

следующем. Если автомобиль стоит на

месте или движется с небольшой

скоростью, то малый поворот руля

приведет к значительному изменению

положения колес, облегчая, например,

процесс парковки. А на автобане рулевое

управление, напротив, "потупеет", сделав

машину менее нервной[Идея, в принципе,

не нова, впервые она была реализована,

кажется, еще в советских луноходах. Из

автопроизводителей с динамическим

рулением экспериментировали в числе

прочих Seat и Citroen. ].



 





Конечно, если на скорости 200

км/час система вдруг переключится в

парковочный режим - последствия будут

малоприятными. Вот группа Твёрдышева и

доказывает, что все возможные варианты

поведения имплементации (контроллеров и

софта) однозначно соответствуют

первоначальной задумке. (Не путать с

отловом багов, здесь задача более

сложная - доказать полное отсутствие

ошибок относительно заданной

спецификации.