Z (pronounced Zed) is a rigorous specification language developed in the 1980s. It uses sets to describe system states plus required invariants, operations, and pre- and post-conditions. This paper is a tutorial demonstrating the usability of Z and it’s tools on a real operating system called FreeRTOS. Z precisely describes the micro-kernel application program interface (API), ProZ animates the specifications, and Z/Eves verifies properties. The focus is on how to use Z/Eves to prove that the operations maintain the invariants and that the initial states are attainable. I was surprised by the care needed to prove mostly obvious theorems.

Much of the Z notation is explained in the paper. If you know Z, there are a few surprises--for example: defining ΔTask in a schema on page 177 and using “topReadyTask” on page 183 to label a formula in a schema so it can be used in a proof. The formula might be simplified by using the “max” function in the Z mathematical toolkit [1]. I spotted one trivial typographical error: “TaskProperty5” is listed as “TaskPriority5.” This is not in the web version [2].

I was happy to see that the authors invite others to use different methods on FreeRTOS. If I were not retired, I would point a graduate student at FreeRTOS. The authors plan to verify the code. Using mathematics and logic plus Floyd’s methods let me show that my code satisfied its specifications and/or discovered bugs back in 1970. It should be easier now.