In general, there are two checking processes within the lifecycle of a system. One is verification of models describing functional specification, and the other is testing of real codes implementing the system. We developed a model checking tool can being used on both processes. Model checking systematically explores the state space of systems. The systems are expressed as the model or real code(or source code) written in programming languages such as C. There are several model checking tools that handle either the models or the real codes, but not both. In testing processes of the real codes, our model checking tool checks both the models and the real codes. The tool executes the binary code on GDB, then examines a composition with the model from which the portions of the model that correspond to the code being executed have been eliminated. A state space of the real code is a set of GDB's breakpoints corresponding to actions to communicate between the eliminated portion and others, so the model is written in a modeling language based on process algebra. This tool enables the re-use of the same model that was used in verification processes.

A model-checking approach to analyzing the robustness of procedures that suffer from human-made faults is proposed. Many procedures executed by humans incorporate fault detection and recovery tasks to recover from human-made faults. Examining whether such recovery tasks work as expected is crucial to preserve the trust and reliability inherent in safety-critical domains. To achieve this, we have employed a fault-injection method that injects a set of human-made faults into a fault-free model for a given procedure. This fault set is selected according to Swain's discrete action classification. The proposed approach uses a model checker to determine paths to error states within the model, and its properties are formalized via calculus of communicating systems and linear temporal logic.