Verification of CPS Based on Control Loop Using Model Checking

CPS (Cyber Physical System) includes a complicated architecture that spans cyber space and physical space. There are several relationships related to the transmission of data and energy and the control and monitoring of CPS components. Many control loops exist, and these control loops represent the cyclic relations of components based on the relationships mentioned above. Design faults in the control loops can cause accidents, and so we propose a method of verifying the stability of control loops to ensure safety in CPS. In the proposed method, control loops are identified in an architecture model proposed by us. An identified control loop is converted into a temporal logic formula, and the stability of a control loop is verified using a model checking tool. The effectiveness of the proposed method was confirmed by applying a farm monitoring system, which can be considered a type of actual CPS.