Towards Design and Implementation of Model Checker for System Software

A model checker is under development as one of the static program checkers for the forthcoming Dependable Embedded Operating System. The checker is designed with priority for scalability, because model checking based on predicate abstraction is promising, but it is not yet applicable to large system software like operating systems. Since the checker is intended to be run everyday in nightly builds, abstraction refinement is not performed on-line but is assumed to be given as hints, because repeating the same refinement is wasting and refinement such as invariant finding sometimes needs human involvement. Being freed from abstraction refinement, the checker can properly handle loops and function calls, and it can keep track of multiple states simultaneously through function calls which is deemed to reduce the cost of state transition calculation. Necessary annotations are provided based on the P-Bus interface, which is a proposed abstract interface internal to the operating system kernel that cleanly separates functionalities of operating systems. The checker works on simple properties attached to the interface in the format of commonly used specification languages.