В этой статье мы формально описываем системы реального времени с абстрактным планировщиком, используя модели Крипке. Эта формализация позволяет специализировать абстрактный планировщик в терминах построенной модели. Мы иллюстрируем этот подход с помощью системы реального времени, в которой работы являются невытесняемыми и имеют фиксированный приоритет (NE-GFP). Мы также формулируем свойство безопасности для систем реального времени, используя линейную временную логику LTL. Мы реализуем нашу формализацию систем реального времени с планировщиком NE-GFP на языке Promela, используемом в инструменте проверки SPIN, и проводим эксперименты для доказательства/опровержения свойства безопасности, чтобы оценить эффективность нашего подхода.