Name
Abstract | ||
|---|---|---|
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 training system, which teaches a humanoid soccer robot 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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-16841-8_48 | ROBOT INTELLIGENCE TECHNOLOGY ANDAPPLICATIONS 3 |
Keywords | Field | DocType |
Model Checking,Formal Verification,Training System for Humanoid Robot Soccer,NuSMV | Computation tree logic,Model checking,Simulation,Computer science,Correctness,Finite-state machine,Soccer robot,System model,Formal verification,Humanoid robot | Conference |
Volume | ISSN | Citations |
345 | 2194-5357 | 1 |
PageRank | References | Authors |
0.35 | 10 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yongho Kim | 1 | 17 | 5.11 |
| Mauricio Gomez | 2 | 5 | 3.19 |
| James Goppert | 3 | 7 | 1.91 |
| Eric T. Matson | 4 | 276 | 42.52 |