Hi Jorge,Further e-mail about this I'll write. And about B-toolkit, he was kind enough to CC to the L4 formal method author. And about scheduler I was correct.
We have actually removed the need for sigma1 (and sigma0). On our
latest version it does not exist.
Few questions I have for my self, and for Ben off course.