Разработка спецификаций модуля
Основные требования к буферу трансляции адресов были получены в письменной форме от разработчиков модуля. В процессе формализации требования уточнялись в результате общения с разработчиками и чтения технической документации. Следует отметить, что все сформулированные разработчиками требования были легко представлены в форме пред- и постусловий.
Проект продемонстрировал удобство и сравнительно небольшую трудоемкость разработки контрактных спецификаций для моделей аппаратного обеспечения. Спецификации были разработаны одним человеком за ≈2 недели, а их объем составил ≈2 500 строк кода на SeC. Отметим также, что в результате проекта было найдено несколько ошибок в реализации модуля.
