Embedded Systems in Ukraine

Согласно Adams, N.E., “Optimizing preventive service of software product,” IBM Journal of Research and Development, выявление трети ошибок всего програмного обеспечения потребуют пять тысячь лет его выполнения.

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

Большинство кода для встроенных систем имеют стоимость около $20-40  за строчку кода (расценки для американского рынка) . Об этом можно прочитать в статье David A. Wheeler “More Than a Gigabuck: Estimating GNU/Linux’s Size“.  Формальное же, математическое, доказательство отсутствия ошибок в коде может поднять стоимость до $700 за строчку

Для микроядра Secure Embedded L4, состоящего из 7,500 строчек С кода, было математически доказано отсутствие ошибок с использованием 10,000 промежуточных теорем в более чем 200,000 строчек формального доказательства. Это доказательство было проверено на компьютере, с помощью интерактивной программы доказательства теорем Isabelle.

“Proving the correctness of 7,500 lines of C code in an operating system’s kernel is a unique achievement, which should eventually lead to software that meets currently unimaginable standards of reliability.”

Посчитать количесвто строчек кода нет так просто, а тем кто хочет это сделать, могу посоветовать почитать статью на Википедии “Количество строк кода“. А для операционной системы Линукс существует замечательная утилита SLOCCount.