Empirical studies of automatic verification for OS scheduler

摘要

It is important to verify reactive programs (i.e. OS) and guarantee qualities. But in exesiting studies, there have been studies of verifications for only finite state transition systems and abstract model. In this paper we propose automatic verification method for reactive systems. Automatic verification is possible,because we construct finite state transition systems from reactive systems by abstracting infinite data damains info finite domains. Finally, we show our methods effective by verification using SMV.