上海科技大学知识管理系统

Cyber-Physical Systems (CPS) are designed to make safety-critical decisions under highly-variable and partially-observable physical environments. Thorough risk analysis should be performed to ensure the safety of CPS, by identifying all sequences of events that lead to the unsafe state. Model checking performs reachability analysis on the state space of a model, which is suitable for risk analysis of CPS. However, based on its search strategy, model checker can only return one sequence of events that leads to the unsafe state. In this paper, we propose a procedure to perform complete risk analysis on CPS software using model checking to find all different sequences of events that lead to the unsafe states.