El modelado y la verificación del comportamiento correcto de sistemas embebidos en tiempo real con restricciones estrictas de tiempo es un problema bien conocido e importante. La falta de cumplimiento de un plazo en la operación del sistema puede tener consecuencias graves en el caso práctico. Este documento propone un enfoque para el modelado formal y el análisis de planificación. Se desarrolla una extensión novedosa de las Redes de Petri llamada Redes de Petri de Tiempo con Restricciones (C-TPN), que permite el modelado de una colección de tareas en tiempo real interdependientes cuya ejecución está limitada por el uso de prioridad y recursos compartidos como procesadores y datos de memoria. Un modelo C-TPN se reduce a una red de Autómatas Temporizados en el contexto de la popular caja de herramientas Uppaal. Tanto las propiedades funcionales como, lo más importante, las temporales pueden ser evaluadas mediante la verificación exhaustiva del modelo y/o la verificación del modelo estadístico basada en simulaciones. Este documento describe y motiva primero el lenguaje de modelado C-TPN propuesto y su semántica formal. Luego, se muestra una traducción a Uppaal. Finalmente, se consideran tres modelos de sistemas embebidos en tiempo real y se verifican a fondo sus propiedades.