A Template System for Modeling and Verifying Agent Behaviors.

The spread of Cyber-Physical Systems (CPSs) leads developers to embed various agents in a large system. It is a complicated and difficult task to analyze and design such systems from comprehensive specifications such as an architecture document because many behaviors of many components including agents must be dealt with. In such a system, the appropriateness of interactions between components should be ensured. However, no method to efficiently define and verify behaviors in such interactions from such specifications taking into consideration the characteristics of CPSs has been proposed. To improve this situation, this paper preliminarily proposes a stepwise method to define and verify behaviors in interactions between CPS components. More specifically, a template system to stepwise define behaviors from an abstract level to a concrete level is presented based on an existing architecture modeling method. Furthermore, a model transformation tool for verifying such behavior definitions by using the model checking tool NuSMV is introduced.