La arquitectura de Aviónica Modular Integrada (IMA) proporciona al software aéreo un mecanismo de particionamiento temporal robusto, que logra un confinamiento confiable de fallas entre aplicaciones de aviónica. Sin embargo, la programación de particiones de un sistema IMA es un problema de optimización no lineal no convexo complejo, lo que dificulta resolver la asignación temporal óptima para particiones mediante métodos analíticos tradicionales. Este artículo presenta un enfoque basado en modelos para optimizar la programación de particiones de sistemas IMA, cuyo comportamiento temporal se modela como una red de autómatas temporizados. Dado un modelo de sistema, el optimizador emplea un algoritmo genético paralelo para buscar los parámetros óptimos de recursos de partición con respecto a la ocupación mínima del procesador. Para cada combinación prometedora de parámetros, las restricciones de planificación y la ocupación del procesador del sistema se evalúan de manera precisa mediante la Verificación de Modelos Clásica y Estadística (es decir, CMC y SMC), respectivamente. También aplicamos pruebas de hipótesis de SMC para la falsificación rápida de soluciones no planificables, acelerando así la verificación de planificabilidad basada en CMC. Dos estudios de caso demuestran que nuestro enfoque propuesto supera a los métodos analíticos clásicos en la ocupación del procesador de sistemas IMA típicos.