Обсуждение

Верификация софта в последнее время становится все более популярной темой. Недавно в Channel9 было парой эпизодов, да и в публикациях от МС все чаще эта тема встречается

Как я понял, наконец-то что-то удается реальное верифицировать. Вот и растет популярность.

у меня знакомый в университете заарланда занимается верификацией ПО для автомобилей, и они как раз тесно сотрудничают с МС по этому поводу. И сам МС набирал народ (где-то в апреле 2008-го) для написания софта (на OCaml/F#) на тему верификации драйверов устройств

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

Ну, драйверы МС с 2002 года верифицирует. Нужно сказать, это сильно поспособствовало :)

Тут все вместе: организация из людей и поддерживающий ее софт. Одно без другого не работает. А менеджер был неправ тем, что требование поставил по-технарски "с запасом, на всякий случай" -- в требованиях же топа было "подешевле". Когда обнаружился огромный запас "на всякий случай", топ указал на то, что система будет работоспособна технически, но не соответствовать его ожиданиям -- это как раз валидация.

test-driven programming давно придумали

а есть ссылки на работы тех лет? я что-то не упомню массовой работы по автоматической верификации драйверов

Чем только не driven программирование... Но я тут не о программировании, а о дизайне вообще. В отличие от программирования, в дизайне есть еще и implementation -- тесты формально идут после implementation (к тестам относится запуск, а для верификации запуск необязателен).

Седьмой слайд на второй ссылке обсуждаемого поста :) "Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas, for example, driver verification we’re building tools that can do actual proof about the software and how it works in order to guarantee the reliability." Bill Gates, April 18, 2002. Keynote address at WinHec 2002 Developing Drivers with the Windows® Driver Foundation, a Microsoft Press book, is now in print, including a chapter about Static Driver Verifier (SDV), which has new rules to enable analysis of drivers written against the Kernel-model Driver Framework API

test-driven programming - это все побеждающий драйв, дизайн делается так, чтобы сразу можно было тестировать, потом пишут тесты - потом собственно имплементацию implementation - это ключевое слово в java, вспоминая мой дизайнерский опыт - подход был в принципе похож

Верификация, без присутствия человека с экспертным опытом, который сможет провалидировать её результаты -- бесполезна, а то и вредна. А учитывая все возрастающую степень доверия "умным программам", а не людям... и благодаря постоянному росту сложности этих самых умных программ... очень реальным становится сценарий, когда все результаты работы сложных систем придется принимать на веру, потому как ни у кого не будут ни знаний ни времени чтобы их оценить.

Я замечу только, что сейчас верят "умным людям" (например, "политикам, которые делают всё, чтобы победить кризис", а это не менее фатально. Люди ошибаются не меньше программ, даже в простых случаях. Людям я бы тоже не слишком доверял. А знаний и времени, чтобы оценить конкретные действия людей (которые, как и программы, хорошо работают на "тестовых примерах") так же ни у кого нет. Так что ваш людской хрен программной редьки не лучше, увы.

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

Удается. Даже я на досуге верифицирую, правда, по мелочи. Но как нибудь соберусь с силами и отверифицирую реальный код. Первую версию одного метода я уже верифицировал, но она слишком простая. Вот вторая версия будет посложнее, но ее можно назвать реальным кодом. Правда, верификация императивного кода - очень геморройное занятие в силу того что нужно записывать ограничения на состояния массивов и объектов в куче. По-моему проще все на функциональных языках переписать. Кстати, появился функциональный язык ATS, у которого система типов достаточно мощная, чтобы задавать на ней спецификации программ. Благодаря этому он по скорости сравним с С, ибо там можно писать фактически в императивном стиле, параллельно доказывая корректность, и компилятор это учитывает. http://www.ats-lang.org/

Это очень интересный вопрос: легкость верификации или ее трудность в зависимости от выбранного языка (в том числе верифицировать-то по идее не помодульно нужно, а весь код в совокупности!). Ибо идея с типами все меньше и меньше находит понимание в массах, а верификацию заменяют тестированием и юнит-тестами. Затраты же времени и сравнение по эффективности невозможны, ибо разные люди имеют производительность в кодировании на разных языках на порядки разные (т.е. мы измерим тем самым разницу интеллектов людей, а не производительность метода верификации/тестирования). Печаль, но все равно процесс потихоньку идет в массы -- хардвер уж точно верифицируется по самое не балуйся, всякие программы в истребителях, как видим, следущие на очереди. Хотя я не поверю, что выбор языка программирования для истребителя будет зависеть от выбранного способа верификации.

> Хотя я не поверю, что выбор языка программирования для истребителя будет зависеть от выбранного способа верификации. Ну для промышленной верификации вообще выбор языка невелик: Си, Джава и С# :). Ну может еще OCaml или еще какие функциональные. Си и так используется в embedded и real-time programming. Джава потихоньку тоже. Про С# не в курсе, зотя вполне возможно что Windows CE будут рано или поздно использовать и в истербителях (страшно, конечно, но на атомных подлодках уже используют) . С другой стороны в данном случае велика польза от верификации. Так что затраты на доказательство корректности императивных операций окупаются. У самолетов софт кстати тоже верифицируется. Точнее там активно используют static checking и abstract interpretation - т.е. в некотором смысле ограниченную верификацию. Французы целую школу Abstract Interpretation сделали как раз похоже в процессе создания софта для Airbus'ов. Немцы использовали верификацию Жабы для железнодорожного софта - чтобы поезда тормозили и не врезались в друг друга. Верифицировали эти модели на Жабе. Шведы и немцы верификацией очень активно занимаются.

> в том числе верифицировать-то по идее не помодульно нужно, а весь код в совокупности! В верификции модульность не проблема. Поскольку фактически создается полная модель кода, то теоремы для корректности взаимодействия модулей тоже генерируются. Т.е. если вызывается функция, то генерируется теорема для preconditions и для инвариантов. Таким образом, если все теоремы доказаны, то код в совокупности тоже отверифицирован (разумеется с учетом полноты спецификации и модели, ибо иногда полная верификация не нужна). Хуже того, атом верификации - это какое-то одно утверждение для одного пути исполнения кода в одном модуле :). Обычно для него генерируется отдельная теорема и надо ее доказать. В простеньком методе несколько путей и по нескольку утверждений для проверки. Т.е. суммарно на один несложный метод выходит 20-30 теоремок. Правда они обычно автоматически доказываются. Но доказать надо все теоремы, ибо они друг на друга полагаются, тут принцип все или ничего :).

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

Кстати насчет использования современного харда для ускорения переборных алгоритмов. Мы как-то обсуждали использования GPU для этих целей, но есть еще такой интересный дивайс как Ambric http://ambric.com/technology/technology-overview.php К сожалению из-за кризиса они приостановили операции, но вообще говоря у них на чипе 336 32-битных РИСК ядра на часто те 350 МГц, пиковая производительность 1.2 ТераОпс - похоже у них в каждом ядре можно программировать конвеер на 10 операций (точно не разобрался пока). Потребление энергии 12-15 Вт. Для переборных задач выглядит очень круто, только памяти к нему на карточках малова-то - 256 Мб. FPGA конечно потенциально покруче, но его гораздо сложнее программировать.