ymik ([info]ymik) wrote,
@ 2009-09-29 13:00:00
Previous Entry  Add to memories!  Tell a Friend  Next Entry
"Нет, сынок, это фантастика!" (с)
Невероятной новостью поделился 3dnews: создан безошибочный код из 7500 строк! Такого не может быть, потому что такого просто не может быть!

«Исследователи из Университета Нового Южного Уэльса (The University of New South Wales, UNSW) и Национального исследовательского института Австралии в области информации и коммуникационных технологий (National ICT Australia, NICTA) добились прорыва в программном обеспечении, который существенно увеличит безопасность и надёжность кода и имеет потенциал для коммерческого успеха. По словам профессора компьютерных наук и директор исследовательских программ в NICTA Гернота Хайзера (Gernot Heiser), впервые команда смогла доказать с математической точностью, что ядро операционной системы – код в "сердце" любого компьютера – на 100% свободен от ошибок ("багов") и следовательно устойчив к сбоям и отказам.»

«По приблизительной оценке качественно разработанное программное обеспечение имеет около 10 ошибок на тысячу строк кода, а очень качественное – от 1 до 3, - поясняет Хайзер. Это означает, что в системах множество недочётов. Мы же показали возможность добиться намного меньшего, предельного уровня, причём наиболее подверженная риску часть имеет доказанную отказоустойчивость. Я думаю, не будет преувеличением сказать, что это открывает совершенно новый мир для создания систем с высокими показателями надёжности и безопасности»

«– Верификация окончательно подтвердила возможность существования кода без ошибок, и в будущем ничто менее передовое не должно признаваться приемлемым в особо важных приложениях»

Я не верю!



(11 comments) - (Post a new comment)


[info]raydac
2009-09-29 09:46 am UTC (link)
то что не работает, не имеет ощибок

(Reply to this) (Thread)


[info]ymik
2009-09-29 11:24 am UTC (link)
гм :) с этой точки зрения даже не посмотрел! :)

(Reply to this) (Parent)(Thread)


[info]raydac
2009-09-29 11:28 am UTC (link)
забавно будет если они продвигают со своей стороны тоже "автоматное программирование" которое с нашей продвигает Анатолий Шалыто и которое потенциально должно сильно снижать процент ошибок

p.s.
мой рекорд помню был - 4000 отлаженных строк за день эмулятора который заработал и отэмулировал то что надо, что показывает что ошибки там если и были то не из тех что бы не дать заработать софтине, но я тогда был молодой длинноногий и политическиграмотный..

(Reply to this) (Parent)(Thread)


[info]ymik
2009-09-29 11:34 am UTC (link)
тут фишка в том. что они математически же это доказали

(Reply to this) (Parent)(Thread)


[info]sleepy16
2009-09-30 11:38 am UTC (link)
+1

другой вопрос, сколько времени (лет!) заняла эта формальная математическая проверка, и для каких возможных входных данных и условий это доказательство действительно :)))))

(Reply to this) (Parent)(Thread)


[info]ymik
2009-09-30 02:35 pm UTC (link)
7 человеколет

(Reply to this) (Parent)


[info]permea_kra
2009-09-30 05:29 am UTC (link)
http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.pdf

(Reply to this) (Parent)(Thread)


[info]ymik
2009-09-30 07:39 am UTC (link)
спасибо! Сейчас прочитаю :) Особенно интересно, как они задачу формулировали.

(Reply to this) (Parent)


[info]sleepy16
2009-09-30 11:45 am UTC (link)
спасибо, посмотрела. они сделали доказательство для очень простого процессора ARM.

а абсолютное большинство обычных выпускаемых процессоров не подлежат формальной проверке, поскольку много операций недетерминированы, да еще и поведение их часто отклоняется от формально документированного.

вобщем все это очень и очень сложно и нереалистично. за обозримое время и деньги можно доказать какое-то одно довольно простое свойство, в лучшем случае несколько, но не общее отстуствие ошибок.

(Reply to this) (Parent)


[info]andy_scott
2009-09-30 07:15 am UTC (link)
Вот, нашел: безбажники из Австралии. Сорри перепутал, про "железную" ОС это следующий его пост,то другое.

(Reply to this) (Thread)


[info]ymik
2009-09-30 07:40 am UTC (link)
да, сейчас просмотрю материалы, особенно тот пдфник из комментария выше

(Reply to this) (Parent)


(11 comments) - (Post a new comment)

Create an Account
Forgot your login or password?
Log in with OpenID
English • Español • Deutsch • Русский…