El modelado de requisitos formales y la gestión de trazabilidad son esenciales para implementar eficazmente la Ingeniería de Sistemas Basada en Modelos (MBSE). Sin embargo, pocos estudios han explorado la integración del modelado de requisitos, la gestión de trazabilidad y la verificación dentro de las metodologías de ingeniería de sistemas basadas en MBSE. Además, el lenguaje de modelado predominante para MBSE, SysML, carece de capacidades suficientes para la descripción de requisitos y la gestión de trazabilidad, así como para representar atributos físicos y capacidades ejecutables, lo que dificulta la verificación colaborativa de requisitos funcionales y no funcionales. Este artículo propone un enfoque integrado para el modelado de requisitos, la gestión de trazabilidad y la verificación, basándose en el modelado integrado previamente propuesto y el lenguaje de simulación llamado lenguaje X. Nuestras contribuciones incluyen principalmente la definición de la especificación ReqXL para el modelado de requisitos orientado a MBSE basado en el lenguaje X, la propuesta de un algoritmo para generar automáticamente trazas de requisitos, y se desarrolló un marco integrado para el modelado de requisitos, la gestión de trazabilidad y la verificación combinando el lenguaje X con ReqXL. Estas funcionalidades fueron personalizadas en la plataforma de modelado y simulación integrada autodesarrollada, XLab, que está específicamente diseñada para el lenguaje X. Además, mostramos la eficacia y promesa de nuestro enfoque a través de un estudio de caso que involucra el diseño de un sistema eléctrico de aeronaves.