FORMAL SPECIFICATION OF A REAL-TIME OPERATING SYSTEM'S COMPONENT

摘要

An attempt to prepare a formal specification of a typical component of the real-time operating system kernel presented in (Halang, 1991), namely the tables describing the time schedules of tasks, and the algorithms responsible for time schedule manipulation, was made. Its main purpose was to learn how to represent entities of rather algorithmic nature in the non-algorithmic specification language used by the Prototype Verification System (PVS). The ideas underlying both the time schedules and their associated algorithms are described shortly. The way formal specifications can be prepared, on the basis of the former, is presented on a step-by step basis. As a first step, the algorithms and data structures are re-written. Then, the time schedules' operating environment, necessary from the point of view of later verification, is modeled. Next, the validity and correctness criteria for a time schedule are identified and formulated. Finally, the theorem to be used for proving basic properties is discussed.