https://opennet.ru/openforum/vsluhforumID3/81317.html В статье "Архитектура Linux Driver Verification (http://www.ispras.ru/ru/proceedings/docs/2011/20/isp_20_2011_163.pdf)" (PDF, 700 Кб) представлено описание применимости метода статического анализа кода для проверки корректности драйверов устройств для платформы Linux. Представленный метод позволяет выявить ошибки на основании анализа исходных текстов, без непосредственного выполнения кода. В отличие от традиционных методов тестирования статический анализ кода позволяет проследить сразу все пути выполнения программы, в том числе, редко встречающиеся и сложно воспроизводимые при динамическом тестировании. <br><br><br>Проект Linux Driver Verification (http://linuxtesting.ru/project/ldv) является открытым и развивается при участии организации Linux Foundation, Института системного программирования Российской Академии Наук (ИСП РАН) и Федерального агентства РФ по науке и инновациям. Наработки проекта распространяются (http://forge.ispras.ru/projects/ldv) в рамках лицензии Apache. Дополнительно под...<br><br>URL: http://www.isp https://opennet.ru/openforum/vsluhforumID3/81317.html#37 Wed, 16 Nov 2011 19:36:37 GMT &gt;Верифицировать можно только код, написанный на нормальном языке типа Ada. //obvious fix.<br><br>Причем в критичных задачах велено использовать толлько его подмножество.<br> https://opennet.ru/openforum/vsluhforumID3/81317.html#36 Wed, 16 Nov 2011 00:44:05 GMT &gt; Юр.лица, в т.ч. коммерческие компании, также как физ.лица платят налоги, и следовательно также вправе пользоваться результатами.<br><br>Пускай пользуются, мне не жалко. Я говорил, если вы не заметили, не о том, что меня зажабило как дядя какой-то в куршавеле бургундское хлещет, а о том что код с "неправильной" лицензией дядя этот заберет у сообщества за спасибо, и не поделится, а все остальные, кто за него своими налогами заплатил лососнут тунца. Компрене ? <br> https://opennet.ru/openforum/vsluhforumID3/81317.html#33 Tue, 15 Nov 2011 11:59:01 GMT &gt; Начиная с "Не стоит путать" идёт моё мнение, которое сложилось в ходе <br>&gt; общения с представителями открытых сообществ и апологетами СПО, в т.ч. вами. <br><br>Именно поэтому и укорил.<br><br>&gt; И коммерческие компании это не только Майкрософт Рус.<br><br>Разумеется. Просто другие вроде бы не замечены в попытках манипуляций общественным мнением здесь.<br><br>Вообще не рекомендую пытаться бросать тень на плетень: на каждый подобный намёк может найтись гораздо более неприятный public disclosure. Хотите обвинить в чём-либо -- скажите прямо и без попыток всунуть рекламу. Если по существу, так почему ж нет.<br><br>Пытаться выровнять несправедливое отношение к Microsoft Corp здесь обычно не стоит: люди по большей части достаточно взрослые и грамотные, чтобы либо не обращать внимания на мелочи, либо поправить вошедшего в раж собеседника. Т.е. своими "защитными" действиями Вы только усугубляете неприязнь к фирме, которая системно применяет ложь как инструмент и затем пытается обелить себя любыми средствами. Пусть исправляют в консерв https://opennet.ru/openforum/vsluhforumID3/81317.html#32 Tue, 15 Nov 2011 11:43:42 GMT &gt; Верифицировать языки Си и С++ это не правильно, т.к. по сложности они <br>&gt; не доступны для понимания. Верифицировать можно только код, написанный на нормальном <br>&gt; языке типа pascal.<br><br>Для того, чтобы быть нормальным, язык должен быть пригодным к использованию, а не верифицируемым. Несмотря на то, что эти качества не взаимоисключающие, первое качество к pascal явно не относится.<br> https://opennet.ru/openforum/vsluhforumID3/81317.html#31 Tue, 15 Nov 2011 11:09:40 GMT Одна из задач столетия звучит как (моя трактовка): "что проще: решить задачу или доказать что задача имеет/не имеет решения?". Примеры: 2+2, трансдентность числа Пи. Важно не только решение, но и используемый мат.аппарат.<br> https://opennet.ru/openforum/vsluhforumID3/81317.html#30 Tue, 15 Nov 2011 10:56:43 GMT Не займёт. Просто потому что верификация - это, собственно, доказательство соответствия кода некоторой модели. Соответственно, нам нужно иметь гарантированно корректно работающий алгоритм верификации, корректно формализованную модель и корректные предположения, положенные в основу модели. Если с первым ещё можно как-то справиться (скажем, очень большим и развесистым тестированием), то со вторым а особенно с третьим ничего не поделать. Причем описать модель частенько сложнее, чем написать сам код. Вот и думайте, где будет больше ошибок...<br><br>Верификация - это просто ещё один инструмент, не более. Ничего она не заменит - может только дополнить.<br> https://opennet.ru/openforum/vsluhforumID3/81317.html#29 Tue, 15 Nov 2011 10:52:28 GMT Ну как вы себе в реальности представляете предоставление прав только гражданам какого-то одного государства? Поэтому по факту - получается всем.<br> https://opennet.ru/openforum/vsluhforumID3/81317.html#28 Tue, 15 Nov 2011 10:10:37 GMT &gt;Верифицировать можно только код, написанный на нормальном <br>&gt; языке типа Ada.<br><br>//obvious fix.<br> https://opennet.ru/openforum/vsluhforumID3/81317.html#27 Tue, 15 Nov 2011 09:54:54 GMT Верифицировать языки Си и С++ это не правильно, т.к. по сложности они не доступны для понимания. Верифицировать можно только код, написанный на нормальном языке типа pascal.<br>