REMES: A Resource Model for Embedded Systems

In this paper, we introduce the model REMES for formal modeling and analysis of embedded resources such as storage,energy, communication, and computation. The model is a state-machine based behavioral language with support for hierarchical modeling, resource annotations, continuous time, and notions of explicit entry and exit points that make it suitable for component-based modeling of embedded systems.The analysis of REMES-based systems is centered around a weighted sum in which the variables represent the amounts of consumed resources. We describe a number of important resource related analysis problems, including feasibility, trade-off, and optimal resource-utilization analysis.To formalize these problems and provide a basis for rigorous analysis, we show how to analyze REMES models using the framework of priced timed automata and weighted CTL. To illustrate the approach, we describe a case study in which it has been applied to model and analyze resource usage of a temperature control system.