Towards Sustainable Development of Energy-Aware Systems names: yv=. The parallel composition A || B of A and B has the following form: A || B = |[ expu; vars; impr; do [] iIJ a i :: A i od ]| where u=yv, s=xw and r=(zt)u. The initial values and locations of the variables, as well as the actions in A || B consist of the initial values, locations, and the actions of the original systems, respectively. The well-definedness of A || B is en- sured by the fact that all its variables have unique names. Thus, the exported and local variables of A and of B have distinct names, and moreover, the local variables of A can always be renamed in order not to be homonym with the exported variables of B (and vice versa). The binary par- allel composition operator `||' is associative and commutative, and thus extends naturally to the parallel composition of a finite set of systems. The parallel composition A || B defines a more not consume any (noticeable) amount of energy for storing data or code. However, the hardware needs energy, from a battery or an electrical socket, in order to execute code. As we model code by actions, we therefore need to strengthen the location guards of code-related actions of a computing unit A in order to prevent executing them unless there is sufficient power for doing it. We also need to model that executing code consumes energy. We do this in two steps. First, the computation unit A that contains the actions a i can compose in parallel with a hardware host HW: A || HW. The energy-awareness is modeled by using the global variables B and charge for every action a i as shown in (4). Second, for any action a i we strengthen gd(a i ) with the conjunc- tion {B, charge} (a i .loc).var. The action a i now has the form: { B , charge } ( a i . loc ) . var