Model checking is a technique to perform a formal verification process that allows a system to have robustness and correctness. In a given system model as a Finite State Machine (FSM), model checker explores all possi...
详细信息
ISBN:
(纸本)9783319168418;9783319168401
Model checking is a technique to perform a formal verification process that allows a system to have robustness and correctness. In a given system model as a Finite State Machine (FSM), model checker explores all possible states in brute-force manner. In this paper, we apply this technique to a trainingsystem, which teaches a humanoidsoccerrobot how to intercept a ball that is passed from other players, to verify that the system is failure-safe in a given requirements. Several Computation Tree Logic (CTL) properties to define a critical or potential situation are specified based on the functionality of the system. We show the results of the given properties using NuSMV, a symbolic model checker introduced by Carnegie Mellon University.
暂无评论