Formal specification and verification of a real-time kernel

The paper presents a case study of application of the VDM formal method to specification and verification of a simple real-time kernel. Specifications of selected external services of the kernel are presented. Then the verification methodology is introduced by demonstrating its basic steps in relation to verification of a selected function-a process waiting for a signal on a condition variable. The experience from the study is discussed.