Analyzing Systems Dependent on Execution Speed with Model Checker

When computational resources are limited, system behavior depends on the execution speed of the processor(s). In such cases, it is difficult to exhaustively analyze system behavior via simulations. Model checking is a verification technique for reactive systems, which is widely used not only in academic research but also in industrial development. We describe a target system to be verified as a labeled transition system and its specification as temporal logic formulae. A model checker then automatically checks that the system satisfies the specification by exhaustively searching the execution paths. In this paper, we propose a technique for the exhaustive analysis of systems dependent on processor speed. We present a case study of a savings bank with an attached electronic coin counter controlled by a tiny microprocessor. We analyze the electronic savings bank using the SPIN model checker. The case study shows the effectiveness of this formal approach in finding the causes of troubles that depend on the execution speed.