@inproceedings{4561,
  abstract     = {We present a formalism for specifying component interfaces that expose component requirements on limited resources. The formalism permits an algorithmic check if two or more components, when put together, exceed the available resources. Moreover, the formalism can be used to compute the quantity of resources necessary for satisfying the requirements of a collection of components. The formalism can be instantiated in several ways. For example, several components may draw power from the same source. Then, the formalism supports compatibility checks such as: can two components, when put together, achieve their tasks without ever exceeding the available amount of peak power? or, can they achieve their tasks by using no more than the initially available amount of energy (i.e., power accumulated over time)? The corresponding quantitative questions that our algorithms answer are the following: what is the amount of peak power needed for two components to be put together? what is the corresponding amount of initial energy? To solve these questions, we model interfaces with resource requirements as games with quantitative objectives. The games are played on state spaces where each state is labeled by a number (representing, e.g., power consumption), and a play produces an infinite path of labels. The objective may be, for example, to minimize the largest label that occurs during a play. We illustrate our approach by modeling compatibility questions for the components of robot control software, and of wireless sensor networks.},
  author       = {Chakrabarti, Arindam and De Alfaro, Luca and Henzinger, Thomas A and Stoelinga, Mariëlle},
  booktitle    = {Third International Conference on Embedded Software},
  isbn         = {9783540202233},
  location     = {Philadelphia, PA, USA},
  pages        = {117 -- 133},
  publisher    = {ACM},
  title        = {{Resource interfaces}},
  doi          = {10.1007/978-3-540-45212-6_9},
  volume       = {2855},
  year         = {2003},
}

@inproceedings{4464,
  abstract     = {We introduce the paradigm of schedule-carrying code (SCC). A hard real-time program can be executed on a given platform only if there exists a feasible schedule for the real-time tasks of the program. Traditionally, a scheduler determines the existence of a feasible schedule according to some scheduling strategy. With SCC, a compiler proves the existence of a feasible schedule by generating executable code that is attached to the program and represents its schedule. An SCC executable is a real-time program that carries its schedule as code, which is produced once and can be revalidated and executed with each use. We evaluate SCC both in theory and practice. In theory, we give two scenarios, of nonpreemptive and distributed scheduling for Giotto programs, where the generation of a feasible schedule is hard, while the validation of scheduling instructions that are attached to the programs is easy. In practice, we implement SCC and show that explicit scheduling instructions can reduce the scheduling overhead up to 35% and can provide an efficient, flexible, and verifiable means for compiling Giotto programs on complex architectures, such as the TTA.},
  author       = {Henzinger, Thomas A and Kirsch, Christoph and Matic, Slobodan},
  booktitle    = {Proceedings of the 3rd International Conference on Embedded Software},
  isbn         = {9783540202233},
  location     = {Philadelphia, PA, USA},
  pages        = {241 -- 256},
  publisher    = {ACM},
  title        = {{Schedule-carrying code}},
  doi          = {10.1007/978-3-540-45212-6_16},
  volume       = {2855},
  year         = {2003},
}