This work proposes structuring formal models using promise theory and System Theoretic Process Analysis (STPA). Promise theory enables reasoning about a system’s dependency structure and information locality, a common source of complexity in cyber-physical systems. STPA, on the other hand, provides the safety constraints that a formal model must satisfy. The core idea behind the proposed approach is to prioritize modeling those parts of the system requirements that are least likely to change in later stages, hence supporting early validation through animation. We illustrate our approach by applying it to a moving block system - a prototype of a novel train protection system in the railway domain, which is currently being investigated as part of Europe’s Rail Joint Undertaking.