При разработке требований к поведению распределенных программных систем инженер должен мысленно упорядочивать и определять последовательности событий. Из-за чередования процессов количество возможных последовательностей растет экспоненциально, поэтому разработка таких требований становится нетривиальным занятием. Как следствие, инженеры ограничиваются составлением очень простых требований, которых зачастую бывает недостаточно, чтобы выразить желаемые свойства системы. В работе рассматривается расширение в линейной темпоральной логике известного и часто используемого на практике темпорального отношения leads-to (по событию--запросу когда-нибудь в будущем будет событие--отклик) на последовательность событий при помощи методики составления контекстных требований. Основным результатом данной работы является построение формальных требований к системе управления энергоснабжением судна на основе данной методики. Формальная верификация этих требований методом проверки модели позволила выявить несколько ошибок в поведении системы, допущенных при ее проектировании, 3 из которых оказались критическими.