Введение в изучение методов обеспечения качества необходимо для понимания разработки сложного и надёжного программного обеспечения. Тем не менее, современная индустрия программного обеспечения требует скорейшего вывода продукта на рынок, а методы формальной спецификации и верификации программ не вызывают особого интереса у широкой массы будущих программистов. В данной статье автор предлагает организовать специальную дисциплину и проводить обучение тестированию, разработке через тестирование и методам формальной верификации с использованием различных методов написания спецификаций и программных средств проверки программ. Цель настоящей дисциплины — пересмотреть отношение будущих разработчиков к качеству программного обеспечения, его спецификации и необходимости автоматической проверки. В рамках данной статьи автор рассматривает собственную дисциплину, объединяющую по сути два курса — тестирование программного обеспечения и формальную верификацию. Предлагаемый подход к обучению в первую очередь практико-ориентирован и включает командную работу. В соответствии с действующим учебным планом дисциплина проводится в последнем семестре для студентов бакалавриата (4 курс). Материал статьи основан на пятилетнем опыте преподавания автора данной дисциплины студентам направления “Программная инженерия”. В статье приведены достаточно объемные и наглядные примеры спецификаций и программ на модельных языках.