We report the experience of the Software Engineering Laboratory of the National Research Council of Canada with the modelling and verification of the kernel of Harmony, a portable real-time multitasking multiprocessor operating system. We explain the aim of this study and give the first results. We use a modelling approach and formalize the models of the system, the scenarios and the properties that are to be checked in PROMELA using the SPIN tool. Several models of the systems were produced with various degrees of abstraction and completeness. The most recent is a tractable one that enables the expression, simulation and verification of any scenario that consists of a bounded number of tasks that may use all the services of the kernel. An exhaustive verification of the intertask communication features of Harmony was carried out by model-checking. It revealed a bug that has been in the system for more than ten years. The first verifications of the dynamic task management primitives lead to the discovery of other bugs and serious critical races. We show that it is possible to detect more than deadlocks when using formal methods for the study of a real medium-sized operating system that encompasses complex internal management