点击次数：

论文类型：会议论文

发表时间：2015-08-26

收录刊物：EI、CPCI-S、Scopus

页面范围：34-39

关键字：energy consumption modeling; cyber physical systems; time state transition matrix; software architecture; bounded model checking

摘要：CPS is kinds of networked embedded systems that combine calculating system and physical environment. Because software is the main component of CPS, its energy consumption will directly affect the trustworthiness of CPS. Software architecture can provide design model and guidance for constructing software structure, behavior and key attributes in design phase. So modeling, analyzing and evaluating the software architecture energy consumption of the CPS software can help find the energy consumption design defects, which will effectively reduce the cost and improve development efficiency. Time state transition matrix (TSTM), designed for modeling embedded software behavior, is a table-based state machine modeling language with time semantic in which the front-end is expressed in the table form and the back-end has strict formalized definition. By introducing energy consumption indicators and constraints for TSTM, form energy consumption TSTM (ETSTM), make it be suitable to the software architecture modeling of energy consumption. On this basis, the energy consumption analysis method with multiple attributes restriction based on bounded model checking technology (BMC) is provided. At last, the effectiveness of the proposed method is validated by modeling and verifying certain type train control software.