A Spiral Proceb of Modeling and Verifying the Scheduling Mechanism of OSEK/VDX in OTS/CafeOBJ Method

Formalization and verification of a system usually are not one time tasks, particularly when the system to be formalized and verified is complicated. The relation between formalization and verification should not be sequential but iterative in that verification follows formalization and in turn helps validate and refine formalization. The iteration is a spiral proceb with a formal model being incrementally developed and more and more properties being verified. In this paper, we present a case study to demonstrate how we formalize and verify in the spiral way a scheduling mechanism and Priority Ceiling Protocol of an industrial automobile standard, i.e. OSEK/VDX, in OTS/CafeOBJ method, an algebraic approach to modeling and verifying systems by interactive theorem proving in CafeOBJ. We start with a prototypical model of the scheduling mechanism, validate and refine it based on verification results. By theorem proving, it reinforces the specifier's understanding of the specifications and their relationship with the specified problem domains. The formal model is refined until all these properties are succebfully proved. We then incrementally extend it to cover more complicated part and verify more properties such as exclusion, deadlock freedom, priority inversion freedom.