Safe decomposition of startup requirements: verification and synthesis