Schedulability Analysis Of Multi-Processor Real-Time Systems Using Uppaal

Multi-processor execution platforms are being more and more commonly adoptedin various real-time systems. In some systems, real-time tasks are generated at runtimeto be executed under time constrains, e.g. interruptions triggered by events should behandled preemptively within their deadlines. Besides some other system verifications,checking whether all the real-time tasks can be finished within their deadlines, i.e.schedulability analysis is a very critical step in the designing phase. In this paper, webreak down a typical multi-processor real-time system into the following modules: thehardware environment, the task system and the multi-processor execution platform.Then we develop a general model capturing the independent and interactive behaviorsof these modules by modeling them as timed automata using the model-checking toolUppaal, which enables us to perform formal verifications and schedulability analysisunder one framework. We present verification results on small systems with a fairlysmall number of tasks and processors and it proves a general and ?exible model whichsystem designers can customize according to a certain system specification.