Spotlight abstraction in model checking real-time task schedulability
scientific article; zbMATH DE number 7497973