Using formal reasoning on a model of tasks for FreeRTOS

摘要

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.