Modelization and verification of a multiprocessor realtime OS kernel.
Thierry Cattel · 1994
ion Features abstract concrete Interruptions interprocessor hardware FIFO software mailboxes physical several priorities several priorities Intertask communication channels _TD_service FSM Task mngt creation synch. + offsprings synch. + offspr. +queues destruction synch. + offsprings synch. + offspr. +queues Scheduling nondeterministic priority preemptive Fig.2.1 - Criterias for incremental modelization approach The best abstraction for interprocessor interrupts management is having a FIFO on each processor that memorizes the pending interrupts ; this is exactly what a hardware FIFO does. We could not find any more abstract model for physical interrupts than the detailed one that mimics reality. Communication through PROMELA channels is the obvious abstraction for intertask communication. Apart from looking at a particular aspect of it, (e.g. synchronization and offsprings tree management), it is difficult to produce an abstraction for task management. A non deterministic schedu...