В рамках проекта Tokeneer, подразумевающего автоматизацию контроля доступа в помещения на основе биометрической информации, агентство национальной безопасности США (АНБ) отрабатывало процесс создания надежных программных систем. Главная цель этого проекта заключалась не столько в создании такого комплекса, сколько в совершенствовании технологий разработки математически верифицированного ПО, не содержащего ошибок и выполняющего только заданные функции. Удивительно, но при создании Tokeneer был почти достигнут абсолютный уровень качества — всего одна ошибка на десять тысяч строк исходных текстов.

В исполнители проекта была выбрана компания Praxis High Integrity Systems, в первую очередь за счет применяемой ею методологии разработки Correctness-by-Construction (CbyC). Она была создана в рамках инициативы National Cyber Security Partnership, предложенной Белым домом США в 2003 г. для реализации национальной стратегии по безопасности киберпространства. Эта инициатива, в частности, нацеливалась на противодействие растущим хакерским угрозам, которые часто используют ошибки в софте, и выработку эффективных методик создания ПО, обеспечивающих минимальное число ошибок. Играл роль и экономический фактор: в 2002 г., по оценкам национального института стандартов и технологий США NIST, потери от низкокачественного софта в США составили 60 млрд. долл., при этом лишь четверть ИТ-проектов завершалась успехом.

При разработке CbyC ставились цели обойти по коммерческой эффективности массово распространенные практики подобного назначения, а также обеспечить устойчивое качество ПО на протяжении всего жизненного цикла даже при активном внесении в него изменений. Был использован 15-летний опыт подрядчика в создании критически важного ПО, и в итоге результативность применения CbyC достигла уровня 0,1 ошибки на 1000 строк кода при сохранении высокой продуктивности кодирования (30 строк в день на человека). Так, проект Tokeneer объемом 9939 строк занял 260 человеко-дней, и в нем была выявлена всего 1 ошибка. Для сравнения: организации, сертифицированные по высшему, пятому уровню популярной модели зрелости процессов разработки ПО CMM, показывают качество на порядок хуже.

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

1. Использовать формальную и наглядную нотацию где только возможно. Так, в проекте Tokeneer для создания спецификаций применялся формальный типизированный язык Z, созданный математиками в 1977 г. и основывающийся на теории множеств, лямбда-исчислениях и предикатах первого порядка. Он был стандартизован ISO в 2002 г., а общедоступную среду для построения Z-спецификаций ZETA можно скачать на сайте uebb.cs.tu-berlin.de/zeta/.

Управление проектными требованиями выполнялось по методике REVEAL, состоящей из трех правил:

— постоянный контакт с заказчиком, совместные семинары по упрощению требований, оперативное выявление и урегулирование конфликтов и недопониманий, регулярные проверки проекта с представителями обеих сторон;

— непрерывное отслеживание требований — насколько они актуальны и точны, правильно классифицированы и удобны для тестирования;

— ведение модели, объясняющей, почему и как требования связаны друг с другом.

Кодирование происходило в созданной на деньги британского МО среде SPARK на языке Ада, что исключало немало ошибок (например, переполнение буфера), характерных для ряда популярных массовых систем и языков. В SPARK упрощена семантика Ады, добавлены средства верификации кода (SPARK Examiner), контроля корректности его оформления, разработчику предлагается набор формальных правил и ограничений, исключающих большинство типовых ошибок при кодировании.

Применялась также среда GNAT Pro фирмы AdaCore, заключившей этой осенью с Praxis стратегическое партнерство по ее развитию и стыковке со SPARK.

2. Проверять проектные сущности с помощью инструментов — отслеживать математическую корректность спецификаций, выполнять статический анализ кода и т. д.

3. Вносить изменения малыми частями и полностью тестировать итоговую модель после каждой модификации.

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

5. Код точно отражает спецификацию и пишется с прицелом на его легкие верификацию и тестирование.

6. Наиболее сложные требования реализуются первыми.

Препятствия к внедрению подобных методик, отмечают ее авторы, кроются в корпоративной культуре и ошибочных мнениях, что “программ без ошибок не бывает” или “в нашей организации это не пройдет”. Но, конечно, для перехода на CbyC или ей подобные технологии требуются определенные усилия, хотя и не очень большие — программистам АНБ понадобилось 12 недель практики “на лету” с минимальной переподготовкой. Но ответственный за этот процесс должен обладать хорошим инженерным мышлением.

В октябре 2008 г. были опубликованы исходные коды и другие проектные материалы Tokeneer, доступные на сайте www.adacore.com/home/gnatpro/tokeneer/.