Download The COMPASS Examples Compendium

D31.3d - The COMPASS Examples Compendium (Public)
9
9.1
The Process Manager Example
Case Description
This example originally came from [CK04] in a VDM-SL setting. This is essentially a scheduler for a multitasking operating system. Processes are identified
by a unique identification. When a process is created it joins a list of waiting
processes and will initially be in a <READY> state.
9.2
Analysing using the Debugger
Just like for the other examples presented above the ProcessManager process can be debugged and it is possible to experiment with different possibilities.
Note that this example is using indexing over the admitted processes. Thus it is
relatively easy to create a deadlock situation here.
16