El Bus de Vehículo Multifunción (MVB) es un componente crítico en la Red de Comunicación del Tren (TCN), que se utiliza ampliamente en la mayoría de las técnicas de trenes modernos del sistema de transporte. Cómo garantizar la seguridad del MVB se ha convertido en un tema importante. Las pruebas tradicionales no podían garantizar la corrección del sistema. En este documento se abordan el modelado y la verificación del sistema MVB. Se utilizan métodos de Red de Petri y de verificación de modelos para verificar el sistema MVB. Se presenta un enfoque de Red de Petri Jerárquica y Coloreada (HCPN) para modelar y simular el protocolo de Transferencia Maestra del MVB. Se proponen métodos síncronos y asíncronos para describir las entidades y el entorno de comunicación. Se diseña un modelo de autómatas del protocolo de Transferencia Maestra. Basándose en nuestra plataforma de verificación de modelos MC, se verifica el protocolo de Transferencia Maestra del MVB y se encuentran