Modeling and formal verification of a telecom system block using MDGs