Correctness proof of an operating system kernel for hard real time computing

An architecture (including both hardware and software solutions) for an operating system kernel to be employed in hard real tune, environments is shortly described, and its functionality is presented By considering its application areas, which comprise safety critical systems, the need for correctness of such a kernel is pointed out. Ways to achieve this property are identified in the context Of appropriate correctness criteria. It is discussed how proper formal methods are selected for verification, and to which particular task each method is applicable. Experiences and observations are presented. As one of the latter, the need to apply both theoretical (formal) and practical methods is underlined, Therefore, a simulator for the kernel was developed, whose functionality is described as well.