Modeling and verification of interactive behavior for cyber-physical systems

Energy Consumption Interaction Automata (ECIA) is presented to model cyber-physical systems´ interaction behavior and energy consumption constraint information. The component-interaction automata is an excellent model for specifying architecture and behavior information, but fails to depict energy consumption constraint information in cyber-physical systems. ECIA extends the description ability of component interaction automata by binding each action with an energy consumption interval. ECIA models of cyber-physical systems can be composed together based on the ECIA composition definition we presented in this paper. Applications of ECIA, such as specifying and verifying components´ interaction properties in the design stage of developing component-based cyber-physical systems, are discussed. An example is given to demonstrate how ECIA can be used to analyze the energy-related properties of components´ behavior in cyber-physical systems.