Изначально контрактные спецификации были предложены
Изначально контрактные спецификации были предложены для описания интерфейсов программных компонентов, но при определенной доработке их вполне можно использовать для описания модулей аппаратного обеспечения. Такие спецификации, с одной стороны, удобны для разработчиков, поскольку хорошо привязываются к архитектуре системы, с другой стороны, на их основе можно автоматически генерировать тестовые оракулы, проверяющие соответствие поведения целевой системы требованиям, описанным в спецификациях. Практическая апробация подхода в проекте по тестированию буфера трансляции адресов микропроцессора показала удобство представления требований к аппаратуре в форме пред- и постусловий и продемонстрировала сравнительно небольшую трудоемкость разработки спецификаций. На настоящий момент нами получен определенный опыт использования технологии тестирования UniTESK и инструмента CTESK для спецификации и тестирования моделей аппаратного обеспечения. Опыт показывает, что некоторые шаги разработки тестов могут быть полностью или частично автоматизированы. Детальное исследование этого вопроса и разработка инструментальной поддержки для автоматизации шагов разработки тестов является основным направлением дальнейшей работы.
